Martin Kleppmann

Distributed systems researcher and O'Reilly author

Dr Martin Kleppmann is a researcher in distributed systems at the University of Cambridge, and author of the acclaimed Designing Data-Intensive Applications┬Ł (O'Reilly Media, 2017). He mainly works on collaboration software, CRDTs, and formal verification of distributed algorithms.

Previously he was a software engineer and entrepreneur at Internet companies including LinkedIn and Rapportive, where he worked on large-scale data infrastructure.

Past Activities

Martin Kleppmann
Code Mesh LDN
08 Nov 2019
14.30 - 15.15

Correctness proofs of distributed systems with Isabelle

Testing systems is great, but tests can only explore a finite set of inputs and behaviours, while many distributed systems have an infinite state space. If you want to be sure that a program does the right thing in all possible situations, testing is not sufficient: only mathematical proof can cover an infinite state space. This talk introduces Isabelle/HOL, an interactive proof assistant (a kind of programming language and REPL for proofs), and explores how to formally verify distributed algorithms.






Attendees will:

  • Get a taste of why and how we can formally verify software and algorithms
  • Understand the most important reasoning tools available, such as proof by induction
  • Learn about the difference between proof assistants like Isabelle and model-checkers like TLA+


Software developers who have experience developing distributed systems, but who have not previously done any formal verification.