V7 · Proof-validity

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

The specifications the proofs prove against (decide_spec, step_spec, inv, chained, the lemma statements) say what the SPEC’s English means. A proof certifies a wrong specification as readily as a right one; each proved invariant has a gym entry written from the English to catch the difference (§17a).

Sites: policy, txn, schema

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.