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,28 @@
+# Proof Requirements
+
+## Current state
+- `src/abi/Types.idr` — Gating types
+- `src/abi/Layout.idr` — Memory layout
+- `src/abi/Foreign.idr` — FFI declarations
+- No dangerous patterns in ABI layer
+- Claims: SLM acts as "inhibitory antagonist" for LLM policy enforcement (GO/NO-GO gating)
+
+## What needs proving
+- **Policy completeness**: Prove that the NO-GO gate blocks ALL policy-violating outputs (no bypass path exists)
+- **Gate monotonicity**: Prove that once a NO-GO decision is made, it cannot be overridden by subsequent processing stages
+- **False positive boundedness**: Prove that the gating function's false-positive rate is bounded (does not degenerate to blocking everything)
+- **Policy composition soundness**: Prove that combining multiple policy rules preserves individual rule guarantees (no rule cancellation)
+- **Deterministic rule evaluation**: Prove the Rust policy oracle produces identical results for identical inputs (no hidden state)
+
+## Recommended prover
+- **Idris2** — Dependent types can express the policy lattice and monotonicity properties
+- **Lean4** — Good for the algebraic properties of policy composition if modeled as a semilattice
+
+## Priority
+- **HIGH** — Conative gating is a security/safety mechanism for LLM outputs. If the gate can be bypassed, the entire safety claim collapses. Policy completeness and gate monotonicity are critical.
+
+## 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,50 @@
+# Test & Benchmark Requirements
+
+## Current State
+- Unit tests: 0 pass / 0 fail (cargo test runs but finds 0 tests)
+- Integration tests: 1 Zig integration test (template)
+- E2E tests: NONE
+- Benchmarks: NONE
+- panic-attack scan: NEVER RUN
+
+## What's Missing
+### Point-to-Point (P2P)
+- src/main.rs — no tests
+- src/contract/src/lib.rs — no tests
+- src/oracle/src/lib.rs — no tests
+- src/slm/src/lib.rs — no tests
+- 2 Elixir source files — no tests
+- 3 Idris2 ABI files — no verification tests
+- 3 Zig FFI files — only template test
+
+### End-to-End (E2E)
+- Contract evaluation workflow
+- Oracle query/response cycle
+- SLM (presumably Small Language Model) interaction
+- Gating decision pipeline (input -> evaluate -> gate/pass)
+
+### Aspect Tests
+- [ ] Security (gating bypass, oracle manipulation, contract exploitation)
+- [ ] Performance (gating decision latency)
+- [ ] Concurrency (concurrent gate evaluations)
+- [ ] Error handling (oracle unavailability, malformed contracts)
+- [ ] Accessibility (N/A)
+
+### Build & Execution
+- [x] cargo build — compiles (with 0 tests)
+- [x] cargo test — passes (0 tests found)
+- [ ] Binary runs and exits cleanly — not verified
+- [ ] CLI --help works — not verified
+- [ ] Self-diagnostic — none
+
+### Benchmarks Needed
+- Gating decision latency
+- Contract evaluation throughput
+- Oracle round-trip time
+
+### Self-Tests
+- [ ] panic-attack assail on own repo
+- [ ] Built-in doctor/check command (if applicable)
+
+## Priority
+- **HIGH** — 5 Rust source files + 2 Elixir + Zig/Idris2 with ZERO tests. Cargo test finds literally nothing. This is a complete test vacuum for a component that makes security-relevant gating decisions.