Remove template-only ABI files that falsely implied formal verification

Template Idris2 ABI files (Types.idr, Layout.idr, Foreign.idr) contained
only RSR template scaffolding with unresolved placeholders and no
domain-specific proofs. Removed to prevent false impression of formal
verification coverage.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -0,0 +1,33 @@
+# PROOF-NEEDS.md — maa-framework
+
+## Current State
+
+- **src/abi/*.idr**: NO
+- **Dangerous patterns**: 1 `Admitted` in `proofs/coq/lambda/LambdaCNO.v` (y_not_cno theorem)
+- **LOC**: ~22,700 (Rust + Coq)
+- **ABI layer**: Missing
+- **Existing proofs**: Coq proofs for lambda CNO (3/4 proven), quantum mechanics exactness
+
+## What Needs Proving
+
+| Component | What | Why |
+|-----------|------|-----|
+| Y combinator non-CNO (y_not_cno) | Close the remaining Admitted proof | 1 of 4 lambda CNO theorems is incomplete |
+| Absolute-zero brainfuck interpreter | Interpreter preserves CNO properties | Claims of computational zero need formal backing |
+| Absolute-zero whitespace interpreter | Same as brainfuck — CNO preservation | Both esoteric interpreters need same guarantee |
+| Aletheia verification checks | Verification pipeline produces sound results | Rhodibot extraction depends on correct checks |
+| Quantum mechanics proofs | Extend QuantumMechanicsExact.v coverage | Existing proofs are partial |
+
+## Recommended Prover
+
+**Coq** — Existing proof infrastructure is in Coq. The `y_not_cno` Admitted needs to be closed in Coq. Aletheia (Rust) verification would benefit from an **Idris2** ABI layer.
+
+## Priority
+
+**MEDIUM** — Has existing proof infrastructure with one known gap. The Admitted y_not_cno is a concrete, closable proof obligation. Aletheia verification correctness is more important long-term.
+
+## Template ABI Cleanup (2026-03-29)
+
+Template ABI removed -- was creating false impression of formal verification.
+The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template
+scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs.

TEST-NEEDS.md

@@ -0,0 +1,59 @@
+# TEST-NEEDS.md — maa-framework
+
+> Generated 2026-03-29 by punishing audit.
+
+## Current State
+
+| Category     | Count | Notes |
+|-------------|-------|-------|
+| Unit tests   | 0     | No inline tests in source |
+| Integration  | 3     | absolute-zero FFI integration_test.zig, aletheia FFI integration_test.zig, rhodibot integration_tests.rs |
+| E2E          | 0     | None |
+| Benchmarks   | 1     | aletheia/benches/verification_benchmark.rs — uses std::time, not criterion (manual benchmark, not automated) |
+
+**Source modules:** ~23 across 2 subsystems. absolute-zero: brainfuck interpreter, whitespace interpreter, main + ABI/FFI. aletheia: checks, config, main, output, types + rhodibot + rhodium-pipeline + ABI/FFI.
+
+## What's Missing
+
+### P2P (Property-Based) Tests
+- [ ] absolute-zero: arbitrary brainfuck program fuzzing (already has fuzz target, good)
+- [ ] aletheia: arbitrary repo structure verification fuzzing
+- [ ] Config parsing: property tests for all config formats
+
+### E2E Tests
+- [ ] absolute-zero: compile -> execute -> verify program output
+- [ ] aletheia: full RSR verification pipeline (scan repo -> check rules -> report)
+- [ ] rhodibot: full bot operation cycle
+- [ ] rhodium-pipeline: extraction pipeline end-to-end
+
+### Aspect Tests
+- **Security:** No tests for aletheia bypass (can a repo trick the verifier?), rhodibot credential handling
+- **Performance:** Benchmark exists but is manual (std::time), not integrated into CI, not criterion-based
+- **Concurrency:** No tests for parallel verification of multiple repos
+- **Error handling:** No tests for malformed repos, missing files, invalid configurations
+
+### Build & Execution
+- [ ] `cargo test` for all Rust crates
+- [ ] `zig build test` for FFI tests
+- [ ] `cargo fuzz` for absolute-zero fuzz targets
+
+### Benchmarks Needed
+- [ ] Verification speed per repo size/complexity (aletheia)
+- [ ] Brainfuck/whitespace interpreter throughput (absolute-zero)
+- [ ] rhodibot processing rate
+- [ ] Pipeline extraction throughput
+
+### Self-Tests
+- [ ] aletheia: verify itself against RSR standards
+- [ ] Config schema validation
+- [ ] ABI version agreement
+
+## Priority
+
+**HIGH.** An RSR compliance verification framework that cannot verify itself is the definition of irony. 23 source modules with 0 unit tests. The 3 integration tests are a start but cover only FFI seams. The benchmark is manual and not CI-integrated. Fuzz targets for absolute-zero are good but need complementary structured tests.
+
+## FAKE-FUZZ ALERT
+
+- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing
+- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file
+- Priority: P2 — creates false impression of fuzz coverage