Today I am happy to announce a very exciting new research project that I’ve been working towards for years!

We are establishing the Centre for Cryptographic Trust Infrastructure (CCTI), funded initially by a £2.4m grant from the Advanced Research + Invention Agency (ARIA) through the Scaling Trust programme. CCTI is a collaboration between the University of Cambridge Department of Computer Science and Technology, the nonprofit SINE Foundation, my longstanding collaborators at Ink & Switch, and the startup Light Squares.

The overall goal of the ARIA Scaling Trust programme is to enable AI agents to coordinate securely on their owners’ behalf, across both the digital and physical worlds. The programme is funding several teams that are investigating the use of cryptography to enable such coordination.

ARIA is a fairly new funding body in the UK, started only 3 years ago. It is modelled after DARPA, but with a civilian rather than military remit. ARIA’s goal is to fund ambitious research that, if successful, will have a huge positive impact on society. For the last year ARIA has already been funding a lot of my collaborators’ work on Automerge through the Safeguarded AI programme, and now I am extremely grateful for their support for CCTI as well!

Introducing CCTI

Imagine you’re a manufacturing company, and you have an AI agent that is tasked with finding a supplier for a particular component you need. Your agent may contact various potential suppliers, even interacting with their agents if they have them. But it’s a messy world out there. How is your agent supposed to know if the other agents are telling the truth? They might be fraudsters, pretending to have the product you want while actually giving you something else (or nothing at all). If you don’t already have some sort of prior history or another way of establishing reputation, there is no way for the agents to know whether they can trust each other.

The traditional economy solves this problem through trusted third parties such as certification bodies, and by using expensive, slow, and manual processes for vetting potential suppliers (for example, flying someone over to inspect their factory in person). But maybe our brave new AI world will allow us to do this faster, cheaper, and more reliably?

Our hypothesis is that cryptographic protocols such as zero-knowledge proofs provide a way for one agent to prove to another that it is telling the truth, but without revealing commercially sensitive data. For example, it would allow a supplier to prove that its products were indeed manufactured using a particular process as claimed. If this works, we believe that it will unlock huge economic opportunities.

But wait, I hear you ask: cryptography can only prove something about the relationship between one number and another number. How could it ever prove something about the physical world? Well, as it happens, for the last two years my PhD student Jessica and I have already been busy using cryptography to prove things about the physical world, and CCTI is a generalisation of this line of work.

In our Emission Impossible paper, Jessica and I show how the operator of a datacenter could cryptographically prove to its customers what carbon emissions have arisen from each customer’s use of computing resources in the datacenter. Since it’s about emissions, it’s about the physical world. We chose datacenters as the use case for that paper because it allowed us to make some simplifying assumptions; in particular, we considered only electricity as the source of emissions and ignored, say, hardware manufacturing. But in subsequent work we’ve been chipping away at these assumptions, and generalising the technique to other use cases.

From the carbon emissions example you can see that we’re interested in sustainability issues. We have also looked into using similar techniques for other sustainability concerns, such as verifying that agricultural commodities were not grown on recently deforested land (as required by the EU Deforestation Regulation). CCTI is broader than this – we’re interested in any case of mutually untrusting parties wanting to establish a trust relationship – but I believe the approach is particularly valuable in the context of sustainability, where companies have a tendency of making dubious claims (“greenwashing”), but where accuracy is important if we want to actually achieve our sustainability goals, such as reducing carbon emissions.

But how does it work?

I will leave a more detailed explanation of our technical approach to another post, but for now I wanted to give a brief outline of how we intend to actually make this work, since otherwise this project may seem outlandish.

Say you want to prove a property about some physical production process (e.g., that your company’s steel was manufactured with a low-carbon process, such as direct reduction with green hydrogen and using an electric arc furnace powered by renewable electricity, rather than a blast furnace). Analysing a sample of the material itself may tell you the process, but it does not tell you what carbon intensity was associated with the hydrogen and the electricity. Thus, we need to prove a property that is not directly observable.

However, indirect facts are observable, and indeed cryptographically attestable. We can download a list of financial transactions from the company’s bank account, and prove using TLSNotary or a similar tool that the transactions are genuine (assuming you trust the bank’s TLS certificate). We can verifiably associate each financial transaction with a digital invoice, and attach product and emissions data to the invoices. That way, you could prove cryptographically that the steel company did not buy any coke, but it did buy a lot of renewable electricity and a lot of green hydrogen (themselves attested through recursively validated proofs). You also need to prove that the company is not reselling high-emissions steel from another producer. And if you can do that, the result is compelling evidence that the steel is indeed green as claimed.

Additionally, the proof process could take input from many other sources: sensor data from trusted sensors can be digitally signed, emails can be authenticated via DKIM signatures, company identities can be attested by government websites, and certification bodies can issue digital certificates. All of these cryptographically attested facts can then feed into a big zero-knowledge proof that deduces the fact you want to prove using domain-specific logic.

There is a lot more to this project – we are exploring game-theoretic models to help agents establish what further evidence would be needed to come to an agreement, allowing us to weigh up the cost of producing the evidence against the benefits it would bring. We are looking into real-world use cases from several different industries to inform the design of the whole system, and we will use LLM-based prototypes to measure the degree to which cryptographic protocols increase the ability of untrusting agents to establish trust and come to an agreement.

If that sounds very ambitious – well, it is. But we think that we have a viable plan for making it happen. And if it works, this project will be hugely impactful, potentially changing the way the world economy works by enabling new business models that would have been infeasible previously. And maybe we can even embed sustainability concerns in every single purchasing decision – which will be critical for decarbonising the economy.

