open-standards/proof/SPEC.md

Proof v0.1 — A Carrier for Verified Work

Status: v0.1.0 draft. Licence: specification text CC-BY-4.0; reference code Apache-2.0.

A vendor-neutral standard for energy-accounted formal verification. A proof obligation is content-addressed; a solver is anything that can attempt one at a declared tier; a discharged obligation seals as a signed receipt that records which tier closed it and the joules it cost. The standard fixes the one axis the field leaves implicit — joules per verified proof — and makes it portable: any prover can emit a Proof receipt, and any auditor can verify it with the family's shared JCR-1 tooling.

---

1. Scope and doctrine

1. Correctness is the verifier's, not the optimizer's. A solver returns proved only when a verifier would accept the artifact. Energy is never traded for correctness; the standard changes which tier pays for a proof, not whether it is checked.
2. Cheapest sufficient solver wins. Every obligation goes to the cheapest tier that can discharge it and escalates only on failure (§4).
3. Energy is reported, honestly. Every closed obligation carries the joules it cost with a provenance tag (§5). An estimate is never dressed as a measurement.
4. A proof is not a specification. A receipt attests that an obligation was discharged. Whether the statement encodes what was meant is a separate, declared property (spec_grounding, §2) that a prover MUST NOT self-certify.
5. Non-goals. The standard does not mandate a proof language, a solver implementation, or a model. It standardizes the goal, the cascade accounting, and the receipt — not the prover.

2. The proof obligation (REQUIRED)

A goal is { statement, context, kind, intent, grounding }:

• statement — the formal proposition, in some context (e.g. lean4@mathlib, smt2). The pair (statement, context) is the unit of identity.
• kind — a coarse difficulty hint (Trivial, Arithmetic, Decidable, General, Hard). It informs but does not bind routing.
• intent — free text: what the statement is meant to encode.
• grounding — the spec-grounding of the statement against intent: Ungrounded (default), HumanReviewed, or CrossChecked. A conforming prover MUST default to Ungrounded and MUST NOT upgrade grounding on its own.

A goal's id is blake3(statement ‖ 0x00 ‖ context) (§3). Identity depends on the statement and context only; intent and grounding do not change it.

3. Canonical serialization and content addressing (REQUIRED)

Content addresses and the signed receipt core use canonical det-CBOR (RFC 8949 §4.2.1): length-first then bytewise key ordering, shortest integer form, and no floats, bools, or nulls in the signed core. A content id is blake3(canonical_cbor(value)), rendered lowercase-hex on the wire. This is the same canonical encoding the JCR-1 receipt signs over (§6), so an id and a receipt agree on bytes.

4. The cascade (REQUIRED)

Solvers occupy a strictly ordered ladder, cheapest first:

Tier	Class	Energy (reference)
T0	deterministic automation (proof-language tactics)	~free CPU
T1	SMT / decision procedures	cheap CPU
T2	a small distilled in-domain prover	a small model
T3	a frontier reasoning model — last resort	the most expensive rung

A conforming router MUST:

1. Attempt solvers in non-decreasing tier order.
2. Stop at the first solver returning proved (the closing tier).
3. Account every joule spent, including on cheaper solvers that ran and failed first. Those joules are wasted_uj — the disclosed cost of escalation, which MUST NOT be hidden.
4. Treat a solver's refusal (it cannot decide the goal) as escalation, never as a counter-result. A solver MUST NOT report proved without verifier acceptance.

The reference energy per tier (50 µJ / 5 mJ / 0.5 J / 50 J) is non-normative. The normative requirement is that the figure is reported and honestly tagged (§5), not its value.

5. Energy and provenance (REQUIRED)

Every reading is integer microjoules with a provenance tag:

• HwShunt — read from a hardware energy interface: a shunt or power meter, the SMC, or a vendor energy counter (RAPL, NVML, Apple IOReport, ...). REQUIRES a present measured figure. A vendor counter's reading is a hardware reading, subject to the liveness requirement below.
• ModelBased — computed from a model calibrated on the host or against a reading (e.g. measured wall time × a power the host measured). A measured figure MAY be absent.
• Estimator — a figure nothing calibrated: a coarse constant, or a model run at a default or assumed parameter (e.g. measured wall time × a default power no host calibrated). A measured figure MUST be absent.

A conforming implementation MUST enforce this coupling: HwShunt without a measured figure, or Estimator with one, is invalid.

