Correctness Proofs of Distributed Systems with Isabelle

Explore the world of correctness proofs for distributed systems using Isabelle/HOL in this 43-minute conference talk from Strange Loop. Dive into the limitations of testing and the power of mathematical proofs for covering infinite state spaces. Learn about automated theorem provers and computerized proof assistants, with a focus on Isabelle/HOL as an interactive tool for formally proving algorithm correctness. Watch live demos of Isabelle in action, analyzing distributed system algorithms and proving theorems. Gain insights into the reasoning style used in proof assistants and discover how they can be applied to real-world problems in distributed systems. Follow along as the speaker covers introduction, motivation, consensus algorithms, agreement properties, theorems, and invariants. While the learning curve for proof assistants is steep, this talk provides a valuable introduction to their potential in ensuring the correctness of complex distributed systems.

Introduction
Motivation
Consensus algorithm
Agreement property
Theorem
Invariants