13df129cb0
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]>
30 lines
1.3 KiB
Text
30 lines
1.3 KiB
Text
Creative Commons Attribution 4.0 International
|
|
|
|
Copyright (c) 2026 Transaction Science, Inc.
|
|
|
|
This specification text and accompanying documents are licensed under the
|
|
Creative Commons Attribution 4.0 International License (CC BY 4.0).
|
|
|
|
You are free to:
|
|
- Share — copy and redistribute the material in any medium or format
|
|
- Adapt — remix, transform, and build upon the material for any purpose,
|
|
even commercially
|
|
|
|
Under the following terms:
|
|
- Attribution — You must give appropriate credit, provide a link to the
|
|
license, and indicate if changes were made. You may do so in any
|
|
reasonable manner, but not in any way that suggests the licensor
|
|
endorses you or your use.
|
|
|
|
No additional restrictions — You may not apply legal terms or technological
|
|
measures that legally restrict others from doing anything the license
|
|
permits.
|
|
|
|
Full licence text: https://creativecommons.org/licenses/by/4.0/legalcode
|
|
|
|
────────────────────────────────────────────────────────────────────────
|
|
|
|
Reference implementations and software accompanying this specification, if
|
|
and when published in this directory, may be released under a separate
|
|
licence (typically Apache-2.0). Refer to the licence file alongside each
|
|
artefact.
|