methods / formal
Formal verification and model checking
Proves or exhaustively explores properties: model checking, proofs, undefined-behaviour interpreters.
When: When a bug would be a memory-safety violation or an interleaving that tests are unlikely to hit: unsafe code, lock-free structures, consensus and protocol logic.
3% of scanned repositories run at least one
5 tools detected
Undefined-behaviour detection
called for by: threads, async code, locks, shared state
Catches: Memory-safety and aliasing violations in unsafe code.
Concurrency model checking
called for by: threads, async code, locks, shared state
Catches: Races and orderings that fail only under specific interleavings.
Proofs and specifications
called for by: algorithms, parsers, data transforms
Catches: Design-level bugs in protocols and algorithms, checked against a specification.