formal-verify
Formal verify
Model individual protocols or sequential invariants. Map counter-examples to events and locations in the source code. Before reporting a pass, confirm that each checked property detects a relevant mutation and that its checker passes.
Choose tools according to the target:
| What can go wrong | Tool | Why |
|---|---|---|
| Thread interleavings that lose wakeups, free resources twice, deliver items twice or out of order, block close, or report errors on the wrong thread | TLA+ with TLC | TLC explores the states of a small instance and reports counter-examples |
| Overflow, out-of-bounds access, panics and broken invariants in a Rust function with bounded loops | Kani | Kani checks the real code for every input within the stated bounds |
| Arithmetic or sequential transitions that break bounds, invariants or encoder round trips, or reach states the code assumes impossible | Lean 4 | Evaluate bounded instances, then prove the property for every size |
Prefer Kani when the function is Rust and its inputs and loops can be bounded, because it checks the production function directly. Use Lean when the property must hold for every size or the code is not Rust.
A thread protocol that depends on arithmetic such as slot = item mod window needs both tools. Use TLA+ for the interleavings with the arithmetic as a constant, and Lean for the arithmetic.
Use the tool the user names. When the table gives another tool for part of the target, report what the named tool leaves unchecked.