docs: add TEST-NEEDS.md and/or PROOF-NEEDS.md from audit

Documents testing and proof gaps identified during batch audit.

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

Author: hyperpolymath

PROOF-NEEDS.md

@@ -0,0 +1,45 @@
+# PROOF-NEEDS.md
+<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+
+## Current State
+
+- **LOC**: ~94,700
+- **Languages**: Elixir, ReScript, Gleam, Julia, Rust, Idris2, Zig
+- **Existing ABI proofs**: `src/abi/*.idr` (template-level)
+- **Dangerous patterns**: 20+ `Obj.magic` in ReScript connector clients (VeriSimDrift, VeriSimFederation, VeriSimHexad, VeriSimProvenance, VeriSimSearch, VeriSimVql, Registry)
+
+## What Needs Proving
+
+### VQL Type Checker (src/vql/)
+- `VQLTypeChecker.res`, `VQLSubtyping.res`, `VQLProofObligation.res` — a query type system
+- Type checking correctness and subtyping transitivity should be formally proven
+- `VQLBidir.res` — bidirectional type inference needs soundness proof
+
+### Connector Client Type Safety (connectors/clients/rescript/)
+- Every client module uses `json->Obj.magic` to cast JSON responses to typed records
+- VeriSimDrift, VeriSimFederation, VeriSimHexad, VeriSimProvenance, VeriSimSearch, VeriSimVql all affected
+- Prove: API response schemas match expected ReScript types
+
+### Registry / Consensus (src/registry/)
+- `KRaftCluster.res` — Raft consensus implementation
+- `KRaftSerializer.res` — serialization for consensus protocol
+- Consensus algorithms have well-known formal specifications — this should be provably correct
+- `MetadataLog.res` — log integrity is critical for database correctness
+
+### Federation Protocol
+- VeriSimFederation handles cross-instance data replication
+- Prove: federation preserves data consistency (eventual consistency guarantees)
+
+### Provenance Chain
+- VeriSimProvenance tracks data lineage
+- Prove: provenance chains are append-only and tamper-evident
+
+## Recommended Prover
+
+- **Idris2** for VQL type system soundness and ABI contracts
+- **Lean4** for Raft consensus correctness (existing Lean4 Raft formalisations exist)
+- **Agda** for provenance chain integrity (algebraic properties)
+
+## Priority
+
+**HIGH** — Database system used as the persistence layer across the entire ecosystem. VQL type checking, Raft consensus, and provenance integrity are all areas where formal proofs would prevent data corruption or consistency violations.

TEST-NEEDS.md

@@ -0,0 +1,52 @@
+# TEST-NEEDS: verisimdb
+
+## Current State
+
+| Category | Count | Details |
+|----------|-------|---------|
+| **Source modules** | 18 | ReScript VQL (10: Bidir, Circuit, Context, Error, Explain, Parser, ProofObligation, Subtyping, TypeChecker, Types), Registry (4: KRaftCluster, KRaftSerializer, MetadataLog, Registry), Parser_test, 3 Idris2 ABI |
+| **Unit tests** | 1 file | VQLParser_test.res (~110 test/assert references) |
+| **Integration tests** | 1 file | integration_test.rs (0 #[test] -- may be stub) |
+| **E2E tests** | 0 | None |
+| **Benchmarks** | 2 files | modality_benchmarks.rs (104 bench/criterion refs), src/lib.rs |
+
+## What's Missing
+
+### P2P Tests (CRITICAL)
+- [ ] No tests for VQL type checker <-> subtyping <-> proof obligation pipeline
+- [ ] No tests for Registry <-> KRaft cluster interaction
+- [ ] No tests for bidirectional type inference (VQLBidir)
+
+### E2E Tests (CRITICAL)
+- [ ] No test that stores data, queries it via VQL, and validates results
+- [ ] No test for the full modality verification pipeline
+- [ ] No test for KRaft consensus with multiple nodes
+
+### Aspect Tests
+- [ ] **Security**: Database with no injection tests, no access control tests
+- [ ] **Performance**: Benchmark files exist -- need to verify they run
+- [ ] **Concurrency**: No concurrent read/write tests, no transaction isolation tests
+- [ ] **Error handling**: No tests for storage corruption, query timeout, cluster partition
+
+### Build & Execution
+- [ ] integration_test.rs has 0 #[test] -- appears to be a stub
+- [ ] No Idris2 ABI compilation test
+
+### Benchmarks Status
+- [x] modality_benchmarks.rs (104 criterion refs) -- appears genuine
+- [ ] No query throughput benchmark
+- [ ] No storage I/O benchmark
+- [ ] No cluster consensus latency benchmark
+
+### Self-Tests
+- [ ] No database self-consistency check
+- [ ] No `verisimdb --self-test` mode
+
+## FLAGGED ISSUES
+- **A DATABASE with 1 test file** -- VQLParser_test.res covers parsing but nothing else
+- **integration_test.rs is a STUB** with 0 actual test functions
+- **Registry/KRaft (distributed consensus) has 0 tests** -- consensus code is untested
+- **VQLBidir, VQLCircuit, VQLExplain, VQLProofObligation all have 0 tests**
+- **Benchmarks appear real** (104 criterion references) -- one bright spot
+
+## Priority: P0 (CRITICAL)