V8 · Proof-validity

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

Verus is sound: what it reports verified holds of the code.

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.