The vericoding seam existed but had only ever closed propositional
tautologies (p | !p) in tests — which proves the plumbing, not the claim.
This makes the claim real:
- a z3-gated integration test discharges a genuine arithmetic postcondition
("if debits equal credits, the net settlement is zero") encoded as an
SMT-LIB2 goal whose negation z3 finds unsat — i.e. the property holds for
all integers. It closes at the SMT tier with real measured joules; the
pre/frame obligations, having no formalization, stay Unformalized (demoted,
never faked). Where z3 is absent the obligation shows Unproved, never a
fabricated pass — the standard's honesty rule holds in CI too.
- a runnable example (`cargo run -p joulecontract-proof --example vericode`)
prints the per-obligation ledger end to end: the postcondition PROVED at
the SMT tier with its measured energy, the unformalized obligations honestly
marked, and discharged=false because the whole contract isn't proved. This
is the artifact the "45% of AI code fails in production" pitch needs — a
contract clause machine-proved, priced in joules.
6 lib tests (z3-gated test skips cleanly without a solver); example clean;
clippy clean.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
5cec3a0fbd