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 (RAPL/NVML/SMC). REQUIRES a present measured figure.
• ModelBased — computed from a calibrated per-operation model (e.g. measured wall time × a power model). A measured figure MAY be absent.
• Estimator — a coarse constant. A measured figure MUST be absent.

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

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.

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
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.

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.

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.