mirror of
https://github.com/saymrwulf/proof-aware-crypto-tooling-agent.git
synced 2026-09-03 19:53:43 +00:00
Tier 2: - request_signature decomposed into named gates (latch, freshness, intent, policy, signer, firewall) - ledger: O(1) tail-read appends under a dedicated lock file (survives rotation rename); hash-chained segment rotation at policy ledger.rotate_at; verify-ledger walks all segments to genesis; archive tampering detected (tested) - docs/threat-model.md (attacker matrix 1-9, proven-vs-trusted, design invariants) + docs/runbook-latch.md (diagnose-first recovery) - lecture 10: executable corrupt-a-member exercise (capsule pin catches one appended byte), honest note on what the pin does NOT stop Lightweight policy engine (POLICY_DENIED wired): - policy.json: per-request/per-day amount ceilings, counterparty allow/deny lists, per-identity overrides; rules make their intent fields mandatory; daily sums from the ledger - Agent UX: - signed refusal receipts travel inside MCP errors (receipt + receipt_path in structuredContent) - airgap over MCP: request_signature signer=airgap + request_id, new airgap_pending tool; park -> list -> device answers -> complete (tested end-to-end) - all 8 tools carry readOnly/destructive annotations - sliding-window rate limiter per tool class (custody/verify/liveness); RATE_LIMITED refusal code; surface control, not ledgered warden-treasury LIVE: - treasury.py: stdlib base58, compact-u16, legacy+v0 wire parsing; every required signature quorum-verified over exact message bytes; completeness gap named in every verdict; RPC fetch uses response as bytes only - - live-quorum test: synthetic Solana tx signed with wallet key -> authentic via 4 proven forks; flipped byte -> not authentic 100 tests green (was 85). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| 00_course_map.ipynb | ||
| 01_threat_model_and_truth_boundary.ipynb | ||
| 02_claim_cards_and_risk_model.ipynb | ||
| 03_lean_replay_and_axiom_audit.ipynb | ||
| 04_proof_hygiene_and_boundaries.ipynb | ||
| 05_third_party_attestation_provider.ipynb | ||
| 06_merkle_transparency_logs.ipynb | ||
| 06a_provider_build_the_log.ipynb | ||
| 06b_agent_verify_inclusion.ipynb | ||
| 07_agent_consequences.ipynb | ||
| 08_capstone_research_program.ipynb | ||
| 09_dogfood_verified_crypto.ipynb | ||
| 10_verified_custody_wallet.ipynb | ||
| README.md | ||
PACTA Curriculum Notebooks
This directory contains a zero-to-hero teaching sequence for proof-aware cryptographic tooling.
Start with 00_course_map.ipynb, then proceed in order. The notebooks are intentionally output-free in git. Run them from the repository root or from this directory; each notebook locates the repo root and imports pacta from src/.
The course teaches:
- theorem-boundary thinking,
- claim cards and residual risk,
- Lean replay and axiom audit concepts,
- proof hygiene,
- third-party proof-check provider trust,
- RFC 9162-style Merkle transparency logs,
- the mirrored provider/agent domain split (6a: one provider builds and dogfood-signs the log; 6b: many agents verify inclusion in ~25 lines, no Lean),
- receipt-gated agent consequences (including the R4 wallet gate, now reachable),
- split-view defense: STH pinning, consistency enforcement, freshness, monitoring,
- dogfood verified cryptography and the honest hybrid post-quantum posture,
- the verified-custody wallet (warden): a quorum boundary of four proven forks, the signing firewall, and the agent-native MCP surface,
- research roadmaps from R4 evidence toward R5 assurance.
This curriculum is not financial advice, not a trading bot, and not a wallet-building guide. It is a training path for engineers and researchers who need to evaluate formal-verification-enhanced cryptographic tooling without overclaiming.