Discover more from Martin Kleppmann’s Blog
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.
Thanks for reading Martin Kleppmann’s Blog! Subscribe for free to receive new posts and support my work.