V9 · Proof-validity

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

Z3, the solver Verus calls, is sound.

Sites: every proof

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.