A pipeline example that composes EVERY methodology-layer standard into a
single certified release — the thesis "vibe coding you can take to an
auditor" made executable:
spec-coverage : 2/2 clauses · complete=true (joule-code-spec)
review : two-stage, independent → approved (joule-code-review)
contract : postcondition PROVED via z3 + frame (joulecontract-proof
in-footprint → gate green + joule-code-joulecontract)
attested-build: verified
→ ✓ CERTIFIED · every clause traces to a proof, an approval, a metered build
The contract gate is the honest composition of its two halves: the formal
postcondition ("if debits==credits then net==0") discharged through z3 over
the JouleProof cascade (a real machine-checked proof, ~1.3 J), AND the frame
checked structurally (the ops' edits stayed in the declared footprint) —
because a frame is a footprint obligation, not a proof goal. Both, or the
gate is red.
Then the other terminal state: pull the independent reviewer (the author
reviews their own op) and separation-of-duties voids it → the same release
is REFUSED, naming [review]. Two outcomes, no third.
The cross-standard deps (joulecontract, proof) are dev-only, so a downstream
consumer of joule-code-release stays light. Runnable:
`cargo run -p joule-code-release --example pipeline` (needs z3 for the
contract gate; without it the postcondition is honestly unproved and the
release refuses — never a faked pass).
Co-Authored-By: Claude Opus 4.8 <[email protected]>
9dd7faa3e3