V11 · Proof-validity

planarian @ a924e09 · Spec v4.6 · snapshot main · all versions

Kani and its back end CBMC are sound within the stated bounds.

Sites: txn::kani, exec::kani

If it is false

Every proof stops describing the real machine: it is proof-validity trust.

No invariant names it in docs/verification-ratio.toml.