proof-aware-crypto-tooling-agent

pacta is a local CLI prototype for interpreting formal-verification evidence in cryptographic tooling. It is not a trading bot, does not move funds, and does not make financial decisions.

The immediate corpus is the saymrwulf/*-verified family of repositories. The shipped Lean files are treated as the verification artifact. This project intentionally does not run Charon, Aeneas, extraction, or Rust-to-Lean regeneration.

Purpose

An autonomous economic agent needs to answer a narrow question before trusting infrastructure:

Does this theorem cover the exact code path that will protect my funds?

pacta helps answer that by replaying pure Lean checks where possible, auditing axioms and proof hygiene, generating machine-readable claim cards, and assigning residual-risk classifications with explicit exclusions.

macOS / Apple Silicon

The prototype is written for Python 3.11+ and macOS on Apple Silicon. It does not assume GNU coreutils, Linux free, Linux taskset, GNU timeout, Docker, Nix, or x86_64.

Lean tooling is detected with shutil.which("lean") and shutil.which("lake"). If neither is available, pacta reports clear diagnostics and still supports offline claim-card generation and static hygiene scans.

Install

python3 -m venv .venv
. .venv/bin/activate
python -m pip install -e ".[dev]"

PyYAML is optional. Without it, pacta can still read the included simple YAML examples and JSON-compatible .yaml files.

Commands

python -m pacta --help
pacta scan --config examples/repos.yaml
pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified
pacta claims --config examples/repos.yaml --repo-name dalek-ed25519-verified --offline-fixture --out claims.yaml
pacta audit --repo ./repos/dalek-ed25519-verified
pacta lean-check --repo ./repos/dalek-ed25519-verified
pacta report --claims claims.yaml --out report.md
pacta score --claims claims.yaml
pacta receipt-verify --attestation provider/out/dalek-ed25519.attestation.yaml --receipt provider/out/dalek-ed25519.receipt.yaml --log-public-key provider/state/local-provider/provider.ed25519.pub
pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --offline-fixture --action build-library
pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --clone --run-axioms --action build-library --artifact-dir artifacts-live
pacta agent --claims claims.yaml --action build-wallet-demo
pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --attestation examples/dalek-ed25519.attestation.yaml --trust-attestation-provider example-proof-checker.invalid --action build-library

Curriculum Notebooks

The notebooks/ directory contains a zero-to-hero teaching sequence for undergraduate students moving toward research-grade assurance engineering:

• 00_course_map.ipynb: course structure, prerequisites, assessment model, references.
• 01_threat_model_and_truth_boundary.ipynb: threat model, theorem boundaries, exclusions.
• 02_claim_cards_and_risk_model.ipynb: claim card schema and R0-R5 scoring.
• 03_lean_replay_and_axiom_audit.ipynb: replay versus transpilation, Lean invocation, axiom audits.
• 04_proof_hygiene_and_boundaries.ipynb: sorry, local axioms, trivial targets, manifest coverage.
• 05_third_party_attestation_provider.ipynb: provider trust transformation and signed attestations.
• 06_merkle_transparency_logs.ipynb: RFC 9162-style Merkle proofs, STHs, Ed25519/ML-DSA policy.
• 07_agent_consequences.ipynb: receipt-gated artifact builds and wallet-denial policy.
• 08_capstone_research_program.ipynb: research roadmap from R3 toward R4/R5.

The notebooks are committed without execution output. They can be opened in Jupyter, VS Code, or any notebook reader. They import pacta directly from this repository and avoid external notebook-only dependencies.

Consequence Engine

pacta agent turns evaluation into an operational consequence.

• build-library requires R3 by default. It builds a small Rust proof-gated component capsule under artifacts/. The capsule embeds the claim card and exposes whether downstream automation may use the component for lower-layer cryptographic code only.
• build-wallet-demo requires R4. An R3 Ed25519 arithmetic claim will refuse this action and write a machine-readable denial artifact instead of building a wallet.

This is intentional. Arithmetic proof evidence can authorize a constrained lower-layer library decision, but it must not contaminate wallet, transaction, custody, or trading-agent risk scoring.

In live mode, --clone --run-axioms downloads the configured repository, replays the local Lean checks, runs the axiom audit, writes claims.yaml and report.md, and only builds the capsule if the resulting score satisfies the policy threshold. Failed replay is a hard consequence: no artifact is built.

Verifier Bootstrap

Some verified repositories rely on a pinned Aeneas Lean project, usually exposed by an environment script such as ~/aeneas-toolchain/env.sh. pacta can use that environment without running extraction:

pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified
pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --clone --run-axioms --action build-library

The configured defaults are:

• env_script: ~/aeneas-toolchain/env.sh
• lean_project_dir: $AENEAS_HOME/backends/lean

If those are missing, the result is R0 for local replay because this machine lacks verifier capability. That is different from saying the theorem is false. It means the agent cannot trust the repository from local machine-checked evidence yet.

Third-Party Attestation

For agents that should not build the full Lean/Aeneas environment locally, pacta also supports an attestation lane. A specialized proof-checking service can replay the proofs in its own controlled environment and publish a certificate describing:

• repository URL and commit,
• theorem/certificate names,
• observed axioms,
• Lean/toolchain environment,
• service identity and signature metadata.

The agent can consume that certificate only when the provider is explicitly trusted:

pacta agent --config examples/repos.yaml \
  --repo-name dalek-ed25519-verified \
  --attestation examples/dalek-ed25519.attestation.yaml \
  --trust-attestation-provider example-proof-checker.invalid \
  --allow-unsigned-attestation \
  --action build-library

This changes the trusted base. The agent is no longer trusting local Lean replay; it is trusting the proof-checking service, its environment, signing key custody, and log retention. Without an explicitly trusted provider, attestation evidence scores R0.

The included examples/dalek-ed25519.attestation.yaml is an unsigned schema/demo fixture and requires --allow-unsigned-attestation. Real provider certificates should be signed and consumed with --attestation-public-key.

Transparency-Logged Attestations

Standalone signatures prove who signed an attestation, but they do not make the provider accountable for equivocation or silent replacement. The nested provider can also append attestations to a local RFC 9162-style Merkle transparency log and issue inclusion receipts.

The log uses:

• RFC9162_SHA256 Merkle leaf/node hashing with 0x00 leaf and 0x01 node domain separation.
• Signed Tree Heads over canonical JSON tree-head payloads.
• OpenSSL Ed25519 signatures today.
• An explicit ML-DSA-65 / FIPS 204 signature slot that is unavailable unless the host has a real backend. If an agent policy requires both signatures, verification fails closed.

Example:

PYTHONPATH=src:provider/src python -m pacta_provider log-init \
  --log-dir provider/state/transparency-log \
  --provider local-pacta-provider \
  --public-key provider/state/local-provider/provider.ed25519.pub

PYTHONPATH=src:provider/src python -m pacta_provider log-append \
  --log-dir provider/state/transparency-log \
  --attestation provider/out/dalek-ed25519.attestation.yaml \
  --private-key provider/state/local-provider/provider.ed25519.key \
  --public-key provider/state/local-provider/provider.ed25519.pub \
  --out provider/out/dalek-ed25519.receipt.yaml

pacta receipt-verify \
  --attestation provider/out/dalek-ed25519.attestation.yaml \
  --receipt provider/out/dalek-ed25519.receipt.yaml \
  --log-public-key provider/state/local-provider/provider.ed25519.pub

Agents can require the receipt before building anything:

pacta agent \
  --config examples/repos.yaml \
  --repo-name dalek-ed25519-verified \
  --repo repos/dalek-ed25519-verified \
  --attestation provider/out/dalek-ed25519.attestation.yaml \
  --trust-attestation-provider local-pacta-provider \
  --attestation-public-key provider/state/local-provider/provider.ed25519.pub \
  --transparency-receipt provider/out/dalek-ed25519.receipt.yaml \
  --transparency-log-public-key provider/state/local-provider/provider.ed25519.pub \
  --require-transparency-receipt \
  --action build-library

To demand post-quantum log signatures as well:

pacta receipt-verify \
  --attestation provider/out/dalek-ed25519.attestation.yaml \
  --receipt provider/out/dalek-ed25519.receipt.yaml \
  --log-public-key provider/state/local-provider/provider.ed25519.pub \
  --require-signatures both

On a host without ML-DSA support, that command should fail. That is intentional. The system records the missing capability as a deployment blocker instead of treating the Ed25519 signature as quantum-robust.

Nested Proof-Check Provider

This repository includes a nested provider prototype under provider/. It searches read-only under your home/GitClone tree for reusable Lean/Aeneas infrastructure, runs the proof replay, signs the result with OpenSSL Ed25519, and emits an attestation.

PYTHONPATH=src:provider/src python -m pacta_provider discover --root ~/GitClone
PYTHONPATH=src:provider/src python -m pacta_provider init-key --key-dir provider/state/local-provider
PYTHONPATH=src:provider/src python -m pacta_provider check \
  --config examples/repos.yaml \
  --repo-name dalek-ed25519-verified \
  --repo repos/dalek-ed25519-verified \
  --provider local-pacta-provider \
  --private-key provider/state/local-provider/provider.ed25519.key \
  --public-key provider/state/local-provider/provider.ed25519.pub \
  --env-script /path/to/aeneas-toolchain/env.sh \
  --lean-project-dir '$AENEAS_HOME/backends/lean' \
  --out provider/out/dalek-ed25519.attestation.yaml

pacta agent \
  --config examples/repos.yaml \
  --repo-name dalek-ed25519-verified \
  --attestation provider/out/dalek-ed25519.attestation.yaml \
  --trust-attestation-provider local-pacta-provider \
  --attestation-public-key provider/state/local-provider/provider.ed25519.pub \
  --transparency-receipt provider/out/dalek-ed25519.receipt.yaml \
  --transparency-log-public-key provider/state/local-provider/provider.ed25519.pub \
  --require-transparency-receipt \
  --action build-library

This is the intended trust transformation: local agents can avoid constructing the full verifier environment, but they must explicitly trust the provider identity and verification key.

Truth Boundary

The Ed25519 repositories should not be marketed as fully verified wallets or fully verified Ed25519 end-to-end. The strongest current claim is lower-layer and theorem-bound:

For selected curve25519-dalek / Solana-Ed25519-family Rust code paths already transpiled into Lean, the repositories contain Lean-checked certificates for field arithmetic over F_p, p = 2^255 - 19, and complete twisted Edwards point-operation laws, under explicit invariants and backend constraints.

pacta treats these as out of scope unless separately proven:

• Full EdDSA signature verification.
• Complete Scalar52 arithmetic.
• SHA-512.
• Encoding, decoding, and canonicality.
• Rust compiler correctness.
• Charon/Aeneas translation faithfulness.
• Side-channel resistance.
• SIMD, AVX, hardware, zkVM, accelerator, or syscall paths.
• Wallet policy, transaction construction, RPC, chain, oracle, market, and LLM decision safety.

Risk Levels

• R0: Unknown or untrusted. No usable evidence.
• R1: Tests, audits, or informal claims only.
• R2: Formal model exists, but it is incomplete, weakly tied to production code, or major proof gaps remain.
• R3: A specific lower-layer implementation artifact is Lean-checked for a specific backend and theorem boundary.
• R4: End-to-end primitive proof covers public API, parsing/encoding, scalar arithmetic, hashing interface, signature equation, rejection rules, and implementation boundary.
• R5: R4 plus reproducible production builds, compiler/build assurance, side-channel analysis, hardware/KMS/MPC integration, and operational controls.

Expected first-pass classification: Ed25519 field plus Edwards point arithmetic can reach R3 if configured certificates compile and the axiom audit is clean. Full Ed25519 signature verification remains R2 or lower unless complete scalar, encoding, hashing, and signature certificates exist.