Martin Kleppmann's blog

Prediction: AI will make formal verification go mainstream

8 Dec 2025

Prediction: AI will make formal verification go mainstream

8 Dec 2025

Much has been said about the effects that AI will have on software development, but there is an angle I haven’t seen talked about: I believe that AI will bring formal verification, which for

Pudding: user discovery for anonymity networks

5 Jul 2024

Pudding: user discovery for anonymity networks

5 Jul 2024

I’d like to introduce an exciting new research paper I worked on! It’s about a system called Pudding, and it was presented by Ceren at the IEEE Symposium on Security and Privacy, one of the top

2023 year in review

4 Jan 2024

A lot has happened in the last year, so I thought it would be good to write up a review. My biggest change in 2023 was that my wife and I had a baby! This has brought a mixture of joys and

Verifying distributed systems with Isabelle/HOL

12 Oct 2022

Verifying distributed systems with Isabelle/HOL

12 Oct 2022

This post also appears on Larry Paulson’s blog. We use distributed systems every day in the form of internet services. These systems are very useful, but also challenging to implement because

Book Review: The Future of Fusion Energy

3 Jan 2022

Book Review: The Future of Fusion Energy

3 Jan 2022

I give a five-star ⭐️⭐️⭐️⭐️⭐️ rating to the following book: Jason Parisi and Justin Ball. The Future of Fusion Energy. World Scientific, 2019. ISBN 978-1-78634-749-7. Available

Several podcast interviews

1 Sep 2021

I regularly get asked to give interviews on the topics that I work on, especially for podcasts. To make them easier to find for anybody who’s interested, I thought I would make a list. They touch

Several podcast interviews

1 Sep 2021

It's time to say goodbye to the GPL

14 Apr 2021

It's time to say goodbye to the GPL

14 Apr 2021

The trigger for this post is the reinstating of Richard Stallman, a very problematic character, to the board of the Free Software Foundation (FSF). I am appalled by this move, and join others in the

Building the future of computing, with your help

23 Feb 2021

For the last five or six years, since I bid goodbye to the startup scene and Silicon Valley, I have been increasingly working in public. I have written a book, given around 100 talks (many of which

Building the future of computing, with your help

23 Feb 2021

Decentralised content moderation

13 Jan 2021

Who is doing interesting work on decentralised content moderation? With Donald Trump suspended from Twitter and Facebook, and Parler kicked off AWS, there is renewed discussion about what sort of

Decentralised content moderation

13 Jan 2021

Using Bloom filters to efficiently synchronise hash graphs

2 Dec 2020

This blog post uses MathJax to render mathematics. You need JavaScript enabled for MathJax to work. In some recent research, Heidi and I needed to solve the following problem. Say you want to sync a

Using Bloom filters to efficiently synchronise hash graphs

2 Dec 2020