Ravencheck: Effectively-Propositional Reasoning for Rust
summary
Ravencheck encodes a purely functional subset of Rust into EEPR with relational abstraction and calls SMT solvers (cvc5 or Z3) to get decidable, fast verification results. It ships as a crate plus macros that live alongside tests, models closures and higher‑order functions (no function equality or higher‑order quantifiers), and verifies CRDT-style commutativity examples by treating mutating helpers as uninterpreted with axioms. Limits include incomplete relational abstraction (debuggable via a partial‑function semantics), limited trait support, and only bounded generic handling, but the tool runs and produces concrete counterexamples or proofs.
AI-written summary · about
chapters (10)
- 0:00Ravencheck introduction
- 1:04Motivation from distributed systems
- 3:12Why verification over testing
- 5:18Tests to verification with Ravencheck
- 7:51Rust mutation and functional interface
- 9:57Dual-purpose functions in Raven logic
- 10:41Higher-order logic in Ravencheck
- 12:49Decidability and EPR restrictions
- 14:56Relational abstraction and debugging
- 15:37Q&A and tool comparison
related talks
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
58mRust for The Curious C++ Developers
19mA Hybrid Approach to Semi-automated Rust Verification
21mA Tour of Empirical Verification in Rust
50mRust's Borrow Checker Proven Correct!
20mModular Specification and Verification of Closures in Rust
20mVerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type(…)
15mModular Specification and Verification of Closures in Rust