CCTI doesn’t have a website yet, as we’re just getting started. But we’ll be writing more about our work as it progresses. Stay tuned!

I just published a short post in which I argue that AI will make formal verification go mainstream. There are three reasons why I think this:

1. A future where LLMs can write proofs of correctness fully automatically, without human input, seems within reach. That will make formalisation vastly cheaper than it has been for the last few decades.

2. If you generate code using AI, but then have to carefully review it by hand, you don’t save much time overall. But if the AI proves that the code is correct, you can confidently use it without having to even look at it.

3. LLMs are great at making up plausible-sounding nonsense, but automated proof checkers won’t be fooled by this, which makes it much safer to use LLMs in this context.

For comments, please find me on Bluesky!

Yesterday (sorry for not sending the announcement sooner) the Bluesky team and I published a paper that’s a bit like a long blog post in PDF format. It’s called “Bluesky and the AT Protocol: Usable Decentralized Social Media”; it describes the architecture and of the Bluesky social network and the underlying AT Protocol, and more importantly, it explains the rationale of why things are designed that way. The paper is a result of me advising the Bluesky team over the course of the last two years.

Social media requires lots of difficult choices, because humans are complicated, but I believe Bluesky does a really good job of balancing the trade-offs. It’s also getting quite popular, having just jumped from about 3 million to 4 million users yesterday! You can find me at @martin.kleppmann.com.

I just posted a review of my year 2023 on my blog: https://martin.kleppmann.com/2024/01/04/year-in-review.html

It’s been an eventful year: my wife and I had a baby, I got a new job (faculty in Cambridge), my industrial collaborations with Automerge and Bluesky have been very successful, local-first software is catching on, I’ve made some progress with the second edition of my book, I organised events and gave talks, and I have published a couple of new research papers.

Hope you have a good 2024!

There’s a new post on my blog: “Verifying distributed systems with Isabelle/HOL”. In this post, I share we’ve learnt about formally proving the correctness of distributed systems algorithms using the Isabelle proof assistant. This is software that can automatically check whether your proofs are correct.

Isabelle doesn’t have any built-in support for distributed systems, but fortunately it’s not too difficult to model a distributed system using the built-in primitives of Isabelle/HOL (one of the standard libraries for Isabelle). This post shows how it’s done.

https://martin.kleppmann.com/2022/10/12/verifying-distributed-systems-isabelle.html

It’s a blog version of a video I made a few years ago. It’s also cross-posted on Larry Paulson’s blog (he’s one of the creators of Isabelle).

When several people work on a document asynchronously, at some point the time comes when you want to merge those changes, and that’s where things get difficult. Our latest paper, on Peritext, addresses this problem. It allows several users’ edits to a rich-text document to be merged while preserving each user’s edits as much as possible. Peritext brings a Git-like collaboration model (with arbitrary branching and merging) to rich text, but without manual resolution of merge conflicts.

Besides the article, our prototype implementation is also open source. Hope you find it interesting!

You can find it here: https://martin.kleppmann.com/2021/09/01/podcast-interviews.html

Just don’t listen to them all at once — you’ll get sick of me droning on and on!

— Martin

My latest blog post is a short paper that I presented today at the 14th Workshop on Hot Topics in Privacy Enhancing Technologies (HotPETs 2021). It’s a proposal for a potential compromise: a way of adding a backdoor to end-to-end encrypted communication systems without opening the door to mass surveillance.

You can find it here: https://martin.kleppmann.com/2021/07/16/cryptographic-backdoors-hotpets.html

I expect this is going to be controversial! Constructive responses welcome as always.

— Martin

You can find it here: https://martin.kleppmann.com/2021/04/14/goodbye-gpl.html

Please let me know your thoughts!

(Sorry that this email notification is delayed by a few days — I was having some trouble with Substack.)

— Martin

Substack is actually a service for sending email newsletters. However, I am not planning to change my blog into a newsletter, since I like my self-hosted setup. I am simply using it as a way of sending email notifications about new blog posts to anyone who wants to receive them.

If you no longer want to receive these messages, apologies for the intrusion, and there should be a link at the bottom to unsubscribe.

New blog post: Building the future of computing, with your help

Moving on to today’s actual news. I have launched a Patreon account! Since most of my work is given away for free (conference talks, educational videos, research papers, open source code, blog posts), I rely on other sources of funding. At the moment I am funded by a charitable research grant, but this is a non-renewable fixed-term contract, and so I am looking to Patreon as a way of hopefully building up a sustainable income that will allow me to continue doing my work when this contract ends.

My blog post goes into more details on what I am planning to do over the next few years, and the Patreon profile details what you get in return for supporting me. Think of it not as a donation, but as an investment in my future work. I aim to give you a good return on your investment through producing teaching materials and research that you will hopefully find useful. I will continue giving away most of my work for free, but as a supporter on Patreon you will be the first to see any new work as it is created.

If you have found my work useful – for example, if you have applied ideas from my talks in your work, or if my book helped you get a job – then I would be especially delighted to welcome you as a supporter on Patreon!

Thanks for your support and best wishes,

Martin

I’ve set up Substack as a way of sending notification emails when I write something new on my blog, martin.kleppmann.com. I mostly write about distributed systems, databases, and information security. My blog posts are infrequent (typically a handful per year) so this is a very low-volume email list.

Subscribe now

You can also tell your friends!