Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols
summary
Basilisk is a Daphne compiler extension that automatically derives inductive invariants for distributed protocols using Provenance Invariants and an analysis called Atomic Sharding and then checks inductiveness so developers avoid the trial‑and‑error loop. The tool proves safety for 16 protocols including MultiPaxos, reduces manual invariant work to zero in the evaluation, emits invariants that imply safety with little hinting, and is implemented and validated end‑to‑end.
AI-written summary · about
chapters (5)
- 0:00Basilisk introduction
- 4:53Inductive invariant automation
- 8:46Provenance invariants insight
- 13:39Automating invariant generation
- 15:24Summary and evaluation
related talks
16mInductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline...
14mDistAI: Data-Driven Automated Invariant Learning for Distributed Protocols
11mFinding Invariants of Distributed Systems: It's a Small (Enough) World After All
45mCorrectness proofs of distributed systems with Isabelle
19mLiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols
19mMostly Automated Verification of Liveness Properties for Distributed Protocols w...
14mA Refinement Methodology for Distributed Programs in Rust
21mEnabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based S...