docs: add M2 estate audit report (2026-04-04)

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

docs/reports/audit/audit-2026-04-04.md

@@ -0,0 +1,130 @@
+# Audit Report — valence-shell (2026-04-04)
+
+## Summary
+
+Valence Shell (vsh) is an advanced research prototype (v0.9.0) of a formally verified shell with proven reversibility guarantees. The codebase exhibits mature RSR compliance, comprehensive CI automation, and disciplined handling of dangerous patterns. However, it is explicitly NOT production-ready—the Lean4 correspondence proofs are ~85% confidence (property-tested only, not mechanized), and several high-priority gaps remain.
+
+## Findings
+
+### Critical
+
+1. **Lean->Rust correspondence unproven** — Testing-based validation only (~85% confidence), no mechanized correspondence proof
+2. **4 proof gaps documented** — PROOF_HOLES_AUDIT.md lists completion gaps across 8 proof files (4 genuine gaps, 4 axioms, 2 structural)
+3. **NOT production-ready** — Explicit disclaimer in CLAUDE.md, README, and docs/INTEGRATION.md
+4. **Dead code detected** — lean_ffi.rs (library doesn't exist), daemon_client.rs (no daemon), multiple stale job control methods
+
+### High
+
+1. **47/58 commits author-spoofed as "Test <test@example.com>"** — Metadata integrity compromised; commits authored by Sonnet LLM without proper attribution
+2. **Version inflation in commit history** — Previous versions claimed 1.0.0 / "production-ready" / "256 proofs" (2026-03-08 correction brought to 0.9.0 / "200+ theorems")
+3. **No mechanized Echidna integration** — Formal property validation pipeline not automated
+
+### Medium
+
+1. **POSIX compliance incomplete** — Functions, script execution, word splitting ($IFS), tilde expansion, trap, alias still missing
+2. **GDPR compliance stubs** — RMO (Remove-Match-Obliterate) for secure deletion not implemented
+3. **Elixir NIF broken** — Reference implementation build broken (low priority, slated for removal)
+4. **10 proof holes** — Mix of genuine gaps, axioms, structural issues (see PROOF_HOLES_AUDIT.md)
+
+## RSR Compliance
+
+- **EXPLAINME.adoc**: present ✓
+- **0-AI-MANIFEST.a2ml**: present ✓
+- **.machine_readable/**: present ✓
+- **SECURITY.md**: present ✓
+- **CONTRIBUTING.md**: present ✓
+
+## Test Coverage
+
+**Comprehensive test suite (602 tests passing, 0 failures):**
+
+- Unit tests (lib): 277
+- Correspondence (Lean 4): 28
+- Extended features: 55
+- Integration tests: 35
+- Integration (extra): 10
+- Lean4 proptest: 16
+- Parameter expansion: 67
+- Property correspondence: 15
+- Property tests: 28
+- Security tests: 15
+- Doctests: 52
+- **Total**: 602 passing, 0 failures
+- Ignored (stress): 14 (run manually)
+
+**Test files:**
+- impl/rust-cli/tests/ — 9 integration test suites
+- impl/elixir/test/ — test_helper.exs (stale)
+- Comprehensive property-based testing via proptest
+
+## Proof Debt
+
+**Status: SIGNIFICANT DEBT, ACTIVELY MANAGED**
+
+From PROOF_HOLES_AUDIT.md:
+- 4 genuine proof gaps (need completion work)
+- 4 axioms (assumed truths, not proven)
+- 2 structural issues (architectural, not logical)
+- 10 holes total across 8 files
+
+Dangerous pattern status:
+- believe_me: 0 actual uses detected ✓
+- assert_total: 0 actual uses detected ✓
+- Admitted (Coq): ~10 remaining (see INTEGRATION.md, lines 163-174)
+- sorry: 0 actual uses detected ✓
+- unsafeCoerce: 0 Haskell uses detected ✓
+- Obj.magic: 24 calls REPLACED in ReScript (eliminated 2026-03-13, annotated 1 for MCP JSON cast)
+
+Proof integrity enforced via:
+- .bot_directives/echidnabot.scm (bans Admitted at severity "critical")
+- CI validation workflow (echidna-validation.yml)
+- CONTRIBUTING.md (line 283): "Avoid admit/Admitted in main branch"
+- Machine-readable policies (MUST.contractile)
+
+## Publication Safety
+
+**Current claim**: "Formally verified shell with proven reversibility guarantees"
+
+**Evidence gap**: Lean4→Rust correspondence is property-tested (~85% confidence) but NOT mechanized. Claims should be downscoped to:
+- "Advanced research prototype with formal reversibility theorems in Lean4"
+- "Property-tested Rust implementation (85% confidence)"
+- "NOT production-ready for security-critical systems"
+
+The shell **functionally works** (602 tests pass), but the **mathematical proof story is incomplete**.
+
+## CI Health
+
+**Status: COMPREHENSIVE, WELL-MAINTAINED**
+
+Active workflows:
+- echidna-validation.yml — Formal proof validation
+- cflite_pr.yml / cflite_batch.yml — Coq/Lean/Agda/Isabelle/Mizar/Z3 validation
+- ts-blocker.yml, npm-bun-blocker.yml — Language policy enforcement
+- workflow-linter.yml — CI integrity
+- instant-sync.yml — Git mirroring
+
+**No obvious failures** detected in workflow definitions. SHA pins verified. No banned languages in CI.
+
+## Verdict
+
+**AFTER REPAIR: Plan B (Conditional Publication)**
+
+This is sophisticated research-grade code that deserves publication—BUT ONLY with corrected claims:
+
+**Required repairs:**
+1. Downscope claims from "formally verified" to "formally specified" (Lean4) with "property-tested implementation" (Rust)
+2. Fix commit author metadata (re-sign 47 commits attributed to "Test <test@example.com>")
+3. Document 4 proof gaps explicitly in README (not hidden in PROOF_HOLES_AUDIT.md)
+4. Implement Echidna CI integration (currently manual/optional)
+5. Remove dead code (lean_ffi.rs, daemon_client.rs, unused job control methods)
+
+**If repairs completed**: PUBLISHABLE as "Advanced Research Prototype — v0.9.0"
+
+**Do not publish as-is** — the version number, feature claims, and proof gap documentation need alignment first.
+
+---
+
+**Audited by**: M2 estate audit (2026-04-04)
+**Previous audit**: 2026-02-12 (Opus)
+**Confidence**: HIGH (repairs are well-scoped)
+**Recommendation**: REPAIR THEN PUBLISH