Transaction-Science/open-standards
Watch
1
0
Fork
You've already forked open-standards
 0
Code Issues Pull requests Projects Releases 15 Packages Wiki Activity Actions 7
open-standards/proof/CONTRIBUTING.md
Transaction Science 13df129cb0 Add the proof open standard — a carrier for verified work 
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]>
2026-06-07 15:30:07 -04:00

1.7 KiB
Raw Permalink Blame History

Contributing to Proof

Proof is one of the Transaction Science open standards. The wire format and the right to fork are public; Transaction Science is the steward, not the proprietor.

Ground rules

  • Reference code (proof-rs/) is Apache-2.0. Specification text (SPEC.md) is CC-BY-4.0.
  • Rust toolchain is pinned by the repo rust-toolchain.toml. cargo test --workspace MUST pass and cargo clippy --workspace --all-targets MUST be warning-free.
  • Any change to a wire structure (the proof/1 receipt core, the canonical encoding) requires regenerating and committing conformance/v1/ (cargo run -p proof-conformance --bin gen-vectors -- conformance/v1).
  • A solver MUST NOT return proved without verifier acceptance, and MUST NOT upgrade a goal's spec_grounding on its own. These are correctness and honesty invariants, not style.

The smallest valuable contributions

  • Real backends behind the Solver trait: a Lean tactic runner at T0, CVC5 alongside z3 at T1, a distilled in-domain prover at T2 — each reporting what actually happened, with measured energy.
  • Measured energy: a HwShunt backend (RAPL/NVML) so a solver reports hardware-measured joules instead of a wall-time model.
  • Conformance: adversarial negatives (a router that hides escalation waste, a receipt sealed for an unproved goal, a provenance/measured mismatch), and independent implementations certifying against conformance/v1/.
  • Spec-grounding tooling: cross-checkers that earn a CrossChecked grounding by comparing a statement against an independent encoding — the honest path the standard refuses to let a prover shortcut.

Issues and PRs scope by the proof subdirectory tag.