# Formal assurance classification

Ten constructive propositional obligation lemmas are machine checked by the
small proof-term type checker in assurance/v127/formal/check.mjs. Their abstract
FINAL constructor is explicitly the conjunction of required obligations. These
lemmas do not prove production JavaScript, arbitrary histories, provider behavior,
exclusive-head consensus or physical truth. They cannot be advertised as the ten
unbounded temporal theorems requested in the assurance program.

The existing finite model, canonical vectors, mutations and schedule simulations
are executable evidence under their declared assumptions. TRACEABILITY.json maps
guards to specifications and tests; mapping presence is not semantic refinement.
Unbounded state-machine proofs and verified refinement remain open engineering.
No Lean/Coq/SMT solver was available in this execution environment.

V128 adds quorum-proof.py with Z3 4.15.4: the negation of the unbounded integer
cardinality lemma is UNSAT with satisfiable premises and a SAT counterexample
when the intersection guard is removed. It does not prove signer non-equivocation
or implementation refinement. formal-model.mjs separately checks a bounded
monotonic/revocation model; its exact state/transition/depth population is recorded.