4 posts
Bounded model checkers like Kani and relational model finders like Alloy let you verify properties with ordinary assertions and constraints.
You don't need to learn linear temporal logic to use a model checker. Tools like Kani, CBMC, and Alloy let you verify properties with ordinary assertions and…
Model checking tools like Kani let you verify Rust properties with assertions instead of formal proofs.
You can prove Rust code correct without writing a single proof. The tool that does it is called a model checker, and for Rust the most practical one right now…
Differential testing lets you find bugs without knowing the correct answer. The problem is that correlated mistakes look like agreement.
You can trust differential testing without a formal proof, but only if you understand exactly where it falls apart. The weakness is called common-mode failure.…
N-version programming assumes your implementations agree.
You built an n-version system. Three independent implementations of the same critical function, a voter that picks the majority result, and a warm feeling that…