# Proof Requirements Master — All 292 Repos
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
<!-- Generated: 2026-04-04 by Claude Opus -->
<!-- Purpose: Single-source mapping of formal verification needs across entire ecosystem -->

## How to Read This Document

Each repo is categorised by **proof tier**:

| Tier | Meaning | Proof Scope |
|------|---------|-------------|
| **T1 — Critical** | Safety-critical, handles proofs/trust/crypto/data integrity | Full formal verification: typing proofs, invariant proofs, bespoke domain proofs |
| **T2 — High** | Core infrastructure, languages, compilers, build systems | Typing proofs + key invariant proofs |
| **T3 — Standard** | Application code, tools, utilities | ABI typing proofs (from template) + bespoke where warranted |
| **T4 — Light** | Documentation, config, curated lists, archives | Template typing proofs only (ABI/FFI boundary) |
| **T5 — Exempt** | Data-only, external forks, staging repos | No proofs required |

**Proof categories** per repo:
- **TP** = Typing Proofs (type soundness, type safety, bidirectional inference)
- **INV** = Invariant Proofs (state machine correctness, monotonicity, bounds)
- **SEC** = Security Proofs (crypto correctness, injection freedom, access control)
- **CONC** = Concurrency Proofs (linearizability, serializability, deadlock freedom)
- **ALG** = Algorithm Proofs (termination, correctness, complexity bounds)
- **ABI** = ABI/FFI Proofs (memory layout, pointer safety, platform compatibility)
- **DOM** = Domain-Specific Proofs (bespoke to the project's problem domain)

**Prover key**: `I2` = Idris2, `L4` = Lean4, `Ag` = Agda, `Cq` = Coq/Rocq, `TLA` = TLA+, `Iz` = Isabelle

---

## T1 — Critical (Full Formal Verification)

### echidna — Neurosymbolic Theorem Proving Platform
**Languages**: Rust (59K), Idris2 (3K), Julia, ReScript
**Existing proofs**: 17 Idris2 ABI modules (0 believe_me), 40+ Coq/Lean/Agda/Isabelle example proofs, 1K+ property tests
**Status**: Partial — core trust pipeline unproven

| # | Proof Needed | Category | Prover | Priority | File(s) |
|---|-------------|----------|--------|----------|---------|
| E1 | Confidence scoring lattice (TrustLevel forms valid partial order) | INV | L4 | P0 | `verification/confidence.rs` |
| E2 | Axiom tracker completeness (no false negatives for dangerous patterns) | SEC | I2 | P0 | `verification/axiom_tracker.rs` |
| E3 | Dispatch pipeline ordering (integrity→sandbox→verify→certs→axioms→confidence) | INV | I2 | P0 | `dispatch.rs` |
| E4 | Trust level soundness (Reject axiom → trust ≤ Level1) | INV | I2 | P0 | `verification/confidence.rs` |
| E5 | Prover dispatch compatibility (linear logic ↛ first-order ATP) | TP | I2 | P1 | `dispatch.rs`, `provers/mod.rs` |
| E6 | ProverKind discriminant injectivity (49 variants, no collisions) | TP | I2 | P1 | `provers/mod.rs` |
| E7 | GNN embedding faithfulness (structural properties preserved) | ALG | Ag | P1 | `gnn/graph.rs` |
| E8 | VQL-UT query safety (injection-free, type-safe at ABI boundary) | SEC | I2 | P1 | `vql_ut.rs` |
| E9 | Proof composition soundness (cross-prover sub-proof combination) | DOM | Ag | P2 | `verification/portfolio.rs` |
| E10 | Pareto frontier maximality (no dominated point remains) | ALG | L4 | P2 | `verification/pareto.rs` |
| E11 | SHAKE3-512/BLAKE3 integrity (solver binary verification soundness) | SEC | L4 | P2 | `integrity/solver_integrity.rs` |
| E12 | ProofState serialization losslessness (JSON roundtrip) | INV | I2 | P2 | `core.rs` |
| E13 | Portfolio cross-checking (disagreement detection completeness) | ALG | L4 | P2 | `verification/portfolio.rs` |

### verisimdb — Cross-Modal Consistency Engine
**Languages**: Rust (49K), Elixir (186K), ReScript (7K), Idris2 (2K)
**Existing proofs**: Idris2 ABI (3 files), ReScript VQL type system (11 proof types), formal semantics docs
**Status**: Partial — octad invariant and Raft consensus unproven

| # | Proof Needed | Category | Prover | Priority | File(s) |
|---|-------------|----------|--------|----------|---------|
| V1 | Octad coherence invariant (8 modalities mutually consistent post-operation) | INV | I2 | P0 | `verisim-octad/src/store.rs` |
| V2 | VQL type inference soundness (bidirectional inference correct) | TP | Cq/L4 | P0 | `src/vql/VQLBidir.res` |
| V3 | VQL subtyping transitivity + decidability | TP | L4 | P0 | `src/vql/VQLSubtyping.res` |
| V4 | Raft consensus safety (no log divergence after commit) | CONC | L4 | P0 | `src/registry/KRaftCluster.res` |
| V5 | Transaction atomicity (all-or-nothing across 8 modalities) | CONC | TLA | P0 | `verisim-octad/src/transaction.rs` |
| V6 | WAL integrity (CRC, replay idempotence, segment ordering) | INV | L4 | P1 | `verisim-wal/src/` |
| V7 | Provenance chain immutability (hash chain, monotonic timestamps) | SEC | Ag | P1 | `verisim-provenance/src/lib.rs` |
| V8 | Drift metric correctness (detection algorithm numerical bounds) | ALG | Iz | P1 | `verisim-drift/src/calculator.rs` |
| V9 | Normalizer conflict resolution determinism | ALG | TLA | P2 | `verisim-normalizer/src/lib.rs` |
| V10 | Transaction serializability under concurrent access | CONC | TLA | P2 | `verisim-octad/src/transaction.rs` |
| V11 | Connector type safety (eliminate Obj.magic JSON casts) | TP | I2 | P2 | `connectors/clients/` |
| V12 | FFI pointer validity + memory ownership | ABI | I2 | P2 | `src/abi/` |

### hypatia — Neurosymbolic CI/CD Intelligence
**Languages**: Elixir (8K+), Rust (3K+), Idris2 (1K), Zig, Logtalk
**Existing proofs**: Idris2 ABI + FFI return type proofs, pipeline state machine (ValidTransition GADT)
**Status**: ~30% — safety triangle, neural networks, learning loop unproven

| # | Proof Needed | Category | Prover | Priority | File(s) |
|---|-------------|----------|--------|----------|---------|
| H1 | Confidence bounds (0.0 ≤ x ≤ 1.0 invariant, never violated) | INV | I2 | P0 | `src/abi/Types.idr` |
| H2 | Dispatch strategy monotonicity (confidence→strategy mapping) | INV | I2 | P0 | `lib/fleet_dispatcher.ex` |
| H3 | Safety triangle ordering (Eliminate > Substitute > Control always) | INV | I2 | P0 | `lib/triangle_router.ex` |
| H4 | Rate limit enforcement (window counters never exceed bounds) | INV | L4 | P0 | `lib/safety/rate_limiter.ex` |
| H5 | Quarantine trigger exclusivity + release time correctness | INV | I2 | P1 | `lib/safety/quarantine.ex` |
| H6 | Outcome log monotonicity (timestamps strictly increasing) | INV | Ag | P1 | `lib/outcome_tracker.ex` |
| H7 | Bayesian confidence update soundness (posterior validity) | ALG | L4 | P1 | `lib/outcome_tracker.ex` |
| H8 | Kin gate atomicity (repo locks prevent concurrent bot actions) | CONC | TLA | P1 | `lib/kin/gate.ex` |
| H9 | Neural consensus aggregation soundness (8 networks → confidence) | ALG | Ag | P2 | `lib/neural/coordinator.ex` |
| H10 | VQL query injection freedom | SEC | I2 | P2 | `lib/vql/client.ex` |
| H11 | Batch rollback completeness (all dispatches revertible) | INV | L4 | P2 | `lib/safety/batch_rollback.ex` |
| H12 | Cross-repo learning isolation (no confidence leakage) | INV | I2 | P2 | `lib/cross_repo_learning.ex` |

### proven — Formal Verification Library
**Languages**: Idris2
**Existing proofs**: Core library — IS the proofs
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| PR1 | All exports total (no partial functions) | TP | I2 | P0 |
| PR2 | No believe_me/assert_total/postulate | SEC | I2 | P0 |
| PR3 | SafeStateMachine transition completeness | TP | I2 | P1 |

### proven-servers — Verified Server Implementations
**Languages**: Idris2, Zig
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| PS1 | Server handler type safety (all endpoints proven) | TP | I2 | P0 |
| PS2 | ABI/FFI boundary correctness | ABI | I2 | P0 |
| PS3 | Request parsing injection freedom | SEC | I2 | P1 |

### ProvenCrypto.jl — Cryptographic Verification
**Languages**: Julia, Idris2
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| PC1 | Crypto primitive correctness (hash, sign, verify) | SEC | I2/L4 | P0 |
| PC2 | Key generation entropy bounds | SEC | L4 | P0 |
| PC3 | Protocol composition soundness | SEC | Ag | P1 |

### stapeln — Container Orchestration (Verified)
**Languages**: Rust, Idris2, Zig
**Existing proofs**: 14/26 postulates proven, crypto FIXED
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| ST1 | Remaining 12 postulates (prove or cite) | INV | I2 | P0 |
| ST2 | Container isolation correctness | SEC | I2 | P1 |
| ST3 | Image signing chain of trust | SEC | L4 | P1 |
| ST4 | Network policy enforcement | SEC | I2 | P2 |

### protocol-squisher — Protocol Translation
**Languages**: Rust (29 crates)
**Existing proofs**: 8/29 crates done (unwrap removal)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| PQ1 | Protocol translation bijectivity | ALG | L4 | P1 |
| PQ2 | Remaining 21 crates: no panics (unwrap-free) | INV | I2 | P1 |
| PQ3 | Buffer overflow freedom | SEC | I2 | P1 |

### januskey — Key Management
**Languages**: Rust
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| JK1 | Key derivation correctness | SEC | L4 | P0 |
| JK2 | Access control policy enforcement | SEC | I2 | P0 |
| JK3 | Key rotation monotonicity | INV | I2 | P1 |

### svalinn — Edge Gateway
**Languages**: Rust, Zig
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| SV1 | Request filtering soundness (no bypass) | SEC | I2 | P0 |
| SV2 | TLS termination correctness | SEC | L4 | P1 |
| SV3 | Rate limiting enforcement | INV | I2 | P1 |

---

## T1 — Critical: Next-Gen Languages (Type System Proofs Essential)

### ephapax — Linear Type Language
**Languages**: Rust (17 crates), Idris2 (17 files), Coq (3 files)
**Existing proofs**: 47 Qed / 2 Admitted in Coq. Substitution lemma is last blocker.
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| EP1 | Close 2 remaining Admitted (substitution lemma, preservation) | TP | Cq | P0 |
| EP2 | Type soundness (progress + preservation) | TP | Cq | P0 |
| EP3 | Linear resource tracking correctness | TP | I2 | P0 |
| EP4 | Region-based memory safety | SEC | I2 | P1 |
| EP5 | Affine type erasure correctness | TP | Ag | P2 |

### eclexia — Economics-as-Code
**Languages**: Rust, Idris2 (4 files), Coq (3 files, 0 Admitted), Agda (1 file)
**Existing proofs**: Type safety theorem COMPLETE. Shadow prices with 5 cited axioms.
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| EC1 | Economic optimality under general conditions (extend beyond research) | DOM | Cq | P1 |
| EC2 | Resource tracking totality (Agda) | TP | Ag | P1 |
| EC3 | Compilation correctness (source semantics = compiled semantics) | ALG | Cq | P2 |

### affinescript — Affine Type Functional Language
**Languages**: OCaml (compiler), Rust (runtime)
**Existing proofs**: NONE — critical gap despite affine type claims
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| AF1 | Type checker soundness (affine types correctly enforced) | TP | Cq | P0 |
| AF2 | Runtime memory safety (Rust runtime) | SEC | I2 | P0 |
| AF3 | Compilation preserves affine properties | TP | Cq | P1 |
| AF4 | GC-free correctness (affine types guarantee no leaks) | ALG | L4 | P2 |

### my-lang — Multi-Dialect Compiler
**Languages**: Compiler impl, Coq (Syntax.v, Typing.v)
**Existing proofs**: Under development for 4 dialects (Me, Solo, Duet, Ensemble)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| ML1 | Per-dialect type soundness (4 dialects) | TP | Cq | P0 |
| ML2 | Dialect interop type safety | TP | Cq | P1 |
| ML3 | Parser correctness | ALG | L4 | P2 |

### wokelang — Consent-Aware Programming
**Languages**: Impl, Idris2 (3 files), Coq + Lean proofs
**Existing proofs**: Multi-language (WokeLang.v, WokeLang.lean)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| WL1 | Consent model soundness (permissions never bypassed) | SEC | I2 | P0 |
| WL2 | Type system soundness | TP | Cq | P1 |
| WL3 | Runtime consent enforcement | SEC | I2 | P1 |

### betlang — Ternary Probabilistic DSL
**Languages**: Racket, Lean (1 file)
**Existing proofs**: Partial Lean, formal semantics docs
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| BL1 | Type checker soundness | TP | L4 | P1 |
| BL2 | Probability distribution correctness | ALG | L4 | P1 |
| BL3 | Ternary logic completeness | DOM | L4 | P2 |

### tangle — Formal Language
**Languages**: Impl, Lean (Tangle.lean)
**Existing proofs**: Lean formalization exists
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| TG1 | Type soundness | TP | L4 | P0 |
| TG2 | Compilation correctness | ALG | L4 | P1 |

### phronesis — Consensus/Crypto Language
**Languages**: Impl, Agda + Coq + Lean4 + TLA+
**Existing proofs**: Multi-formalism academic proofs
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| PH1 | Consensus protocol safety (TLA+ model checking) | CONC | TLA | P0 |
| PH2 | Crypto primitive correctness | SEC | L4 | P0 |
| PH3 | Type system soundness | TP | Cq | P1 |

### oblibeny — Constraint Language
**Languages**: Impl, Idris2 (2 files), Lean (1 file)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| OB1 | Constraint solver termination | ALG | L4 | P1 |
| OB2 | Type system soundness | TP | L4 | P1 |

### julia-the-viper — Julia Security Extension
**Languages**: Julia, Idris2 (1 file), Lean (5 files)
**Existing proofs**: Active Lean security proofs
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| JV1 | Security property enforcement | SEC | L4 | P0 |
| JV2 | Sandboxing correctness | SEC | I2 | P1 |

### anvomidav — Language Implementation
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| AV1 | Type system soundness | TP | L4 | P1 |
| AV2 | ABI correctness | ABI | I2 | P2 |

### error-lang — Error Handling Language
**Existing proofs**: 1 Idris2 file
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| EL1 | Error propagation soundness | TP | I2 | P1 |
| EL2 | Recovery strategy completeness | ALG | L4 | P2 |

---

## T2 — High (Typing Proofs + Key Invariants)

### 007-lang — Private Language (PRIVATE — Triple Confirm)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| 07-1 | Type checker soundness (Five Facets) | TP | I2 | P0 |
| 07-2 | Hermeneutic semantics well-foundedness | DOM | Ag | P1 |
| 07-3 | Algebraic dispatch correctness | ALG | L4 | P1 |
| 07-4 | Dual AST safety | TP | I2 | P1 |

### typed-wasm — Typed WebAssembly (12 Levels)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| TW1 | Per-level type soundness (12 levels) | TP | Cq | P0 |
| TW2 | WASM validation correctness | ALG | L4 | P1 |
| TW3 | Memory safety per level | SEC | I2 | P1 |

### panll — Panel Management (108 panels, ~686 modules)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| PL1 | TEA framework type safety | TP | I2 | P1 |
| PL2 | Panel lifecycle state machine | INV | I2 | P1 |
| PL3 | Workspace layer isolation | SEC | I2 | P2 |

### gossamer — Window Management System
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| GS1 | Window state machine correctness | INV | I2 | P1 |
| GS2 | IPC handler type safety (25 handlers) | TP | I2 | P1 |
| GS3 | Groove protocol compliance | INV | I2 | P2 |

### typell — Type-Level Language
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| TL1 | Type system soundness (meta-level) | TP | Ag | P0 |
| TL2 | Compilation correctness | ALG | L4 | P1 |

### boj-server — MCP Server (95 cartridges)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| BJ1 | Cartridge dispatch type safety | TP | I2 | P1 |
| BJ2 | Auth/credential handling | SEC | I2 | P1 |
| BJ3 | API contract compliance (95 cartridges) | INV | I2 | P2 |

### panic-attacker — Security Scanner
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| PA1 | Pattern detection completeness (no false negatives for critical) | ALG | I2 | P1 |
| PA2 | Output format correctness | INV | I2 | P2 |

### gitbot-fleet — Bot Orchestration
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| GF1 | Bot action isolation (no cross-contamination) | CONC | TLA | P1 |
| GF2 | Confidence threshold enforcement | INV | I2 | P1 |

### statistease — Statistical Engine (478 tests)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| SE1 | Statistical algorithm correctness (numerical bounds) | ALG | Iz | P1 |
| SE2 | VeriSimDB query type safety | TP | I2 | P2 |

### idaptik — Main Game (AGPL, Co-developed)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| ID1 | Game state machine correctness | INV | I2 | P1 |
| ID2 | ABI/FFI boundary (ReScript ↔ Rust) | ABI | I2 | P1 |
| ID3 | Character system invariants (Jessica, Q, Moletaire) | DOM | I2 | P2 |

### the-nash-equilibrium — Strategy Game (AGPL)
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| NE1 | Game balance proofs (equilibrium existence) | DOM | L4 | P2 |
| NE2 | State machine correctness | INV | I2 | P2 |

### reposystem — Repository Management
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| RS1 | TUI state machine (Rust/ratatui) | INV | I2 | P1 |
| RS2 | SPARK integration correctness | SEC | I2 | P1 |

### groove-browser-harness — Groove Browser Extension
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| GB1 | Groove protocol compliance | INV | I2 | P1 |
| GB2 | Message integrity | SEC | I2 | P2 |

### conflow — CI/CD Pipeline Engine
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| CF1 | Pipeline DAG acyclicity | ALG | L4 | P1 |
| CF2 | Step execution ordering | INV | I2 | P1 |

### burble — Voice/Video Platform
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| BU1 | WebRTC signal integrity | SEC | I2 | P1 |
| BU2 | DTLS/SRTP key exchange | SEC | L4 | P1 |
| BU3 | Topology state machine | INV | I2 | P2 |

### cloudguard-cli / cloudguard-server — Cloud Security
| # | Proof Needed | Category | Prover | Priority |
|---|-------------|----------|--------|----------|
| CG1 | Security policy enforcement (no bypass) | SEC | I2 | P0 |
| CG2 | Credential handling safety | SEC | I2 | P1 |

---

## T3 — Standard (ABI Typing Proofs + Bespoke Where Warranted)

### Infrastructure & Tooling
| Repo | Proofs Needed | Prover |
|------|--------------|--------|
| `standards` | ABI + standards compliance invariants | I2 |
| `developer-ecosystem` | ABI per satellite | I2 |
| `asdf-tool-plugins` | Plugin interface type safety | I2 |
| `maa-framework` | ABI + absolute-zero integration | I2 |
| `nickel-augmentation` | ABI + Nickel contract proofs | I2/L4 |
| `filesoup` | Plugin API type safety + ABI | I2 |
| `ambientops` | ABI + container orchestration | I2 |
| `patallm-gallery` | ABI per gallery item | I2 |

### -iser Ecosystem (29 repos — all need ABI typing proofs)
| Repo | Proofs Needed | Prover |
|------|--------------|--------|
| `a2mliser` | ABI + A2ML validation correctness | I2 |
| `k9iser` | ABI + K9 validation correctness | I2 |
| `idrisiser` | ABI + Idris2 tooling correctness | I2 |
| `iseriser` | ABI + meta-iser correctness | I2 |
| `affinescriptiser` | ABI | I2 |
| `alloyiser` | ABI | I2 |
| `anvomidaviser` | ABI | I2 |
| `atsiser` | ABI | I2 |
| `betlangiser` | ABI | I2 |
| `bqniser` | ABI | I2 |
| `chapeliser` | ABI | I2 |
| `dafniser` | ABI | I2 |
| `eclexiaiser` | ABI | I2 |
| `ephapaxiser` | ABI | I2 |
| `futharkiser` | ABI | I2 |
| `halideiser` | ABI | I2 |
| `julianiser` | ABI | I2 |
| `lustreiser` | ABI | I2 |
| `mylangiser` | ABI | I2 |
| `nimiser` | ABI | I2 |
| `oblibeniser` | ABI | I2 |
| `otpiser` | ABI | I2 |
| `phronesiser` | ABI | I2 |
| `ponyiser` | ABI | I2 |
| `tlaiser` | ABI | I2 |
| `typedqliser` | ABI | I2 |
| `verisimiser` | ABI | I2 |
| `wokelangiser` | ABI | I2 |

### A2ML/K9 Ecosystem
| Repo | Proofs Needed | Prover |
|------|--------------|--------|
| `a2ml-rs` | ABI + parser correctness | I2/L4 |
| `a2ml-deno` | ABI + validation | I2 |
| `a2ml_ex` | ABI + Elixir NIF safety | I2 |
| `a2ml_gleam` | ABI | I2 |
| `a2ml-haskell` | ABI + parser correctness | L4 |
| `a2ml-validate-action` | ABI + CI correctness | I2 |
| `a2ml-pre-commit` | ABI | I2 |
| `k9-rs` | ABI + parser correctness | I2/L4 |
| `k9-deno` | ABI | I2 |
| `k9_ex` | ABI | I2 |
| `k9_gleam` | ABI | I2 |
| `k9-haskell` | ABI | I2 |
| `k9-validate-action` | ABI | I2 |
| `k9-pre-commit` | ABI | I2 |
| `tree-sitter-a2ml` | Grammar correctness | L4 |
| `tree-sitter-k9` | Grammar correctness | L4 |
| `pandoc-a2ml` | ABI + format preservation | I2 |
| `pandoc-k9` | ABI + format preservation | I2 |
| `metadata-grammar` | Grammar completeness | L4 |

### Julia Packages (19 repos)
| Repo | Proofs Needed | Prover |
|------|--------------|--------|
| `Hyperpolymath.jl` | ABI | I2 |
| `AcceleratorGate.jl` | ABI + gate logic | I2 |
| `Axiology.jl` | ABI + value theory proofs | I2/L4 |
| `Axiom.jl` | ABI + axiom system consistency | L4 |
| `BowtieRisk.jl` | ABI + risk calculation bounds | I2 |
| `Causals.jl` | ABI + causal inference correctness | L4 |
| `Cladistics.jl` | ABI + tree construction | I2 |
| `Cliodynamics.jl` | ABI | I2 |
| `Cliometrics.jl` | ABI | I2 |
| `Exnovation.jl` | ABI | I2 |
| `FirmwareAudit.jl` | ABI + audit completeness | I2 |
| `HackenbushGames.jl` | ABI + game theory proofs | L4 |
| `HardwareResilience.jl` | ABI | I2 |
| `InvestigativeJournalist.jl` | ABI | I2 |
| `JuliaKids.jl` | ABI | I2 |
| `KnotTheory.jl` | ABI + knot invariant proofs | L4/Ag |
| `LowLevel.jl` | ABI + memory safety | I2 |
| `MacroPower.jl` | ABI + macro hygiene | I2 |
| `MinixSDK.jl` | ABI | I2 |

### Web / Application Repos
| Repo | Proofs Needed | Prover |
|------|--------------|--------|
| `rescript-tea` | ABI + TEA model correctness | I2 |
| `rescript-vite` | ABI | I2 |
| `rescript-dom-mounter` | ABI + DOM safety | I2 |
| `rescript-evangeliser` | ABI | I2 |
| `nafa-app` | ABI | I2 |
| `aerie` | ABI | I2 |
| `project-wharf` | ABI | I2 |
| `lcb-website` | ABI | I2 |

### Security / Ops Tools
| Repo | Proofs Needed | Prover |
|------|--------------|--------|
| `cloudflare-dns-terraform` | ABI + DNS record type safety | I2 |
| `http-capability-gateway` | ABI + capability model proofs | I2/L4 |
| `explicit-trust-plane` | ABI + trust model correctness | I2 |
| `sdp-hkdf-deployment` | ABI + HKDF correctness | L4 |
| `safe-brute-force` | ABI + rate limiting bounds | I2 |
| `reasonably-good-token-vault` | ABI + token lifecycle | I2 |
| `sanctify-php` | ABI + sanitization completeness | I2 |
| `php-aegis` | ABI + input validation | I2 |
| `pimcore-fortress` | ABI | I2 |

### Other T3 Repos
| Repo | Proofs Needed | Prover |
|------|--------------|--------|
| `flat-mate` | ABI + file matching correctness | I2 |
| `flatracoon` | ABI | I2 |
| `cookie-rebound` | ABI + privacy property | I2 |
| `docmatrix` | ABI + document transformation | I2 |
| `docudactyl` | ABI | I2 |
| `dictask` | ABI | I2 |
| `raze-tui` | ABI + TUI state machine | I2 |
| `seamstress` | ABI + stitching correctness | I2 |
| `supernorma` | ABI + normalization proofs | I2/L4 |
| `valence-shell` | ABI + shell safety | I2 |
| `vexometer` | ABI + metric correctness | I2 |
| `vex-tools` | ABI | I2 |
| `vql-ut` | ABI + VQL query safety | I2 |
| `v-graphql` | ABI + schema validation | I2 |
| `v-grpc` | ABI + proto compliance | I2 |
| `v-rest` | ABI + REST contract | I2 |
| `kea` | ABI | I2 |
| `laminar` | ABI + flow control | I2 |
| `laniakea` | ABI | I2 |
| `linguist` | ABI + language detection | I2 |
| `neurophone` | ABI | I2 |
| `ochrance` | ABI + protection model | I2 |
| `ochrance-framework` | ABI + framework safety | I2 |
| `odds-and-sods-package-manager` | ABI + package resolution | I2/L4 |
| `polyglot-formalisms-elixir` | ABI + formalism correctness | I2 |
| `polyglot-formalisms-gleam` | ABI | I2 |
| `PolyglotFormalisms.jl` | ABI | I2 |
| `polyglot-i18n` | ABI + i18n completeness | I2 |
| `polysafe-gitfixer` | ABI + git safety | I2 |
| `boj-server` | ABI | I2 |
| `rrecord-verity` | ABI + record validation | I2 |
| `resource-record-fluctuator` | ABI + DNS correctness | I2 |
| `format-registrations` | ABI | I2 |
| `formatrix-docs` | ABI | I2 |
| `universal-project-manager` | ABI + project model | I2 |
| `universal-language-server-plugin` | ABI + LSP compliance | I2 |
| `universal-chat-extractor` | ABI | I2 |
| `universal-extension-format` | ABI + format correctness | I2 |
| `unified-dataset-vocab` | ABI + vocab consistency | I2 |
| `v3-templater` | ABI + template correctness | I2 |
| `ubicity` | ABI | I2 |
| `tropical-resource-typing` | ABI + tropical algebra proofs | L4 |
| `tma-mark2` | ABI | I2 |
| `thejeffparadox` | ABI | I2 |
| `snapcreate` | ABI | I2 |
| `squeakwell` | ABI | I2 |
| `session-sentinel` | ABI + session lifecycle | I2 |
| `robodog-ecm` | ABI | I2 |
| `robot-vacuum-cleaner` | ABI | I2 |
| `rpa-elysium` | ABI + RPA safety | I2 |
| `refugia` | ABI | I2 |
| `preference-injector` | ABI + injection safety | I2 |
| `presswerk` | ABI | I2 |
| `neural-foundations` | ABI + NN property proofs | L4/Ag |
| `modshells` | ABI + shell composition | I2 |
| `megadog` | ABI | I2 |
| `kaldor-iiot` | ABI + IIoT safety | I2 |
| `kategoria` | ABI + category theory | L4/Ag |
| `ipfs-overlay` | ABI + content addressing | I2 |
| `ipv6-tools` | ABI + IPv6 format correctness | I2 |
| `intsoc-transactor` | ABI + transaction safety | I2 |
| `infrastructure-automation` | ABI | I2 |
| `i-human` | ABI | I2 |
| `hybrid-automation-router` | ABI + routing correctness | I2 |
| `hesiod-dns-map` | ABI + DNS correctness | I2 |
| `heterogenous-mobile-computing` | ABI | I2 |
| `grim-repo` | ABI | I2 |
| `gv-clade-index` | ABI + clade correctness | I2 |
| `git-reticulator` | ABI + git operation safety | I2 |
| `git-scripts` | ABI | I2 |
| `fireflag` | ABI + feature flag safety | I2 |
| `feedback-o-tron` | ABI | I2 |
| `excel-economic-numbers-tool` | ABI + numerical accuracy | I2 |
| `ensaid-spec` | ABI + spec conformance | I2 |
| `elixir-mcp-server` | ABI + MCP compliance | I2 |
| `empty-linter` | ABI + lint rule correctness | I2 |
| `double-track-browser` | ABI | I2 |
| `dotmatrix-fileprinter` | ABI | I2 |
| `defiant` | ABI | I2 |
| `conative-gating` | ABI + gating correctness | I2 |
| `cloud-sync-tuner` | ABI | I2 |
| `civic-connect` | ABI | I2 |
| `chimichanga` | ABI | I2 |
| `checky-monkey` | ABI + check correctness | I2 |
| `candy-crash` | ABI | I2 |
| `bunsenite` | ABI | I2 |
| `branch-newspaper` | ABI | I2 |
| `blocky-writer` | ABI | I2 |
| `blue-screen-of-app` | ABI | I2 |
| `bofig` | ABI + config validation | I2 |
| `befunge93-vault-cracker` | ABI | I2 |
| `anamnesis` | ABI | I2 |
| `aspasia` | ABI | I2 |
| `academic-workflow-suite` | ABI | I2 |
| `accessibility-everywhere` | ABI | I2 |
| `ffmpeg-ffi` | ABI + FFI correctness (critical for media) | I2 |
| `live-files` | ABI + file watch correctness | I2 |
| `misinformation-defence-platform` | ABI + detection correctness | I2/L4 |
| `proof-of-work` | ABI + PoW verification | L4 |
| `dicti0nary-attack` | ABI + CTF safety | I2 |
| `voyage-enterprise-decision-system` | ABI + decision model proofs | L4 |
| `nextgen-databases` | ABI per sub-database | I2 |
| `social-media-tools` | ABI | I2 |
| `ssg-collection` | ABI | I2 |
| `wordpress-tools` | ABI | I2 |
| `zotero-tools` | ABI | I2 |
| `zerostep` | ABI | I2 |
| `zerotier-k8s-link` | ABI + network safety | I2 |
| `twingate-helm-deploy` | ABI | I2 |
| `thunderbird-template-reloaded` | ABI | I2 |

---

## T4 — Light (Template Typing Proofs Only)

| Repo | Notes |
|------|-------|
| `awesome-idris2` | Curated list — template ABI only |
| `awesome-mcp-servers` | Curated list — template ABI only |
| `awesome-nickel` | Curated list — template ABI only |
| `blog-drafts` | Content — template ABI only |
| `hyperpolymath` | GitHub profile — template ABI only |
| `hyperpolymath.github.io` | Static site — template ABI only |
| `HyperpolymathRegistry` | Julia registry — template ABI only |
| `homebrew-tap` | Homebrew formulae — template ABI only |
| `im-docs` | Documentation — template ABI only |
| `manifesto` | Policy document — template ABI only |
| `palimpsest-license` | License text — template ABI only |
| `palimpsest-plasma` | License tooling — template ABI only |
| `vscode-a2ml` | VS Code ext — template ABI only |
| `vscode-k9` | VS Code ext — template ABI only |
| `a2ml-showcase` | Demo — template ABI only |
| `k9-showcase` | Demo — template ABI only |
| `squisher-corpus` | Test corpus — template ABI only |
| `nexia-list` | Curated list — template ABI only |
| `no-nonsense-nntps` | Docs — template ABI only |
| `boinc-boinc` | External integration — template ABI only |

---

## T5 — Exempt (No Proofs Required)

| Repo | Reason |
|------|--------|
| `verisimdb-data` | Data-only (git-backed flat files) |
| `idaptik-rescript13-staging` | Temporary staging repo |
| `007-lang-private-docs` | Documentation only |
| `007` | Meta/config repo |
| `7-tentacles` | Educational scheme, not a language |
| `HOL` | External fork (Higher Order Logic) |
| `rescript` | External fork |
| `pow-the-game` | Game assets |
| `games & trivia` | Game collection |
| `airborne-submarine-squadron` | Game (AGPL, separate concerns) |
| `phantom-metal-taste` | Game/creative |
| `zatty` | Utility |
| `interpreter-mk2` | Experimental |
| `extensions` | Extension collection |
| `hyperpolymath-sovereign-registry` | Registry data |
| `julia-ecosystem` | Ecosystem meta |
| `mcp-servers` | Config/integration |

---

## Summary Statistics

| Tier | Count | Proof Items | Primary Prover |
|------|-------|-------------|----------------|
| T1 Critical | ~25 repos | ~120 proofs | I2, L4, Cq, Ag |
| T2 High | ~20 repos | ~45 proofs | I2, L4, TLA |
| T3 Standard | ~210 repos | ~210 ABI proofs + ~60 bespoke | I2 |
| T4 Light | ~20 repos | ~20 template proofs | I2 |
| T5 Exempt | ~17 repos | 0 | — |
| **Total** | **292 repos** | **~455 proofs** | **Idris2 dominant** |

## Standard Proof Files Per Repo

Every RSR-compliant repo MUST have:
1. `PROOF-NEEDS.md` — What proofs are needed (from this master list)
2. `PROOF-STATUS.md` — What proofs are done, in progress, or blocked
3. `verification/proofs/` — Actual proof files organised by prover

Templates for these files live in `rsr-template-repo`.

---
*Generated 2026-04-04. Authoritative source: `~/Desktop/PROOF-REQUIREMENTS-MASTER.md`*
*Update this document when proof requirements change. Per-repo PROOF-NEEDS.md files are derived from this master.*
