The verification cargo class: energy-accounted formal verification as a
vendor-neutral standard. A proof obligation is content-addressed; a solver
attempts one at a declared tier; a discharged obligation seals as a signed
JCR-1 receipt recording which tier closed it and the joules it cost. The
cheapest sufficient solver wins, correctness stays the verifier's, and the
joules a cheaper solver spent before failing are disclosed, never hidden.
- SPEC.md (§1–§9): the obligation, canonical det-CBOR addressing, the
cheapest-sufficient cascade with disclosed escalation, the honest
energy/provenance model, the proof/1 JCR-1 receipt, the cache, conformance.
- proof-rs/: a 6-crate Apache-2.0 reference workspace. Two real rungs with
measured energy — an in-process propositional decider (T0) and z3, shelled
or kept resident (T1) — over honest model-tier stand-ins; the escalation
router with the proof-cache flywheel and frontier-only baseline accounting;
the proof/1 receipt vendored byte-compatible with the family JCR-1 verifiers;
C1–C5 + a negative pack, all checks real, with published vectors.
- proof carries spec_grounding in the signed receipt: a proof is not a
specification, and a prover may never self-certify that the statement
encodes intent.
cargo test --workspace green; cargo clippy --workspace --all-targets clean.
JouleProof (jouleproof.transaction.science) is the steward + services layer
over this standard.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
13df129cb0