# Contributing to Proof

Proof is one of the [Transaction Science open standards](../README.md). 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.