V10 · Proof-validity

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

rustc compiles the verified code to a program with the semantics Verus checked.

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.