Liveness. A reading from a vendor energy counter (RAPL, NVML, Apple IOReport, ...) MAY be graded as a hardware reading only while the counter is demonstrably live for the domain the figure claims: the implementation MUST have observed the counter covering that domain advance under load (for Apple IOReport: every CPU energy rail the figure sums - the rail itself, one per die on a multi-die part - advancing on its own in at least 5 sample intervals, in at least 4 of every 5, over at least 300 ms while the probing thread burns CPU; an interval runs from when one sample is in hand to when the next is, and only one no longer than three of the probe's ticks, 75 ms at its 25 ms tick, counts: a longer one counts as nothing, neither among the intervals, nor as an advance, nor towards the 300 ms, which is the summed length of the intervals that count; one rail that held leaves the whole figure not live). A counter that is present but not live - frozen, or republished in lumps - MUST NOT produce a hardware-graded figure; the implementation falls back to its estimator or reports the work unmetered, and SHOULD record why. In this standard a hardware-graded figure is HwShunt; the fallback is ModelBased or Estimator.

Batch accounting reports, against a frontier-only baseline (every goal costed at T3), the total joules, the savings, and the energy attributed to each closing tier. The per-tier breakdown is REQUIRED so that Amdahl behaviour — the few hardest goals dominating the joules — is visible rather than averaged away.

5.1 The joule ceiling (OPTIONAL to declare, REQUIRED to honour)

Accounting says what a proof cost. A ceiling says what it is allowed to cost. A standard whose premise is joules-per-verified-proof needs both: the ladder spans a millionfold from T0 to T3, so an unbounded cascade will escalate a goal nobody wanted solved that badly into the most expensive rung available and report the bill afterwards.

A caller MAY declare a ceiling in microjoules for a run. Where one is declared:

• An implementation MUST NOT begin a rung whose nominal cost would take the run past the ceiling. The check is on the next rung's cost, before it runs. Refusing after the fact spends precisely the joules the ceiling exists to withhold.
• A ceiling below the cheapest rung's nominal cost attempts nothing and reports that it attempted nothing. This is a coherent request, not an error.
• A run halted for want of budget MUST be distinguishable from a run no rung could decide. proved = false alone conflates them, and the two are different claims about the world: a budget halt says nothing whatever about whether the goal is provable. An implementation MUST record the tier it refused.
• Actual spend MAY exceed the ceiling when a solver overshoots its nominal cost. Those joules were really spent, so the receipt MUST report them as spent rather than clamping to the budget. A ceiling bounds what is attempted, not what physics did.
• Batch accounting MUST count budget halts separately from failures, for the same reason: folding them together makes a batch look mathematically harder than it was.

Where a ceiling was declared, the receipt (§6) carries it, so a proof is not merely costed but demonstrably obtained within a declared budget. A receipt from a run with no ceiling omits the field and is byte-identical to one sealed before this section existed.

5.2 Stand-in solvers (REQUIRED to declare)

A reference stand-in is a solver that returns a verdict to exercise the ladder and discharges nothing — it decides by goal kind, never by inspecting the claim. The reference implementation ships a full ladder of them so the cascade, the accounting and the receipt can be demonstrated without a solver estate.

They are a hazard precisely because the rest of the pipeline is sound. A stand-in at the top rung returns Proved for any goal, with the content address of the goal's own statement as its "artifact" — the claim offered as its own evidence — and the sealing path will sign that into a JCR-1 receipt that verifies under the steward key. Such a receipt is not forged. It is honestly signed and substantively empty, which is worse, because it verifies.

Neither existing qualifier catches this. Provenance qualifies an attempt's energy; SpecGrounding qualifies its intent. Neither says whether the verdict was earned.

• A solver that is a stand-in MUST declare itself as one.
• An implementation MUST record, on the result and through any proof cache, whether the closing solver was a stand-in. A cache hit that dropped the marker would launder an unearned proof into an unmarked one.
• A relying party that will act on a proof MUST check it. Verifying the envelope establishes the signature, not that anything was proved. The marker therefore rides in the signed receipt as closed_by_stub (§6.1), so a party holding only the artifact can make that check without trusting the prover.
• A stand-in MUST NOT be presented as a decision procedure in any published figure or claim derived from a run.

Note the trait-level default is "not a stand-in", which is the unsafe direction and is deliberate: it keeps real solvers from having to opt out, but it means the declaration is a contract on the implementor, not a property the framework can infer. A new stand-in that forgets to declare itself is indistinguishable from a real one.

6. The receipt (REQUIRED)

A discharged obligation seals as a JCR-1 receipt — the family's shared signed-receipt envelope: canonical det-CBOR inside a COSE_Sign1 envelope (RFC 9052, EdDSA/Ed25519, alg = -8). The proof/1 profile signs a flat uint/text core:

proof_receipt     = "proof/1"
goal_id           = hex(blake3(statement ‖ 0x00 ‖ context))
verdict           = "proved" | "unproved"
closed_by         = "T0".."T3"           ; omitted if unproved
artifact          = hex(content-id)      ; omitted if unproved
total_uj          = uint                 ; all joules, incl. escalation
wasted_uj         = uint                 ; joules on failed cheaper attempts
baseline_uj       = uint                 ; frontier-only cost of this goal
energy_provenance = "HwShunt" | "ModelBased" | "Estimator"
spec_grounding    = "Ungrounded" | "HumanReviewed" | "CrossChecked"
from_cache        = 0 | 1
closed_by_stub    = 1                    ; omitted when the closer was real (§5.2)
ceiling_uj        = uint                 ; omitted when the run was unbounded
steward           = the signer's id (the COSE kid)

A conforming implementation MUST refuse to seal a receipt for an unproved goal, and MUST carry spec_grounding so a receipt for an Ungrounded statement says, in the signed artifact itself, that the statement was not validated against intent. Proof receipts are byte-compatible with the family's JCR-1 verifiers.

6.1 closed_by_stub — the verdict's own qualifier

An implementation MUST emit closed_by_stub = 1 when the rung that closed the goal was a reference stand-in (§5.2), and MUST omit the field otherwise.

§5.2 already requires a relying party to check this before acting on a proof. Until it entered the signed core the marker lived only on the in-process result, so a party holding only the receipt — which is the entire purpose of sealing one — could not perform the check the specification asks of them. A verifier that must consult the prover to learn whether a proof is real is not a verifier.

closed_by does not answer this. It names a tier, and the same tag covers a real decision procedure on one ladder and a stand-in on another; T0 is a propositional decider in a real ladder and a GoalKind gate in the reference one. Nor do the other qualifiers: energy_provenance qualifies the energy and spec_grounding the intent. This is the only field that says whether the verdict was earned.

Omit-when-false is normative, not an optimization. It makes the field free for honest proofs: a receipt closed by a real solver canonicalizes to exactly the bytes it did before this field existed, so every such receipt sealed under an earlier revision still verifies. The byte cost falls only on receipts that were making an unearned claim.

7. The cache (RECOMMENDED)

A verified proof SHOULD be memoized by goal id. An identical goal then closes for zero new joules (from_cache = 1, total_uj = 0), and the accumulating corpus of verified proofs — not the routing — is the durable asset. The cache is the energy flywheel: the more proved, the cheaper future proofs become.

A cache hit's zero is not a reading: nothing was metered to close it. Its energy_provenance MUST be Estimator, never the grade of the solver that closed the goal when it was first proved, so a hit can never be graded above the proof it reuses or present a measured zero.

8. Conformance

A conforming implementation passes, with real checks:

• C1 — cheapest-sufficient routing: each goal closes at the cheapest tier that can discharge it.
• C2 — disclosed escalation: total_uj equals the sum of all attempts, and wasted_uj is exactly the joules of cheaper attempts that failed first.
• C3 — energy honesty: the ladder is strictly monotone; the batch is accounted against a frontier-only baseline with non-negative savings.
• C4 — the flywheel: re-proving an identical goal costs zero new joules.
• C5 — the receipt: a proved result seals to JCR-1 and verifies; a wrong steward fails.
• C-neg: provenance coupling is enforced; an unproved goal cannot be sealed; a tampered envelope fails; canonical CBOR rejects floats/bools.

Published vectors live in conformance/v1/ (cargo run -p proof-conformance --bin gen-vectors).

9. Non-goals

The standard does not certify a prover's capability, does not validate that a statement encodes a real-world requirement (that is the spec_grounding axis, owned by humans), and does not prescribe a model or a proof language. Efficiency diffuses; the standard's contribution is to make the joules portable and the spec-grounding honest, so that "verify every line" can be reasoned about as a cost, not a slogan.