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,27 @@
+# Proof Requirements
+
+## Current state
+- `src/abi/Types.idr` — Feedback types
+- `src/abi/Layout.idr` — Memory layout
+- `src/abi/Foreign.idr` — FFI declarations
+- No dangerous patterns in ABI layer
+- Claims: "formal verification via Idris2 for critical ABI definitions and memory safety proofs", "Production Ready"
+- 92K lines of source
+
+## What needs proving
+- **Deduplication correctness**: Prove the deduplicator never drops unique feedback entries and never allows true duplicates through
+- **Submission atomicity**: Prove feedback submissions either fully succeed or fully fail (no partial submissions that corrupt state)
+- **Memory layout proofs**: The README claims "memory safety proofs" — these should be materialized in the ABI layer with actual dependent type proofs for layout correctness
+- **Rate limiting fairness**: Prove rate limiting does not permanently block legitimate users
+
+## Recommended prover
+- **Idris2** — Already used for ABI; the claim of "memory safety proofs" needs to be substantiated with actual proofs in the existing `.idr` files
+
+## Priority
+- **MEDIUM** — The README explicitly claims formal verification and memory safety proofs. If those proofs do not exist in substance, the claim is misleading. Priority is to either write the proofs or soften the claims.
+
+## 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,80 @@
+# Test & Benchmark Requirements
+
+## Current State
+- Unit tests: NONE (0 test files found)
+- Integration tests: NONE
+- E2E tests: NONE
+- Benchmarks: NONE
+- panic-attack scan: NEVER RUN
+
+## What's Missing
+### Point-to-Point (P2P)
+34 Elixir source files with ZERO test files:
+- feedback_a_tron/application.ex — no tests
+- feedback_a_tron/deduplicator.ex — no tests
+- feedback_a_tron/mcp/tools/submit_feedback.ex — no tests
+- feedback_a_tron/mcp/tools/migration_observe.ex — no tests
+- feedback_a_tron/mcp/server.ex — no tests
+- feedback_a_tron/network_verifier.ex — no tests
+- feedback_a_tron/submitter.ex — no tests
+- feedback_a_tron/audit_log.ex — no tests
+- feedback_a_tron/cli.ex — no tests
+- feedback_a_tron/migration_observer.ex — no tests
+- feedback_a_tron/verisim_writer.ex — no tests
+- feedback_a_tron/batch_reviewer.ex — no tests
+- feedback_a_tron/report_generator.ex — no tests
+- feedback_a_tron/pipeline/supervisor.ex — no tests
+- feedback_a_tron/pipeline/producer.ex — no tests
+- feedback_a_tron/pipeline/verisim_consumer.ex — no tests
+- feedback_a_tron/pipeline/review_consumer.ex — no tests
+- feedback_a_tron/secure_dns.ex — no tests
+- feedback_a_tron/channels/nntp.ex — no tests
+- feedback_a_tron/channels/discourse.ex — no tests
+- Plus ~14 more modules
+- 3 Idris2 ABI files — no tests
+- 1 Julia file — no tests
+
+### End-to-End (E2E)
+- Submit feedback -> deduplicate -> review -> write to VeriSimDB
+- MCP server: receive tool call -> process -> respond
+- Batch review: load batch -> review all -> generate report
+- Pipeline: produce events -> consume -> write to VeriSimDB
+- Migration observation: detect migration -> observe -> record
+- NNTP channel: receive -> process -> forward
+- Discourse channel: receive -> process -> forward
+- CLI: submit/review/report commands
+
+### Aspect Tests
+- [ ] Security (MCP tool injection, network verifier bypass, NNTP injection, audit log tampering)
+- [ ] Performance (batch review throughput, pipeline backpressure, VeriSimDB write latency)
+- [ ] Concurrency (GenStage pipeline, concurrent submissions, supervisor restart)
+- [ ] Error handling (VeriSimDB unavailable, network failures, malformed feedback)
+- [ ] Accessibility (N/A)
+
+### Build & Execution
+- [ ] mix compile — not verified
+- [ ] mix test — not verified (no test files to run)
+- [ ] MCP server starts — not verified
+- [ ] CLI --help works — not verified
+- [ ] Self-diagnostic — none
+
+### Benchmarks Needed
+- Feedback submission throughput
+- Deduplication speed and accuracy
+- Pipeline end-to-end latency
+- VeriSimDB write performance
+- Batch review performance at scale
+
+### Self-Tests
+- [ ] panic-attack assail on own repo
+- [ ] MCP server health check
+- [ ] Pipeline self-test
+
+## Priority
+- **HIGH** — 34 Elixir source files with ZERO tests. This is a feedback processing system with MCP integration, GenStage pipeline, multi-channel input (NNTP, Discourse), VeriSimDB integration, and audit logging. Not a single module has a test file. The pipeline supervisor/producer/consumer pattern especially needs testing for correctness under load and failure conditions.
+
+## 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