The formal tier is now a live gate, not just an example. When a run carries
`<workspace>/.joule-fix/formal.json` (a domain JouleContract + the
Formalizations encoding the obligations the fix must honor), the harness
discharges them through the joulecontract→proof vericoding bridge over a real
z3, as a seventh gate `formal-proof`. A refuted or unproven obligation fails the
gate and reverts the fix exactly like a failed test — the rung above build+test.
- Decision-procedure ladder only ([Propositional, Z3Smt]); a formal gate must
not fall through to a model stand-in.
- The spec is loaded + validated UP FRONT (indices, duplicates), before any
edit, so a malformed spec fails on a clean tree rather than mid-run (which
would otherwise leave the operational fix un-reverted).
- Per-obligation discharge written to .joule-fix/formal-discharge.json as
re-checkable evidence; proof joules reported (ModelBased, in-process) beside
the cargo-attributed gate energy. No formal.json ⇒ no formal gate, run is
identical to before.
Live, both directions, on real z3:
- correct postcondition (net = debits - credits): formal-proof ✓ (proved by
Smt, 0.10 J), all seven gates green, fix ships.
- buggy postcondition (net = debits + credits): all six OPERATIONAL gates
green, but formal-proof ✗ (1 refuted, counter-model debits=credits=1⇒net=2),
fix REVERTED, refusal receipt. An operationally-valid lint fix refused
because its formal claim was disproved.
Two harness tests (proven→ships, refuted→reverts), gated on z3 availability.
Example's soundness note updated (the proof crate now halts on refutation).
Co-Authored-By: Claude Opus 4.8 <[email protected]>
b5cce1b398