Basilisk - Using Provenance Invariants to Automate Proofs of Undecidable Protocols

Learn about an innovative approach to automatically proving the correctness of distributed protocols through this 16-minute conference talk from OSDI '25. Discover how the Basilisk tool addresses the fundamental challenge of finding inductive invariants for formal verification without restricting protocols to decidable logic fragments. Explore the concept of Provenance Invariants, which relate local variables to their protocol step origins, enabling automatic derivation of complex inter-host properties that previously required manual developer input. Understand the Atomic Sharding algorithm that statically analyzes protocol steps to generate these invariants automatically. Examine the practical application of Basilisk across 16 distributed protocols, demonstrating how it successfully finds sufficient invariants to prove safety properties with minimal developer assistance. Gain insights into this Best Paper award-winning research that advances the field of distributed systems verification by making formal proofs more accessible and automated.