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

@@ -1,10 +1,48 @@
 # PROOF-NEEDS.md
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+
+## Current State
+
+- **LOC**: ~18,000
+- **Languages**: OCaml, Rust, Idris2, Zig
+- **Existing ABI proofs**: `src/abi/*.idr` (template-level)
+- **Dangerous patterns**: None detected
+
+## What Needs Proving
+
+### Type Checker (compiler/lib/typecheck.ml — 775 lines)
+- Core type checker for a Turing-complete topological programming language
+- Prove: type soundness (preservation + progress)
+- Prove: type checking terminates on all inputs
+
+### Evaluator (compiler/lib/eval.ml)
+- Prove: evaluation preserves types (subject reduction)
+- Prove: well-typed programs in the decidable fragment terminate
+
+### Parser Correctness (compiler/lib/)
+- `token.ml`, lexer/parser
+- Prove: parser accepts exactly the language defined by the grammar
+- Less critical than type system proofs but valuable for confidence
+
+### WASM Compilation (compiler/tangle-wasm/src/lib.rs)
+- Prove: compilation preserves semantics (source-level evaluation matches WASM execution)
+- This is a compiler correctness theorem — high value but high effort
+
+### Fuzz Testing Coverage
+- `compiler/fuzz/fuzz_lexer.ml`, `fuzz_parser.ml` — fuzzing is present but not formal
+- Proofs would subsume the need for fuzzing on core invariants
+
+## Recommended Prover
+
+- **Coq** or **Lean4** — OCaml type checkers have a strong tradition of Coq mechanisation (e.g., CompCert)
+- **Idris2** for the ABI layer
+
+## Priority
+
+**HIGH** — Programming language with a type checker and evaluator. Type soundness is the minimum bar for a language claiming Turing-completeness with a type system. Without it, the topological type claims are unverified.
 
 ## 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.
-
-When this project needs formal ABI verification, create domain-specific Idris2 proofs
-following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-server`.

TEST-NEEDS.md

@@ -0,0 +1,47 @@
+# TEST-NEEDS: tangle
+
+## Current State
+
+| Category | Count | Details |
+|----------|-------|---------|
+| **Source modules** | 11 | Rust: ast, ast_jtv, lexer, parser, parser_jtv, eval, lib, main, sexpr + 3 Idris2 ABI |
+| **Unit tests (inline)** | 252 | lexer=151, parser=40, parser_jtv=32, eval=29 |
+| **Integration tests** | 0 | None |
+| **E2E tests** | 0 | None |
+| **Benchmarks** | 4 files | bench_lexer.rs (135L), bench_parser_rust.rs (106L), bench_lexer.ml (113L), bench_parser.ml (88L) |
+| **Fuzz tests** | 2 | fuzz_lexer.rs, fuzz_parser.rs |
+
+## What's Missing
+
+### E2E Tests
+- [ ] No test that parses a Tangle program and evaluates it end-to-end
+- [ ] No test for the sexpr output format
+- [ ] No test for the main binary
+
+### Aspect Tests
+- [ ] **Security**: No injection/escape tests for the parser
+- [ ] **Performance**: Benchmarks exist -- need to verify they actually run
+- [ ] **Concurrency**: N/A for a language parser
+- [ ] **Error handling**: No tests for error recovery, partial parse, unterminated strings
+
+### Build & Execution
+- [ ] OCaml benchmarks (bench_lexer.ml, bench_parser.ml) -- does OCaml build config exist?
+- [ ] No Idris2 ABI compilation test
+
+### Benchmarks Status
+- [x] bench_lexer.rs (135 lines) -- appears real
+- [x] bench_parser_rust.rs (106 lines) -- appears real
+- [?] bench_lexer.ml (113 lines) -- needs OCaml build verification
+- [?] bench_parser.ml (88 lines) -- needs OCaml build verification
+
+### Self-Tests
+- [ ] No self-diagnostic mode
+
+## FLAGGED ISSUES
+- **252 inline unit tests is good** for a parser/lexer
+- **Benchmarks appear genuine** -- best benchmark setup among scanned repos
+- **Fuzz tests exist** -- rare and commendable
+- **ast.rs, ast_jtv.rs, sexpr.rs have 0 tests** -- structural modules untested
+- **No integration/E2E despite having eval** -- can't verify programs actually run correctly
+
+## Priority: P2 (MEDIUM) -- solid unit/bench/fuzz foundation, needs E2E and integration