proof-aware-crypto-tooling-.../AGENTS.md

# AGENTS.md

Guidance for future Codex runs in this repository:

- Do not add Charon or Aeneas transpilation flows.
- Do not regenerate Lean from Rust. Treat shipped Lean files in verified repos as the artifact.
- Do not claim end-to-end verification unless theorem coverage actually exists.
- Keep macOS and Apple Silicon portability. Do not rely on GNU `timeout`, `free`, `taskset`, Docker, Nix, or x86_64 assumptions.
- Prefer explicit theorem-boundary language over marketing language.
- Update tests with every behavior change.
- Do not silently lower risk ratings. A lower score must explain the failed or missing evidence.
- Do not hide proof failures behind warnings.
- Keep claim cards machine-readable and reports explicit about proven claims, preconditions, exclusions, trusted base, and residual risk.
- Consequence-producing commands must be policy gated. Do not build wallet or trading-agent artifacts from `R3` arithmetic evidence.
- Distinguish verifier capability failures from proof failures. Missing `Mathlib`, missing `Aeneas`, or a missing pinned env script means local replay is unavailable; do not treat it as a clean proof.
- Third-party proof-checking attestations are allowed only as an explicit trust transformation. They must identify the provider, subject repo/commit, theorem names, observed axioms, and signature status. Untrusted attestations must not authorize builds.
- Transparency receipts must be verified against the exact attestation bytes, Signed Tree Head, log public key, and inclusion proof before they can authorize consequences.
- Keep the Merkle log RFC 9162-style unless a new standard is deliberately adopted and documented. Do not replace it with an ad hoc hash chain.
- Do not pretend ML-DSA exists. If no real ML-DSA backend is available, record the signature slot as unavailable and fail closed for policies that require both Ed25519 and ML-DSA.
- Provider private keys and transparency log state belong under ignored `provider/state/` or `provider/out/` paths. Do not commit local trust state.
- Curriculum notebooks are generated by `scripts/build_curriculum_notebooks.py`. Update the generator, regenerate `notebooks/`, and keep notebook code cells output-free.
initial proof-aware tooling prototype 2026-07-03 08:51:03 +00:00			`# AGENTS.md`

			`Guidance for future Codex runs in this repository:`

			`- Do not add Charon or Aeneas transpilation flows.`
			`- Do not regenerate Lean from Rust. Treat shipped Lean files in verified repos as the artifact.`
			`- Do not claim end-to-end verification unless theorem coverage actually exists.`
			- Keep macOS and Apple Silicon portability. Do not rely on GNU `timeout`, `free`, `taskset`, Docker, Nix, or x86_64 assumptions.
			`- Prefer explicit theorem-boundary language over marketing language.`
			`- Update tests with every behavior change.`
			`- Do not silently lower risk ratings. A lower score must explain the failed or missing evidence.`
			`- Do not hide proof failures behind warnings.`
			`- Keep claim cards machine-readable and reports explicit about proven claims, preconditions, exclusions, trusted base, and residual risk.`
add policy-gated agent consequences 2026-07-03 09:05:06 +00:00			- Consequence-producing commands must be policy gated. Do not build wallet or trading-agent artifacts from `R3` arithmetic evidence.
add verifier bootstrap and attestation lane 2026-07-03 09:24:13 +00:00			- Distinguish verifier capability failures from proof failures. Missing `Mathlib`, missing `Aeneas`, or a missing pinned env script means local replay is unavailable; do not treat it as a clean proof.
			`- Third-party proof-checking attestations are allowed only as an explicit trust transformation. They must identify the provider, subject repo/commit, theorem names, observed axioms, and signature status. Untrusted attestations must not authorize builds.`
add transparency log trust provider 2026-07-03 12:09:34 +00:00			`- Transparency receipts must be verified against the exact attestation bytes, Signed Tree Head, log public key, and inclusion proof before they can authorize consequences.`
			`- Keep the Merkle log RFC 9162-style unless a new standard is deliberately adopted and documented. Do not replace it with an ad hoc hash chain.`
			`- Do not pretend ML-DSA exists. If no real ML-DSA backend is available, record the signature slot as unavailable and fail closed for policies that require both Ed25519 and ML-DSA.`
			- Provider private keys and transparency log state belong under ignored `provider/state/` or `provider/out/` paths. Do not commit local trust state.
add proof-aware crypto curriculum notebooks 2026-07-03 12:42:59 +00:00			- Curriculum notebooks are generated by `scripts/build_curriculum_notebooks.py`. Update the generator, regenerate `notebooks/`, and keep notebook code cells output-free.