Verifying distributed systems with Isabelle/HOL
Hi there! Not posted for a while. In case you’re wondering, you’re getting this email because you subscribed to my blog posts at martin.kleppmann.com.
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).