The README makes claims. This file backs them up with evidence from real code.
From README (lines 44, 60):
✓ 555 Tests Passing: Unit, correspondence, integration, property, security
✓ ~250+ Theorems: Proven across different logical foundations (4 proof gaps remain)
Evidence: /var/mnt/eclipse/repos/valence-shell/impl/rust-cli/tests/ contains 602 passing tests (updated 2026-03-08): 277 unit tests, 28 correspondence tests, 55 extended, 35 integration, 10 extra, 16 lean4 proptest, 28 property, 15 security, 52 doctests. Proof files at /var/mnt/eclipse/repos/valence-shell/proofs/coq/ (~1,200 lines), /var/mnt/eclipse/repos/valence-shell/proofs/lean4/ (~900 lines), /var/mnt/eclipse/repos/valence-shell/proofs/agda/, /var/mnt/eclipse/repos/valence-shell/proofs/isabelle/, /var/mnt/eclipse/repos/valence-shell/proofs/mizar/, /var/mnt/eclipse/repos/valence-shell/proofs/z3/.
Caveat: Test suite proves the Rust implementation works correctly. Proofs verify abstract models of reversibility. The extraction gap between Lean 4 proofs → Rust implementation is NOT mechanically verified—it’s ~85% confidence via property testing only. This is not production-ready.
From README (lines 40, 192-209):
✓ Formally Proven Reversibility:
rmdir(mkdir(p, fs)) = fs… Theorem mkdir_rmdir_reversible : forall p fs, mkdir_precondition p fs → rmdir p (mkdir p fs) = fs.
Evidence: /var/mnt/eclipse/repos/valence-shell/proofs/coq/FileSystem.v contains the theorem mkdir_rmdir_reversible proven in Coq with ~200 lines of tactics. Same theorem proven in /var/mnt/eclipse/repos/valence-shell/proofs/lean4/Reversibility.lean (Lean 4), /var/mnt/eclipse/repos/valence-shell/proofs/agda/, etc. Cross-validation across 5-6 proof systems increases confidence.
Caveat: Proofs operate on abstract filesystem models (not real POSIX). The Rust FFI layer (src/commands.rs) calls real syscalls (mkdir, rmdir) which are NOT proven to match the abstract model. A POSIX implementation bug could violate the proofs.
From README (lines 22-27):
Current Status: v0.9.0 — Advanced Research Prototype
NOT production-ready. Functional shell with formally proven reversibility, but POSIX compliance is incomplete and Lean→Rust correspondence is testing-based (~85% confidence), not mechanized.
Progress: ~72% of full roadmap complete, 602 tests passing (0 failures)
Evidence: /var/mnt/eclipse/repos/valence-shell/CLAUDE.md (lines 15-47) provides honest status: v0.9.0, ~72% complete, 4 real proof gaps (documented in /var/mnt/eclipse/repos/valence-shell/docs/PROOF_HOLES_AUDIT.md). Main gaps: no mechanized Lean→Rust correspondence, RMO/GDPR compliance stubs only, shell functions/script execution missing.
Caveat: This is refreshingly honest about limitations. Most projects would claim v1.0.0 and "production-ready"—this one correctly downgrades false claims from the Sonnet audit.
Uses polyglot formal verification stack (Coq + Lean 4 + Agda + Isabelle + Mizar + Z3). Same pattern across: - absolute-zero — Compositional algebra with CNO (Certified Null Operation) theory - proven-servers — Protocol verification (Idris2 ABI) - burble — Telecom control plane (Lean 4 core)
All share: Multiple proof systems for cross-validation, honest status reporting, no extraction claims without mechanization.
| Path | Contents & Purpose |
|---|---|
|
Rust CLI entry: REPL loop, command parsing, interactive shell with reedline |
|
Library root: module declarations, public API |
|
ShellState: file system state, operation history, undo/redo stacks. Core reversibility tracking. |
|
Built-in commands: mkdir, rmdir, touch, rm, cp, mv, ln, undo, redo, explain, checkpoint, restore, diff |
|
Command parsing: tokenization, variable expansion, glob expansion, quote processing. No formal proofs—empirical parsing. |
|
External command execution: PATH lookup, subprocess spawning, pipe handling, redirection setup |
|
Unix pipeline implementation: multi-stage pipes with proper file descriptor management |
|
I/O redirection: > (write), >> (append), < (read), 2> (stderr), 2>> (append stderr), &> (both), 2>&1 (combine) |
|
POSIX-compliant glob expansion: *, ?, […], {…}. Hidden file handling (requires explicit leading dot). |
|
Job control: bg, fg, jobs, kill commands. Signal handling for Ctrl+Z (SIGTSTP), Ctrl+C (SIGINT). |
|
Process substitution: <(cmd) and >(cmd) via FIFOs |
|
Arithmetic expansion: $expr with full operator support, shift overflow protection |
|
Here documents: <<DELIM, <←DELIM, <<<word |
|
test/[ and [[ ]] builtins for conditionals |
|
Command correction: Levenshtein distance for "Did you mean?" suggestions |
|
Interactive REPL with reedline, syntax highlighting, multi-line input for control structures |
|
Coq proofs: ~1,200 lines. Theorems for mkdir/rmdir, create/delete, write reversibility. |
|
Lean 4 proofs: ~900 lines. Same theorems, dependent type theory style. |
|
Agda proofs: ~700 lines. Intensional type theory foundation. |
|
Isabelle/HOL proofs: ~650 lines. Higher-order logic approach. |
|
Mizar proofs: ~400 lines. Tarski-Grothendieck set theory. |
|
Z3 SMT proofs: ~150 lines. Automated first-order logic verification. |
|
Correspondence tests: Lean 4 theorem validation via property testing (~85% confidence, not mechanized) |
|
Full end-to-end shell tests: pipes, redirections, glob expansion, job control |
|
Security tests: path traversal prevention, injection resistance, resource limits |
|
Property-based tests: glob correctness, arithmetic soundness, operation sequence reversibility |
|
Honest audit: 4 real proof gaps, 4 axioms, 2 structural gaps. Clear about what’s NOT proven. |
|
Detailed POSIX compliance roadmap: M1-M11 milestones, current status (M1-M9 complete, M10-11 partial) |
|
Comprehensive AI context: honest status (v0.9.0, ~72% complete), architecture, test results, critical issues |
|
Three-layer architecture (Valence Shell / Echo Types / Ochrance) + forbidden-moves rules for agents and reviewers. |
Valence Shell does not stand alone. It sits in a three-layer architecture:
-
Valence Shell (this repo) — shell operations, history, undo/redo, in-model reversibility proofs.
-
hyperpolymath/echo-types— semantic theory of structured loss; names what is recoverable, constrained, or genuinely lost. -
hyperpolymath/ochrance— receipt + attestation substrate (A2ML manifests, Merkle-backed state commitments, repair witnesses).
The bridge is documentation-and-orientation-only, not a mechanised dependency. See ECHO-TYPES-OCHRANCE-BRIDGE.adoc for the canonical forbidden-moves list (no claiming production-readiness, mechanised Lean→Rust correspondence, RMO/GDPR beyond stubs, or Ochrance cryptographic integrity).
Honest Assessment: Advanced research prototype. NOT production-ready. Extraction gap (Lean→Rust) is the critical blocker for any production claim.
What Works: - Functional shell: 602 tests passing, interactive REPL working - Formal proofs: 250+ theorems across 6 systems (about abstract models) - Reversibility tracking: undo/redo fully functional - Most POSIX features: pipes, redirections, glob, job control, variables
What’s Broken:
- NO mechanized Lean→Rust correspondence (85% confidence only)
- NO shell functions (func() { … })
- NO shell script execution (.sh files)
- RMO/GDPR compliance: stubs only
- POSIX compliance: ~72% (functions + script execution missing)
Open an issue or reach out at j.d.a.jewell@open.ac.uk — happy to explain the proof architecture, reversibility guarantees, or the honest gap between proofs and implementation.