Valence Shell (vsh)

Formally verified shell implementing the MAA (Mutually Assured Accountability) Framework.

Every operation backed by machine-checkable proofs, enabling GDPR compliance with mathematical certainty.

Important

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) See [_verification_status] and CHANGELOG for details.

Overview

Valence Shell is a formally verified shell with proven reversibility guarantees. Unlike traditional shells where "undo" is a best-effort feature, vsh provides mathematical proofs that operations can be reversed.

Key Features

Features

Formal Verification

• ✓ Formally Proven Reversibility: rmdir(mkdir(p, fs)) = fs

• ✓ Polyglot Verification: 6 proof systems (Coq, Lean 4, Agda, Isabelle, Mizar, Z3)

• ✓ ~250+ Theorems: Proven across different logical foundations (4 proof gaps remain)

• ✓ Content Operations: File read/write with proven reversibility

• ✓ MAA Framework: Mutually Assured Accountability with audit trails

Shell Features (v0.9.0)

• ✓ Unix Pipelines: Multi-stage pipelines (cmd1 | cmd2 | cmd3)

• ✓ I/O Redirections: All POSIX redirections (>, >>, <, 2>, 2>>, &>, 2>&1)

• ✓ Process Substitution: <(cmd) and >(cmd) with FIFO implementation

• ✓ Arithmetic Expansion: $expr with full operator support

• ✓ Here Documents: <<DELIMITER, <←DELIMITER, <<<word

• ✓ Job Control: Background jobs, fg, bg, kill, job specifications

• ✓ Shell Variables: $VAR, export, assignment, expansion

• ❏ GDPR Compliance: Secure deletion (obliterate) + audit logging (stubs only)

• ✓ Syntax Highlighting: Real-time color-coded REPL

• ✓ Command Correction: Intelligent typo suggestions

• ✓ Friendly Errors: fish-style helpful error messages

• ✓ Smart Pager: Auto-paging for long output

• ✓ 3-Tier Help: Quick/verbose/man page documentation

• ✓ 555 Tests Passing: Unit, correspondence, integration, property, security

Implementation

• ✓ Production-Ready Rust CLI: 95% complete, fully functional shell

• ✓ Offline-First: All proofs verifiable air-gapped

• ✓ Fuzzing: 4 fuzz targets with cargo-fuzz integration

What Makes This Different?

Feature	Traditional Shells	Valence Shell
Undo	Best-effort, manual	Mathematically proven correct
Verification	Testing only	Formal proofs in 6 systems
Accountability	Logs (can be tampered)	MAA framework with proofs
Trust	"Hope it works"	Mathematical guarantees

Quick Start

Prerequisites

Minimum (to run demonstrations):

# One of:
OCaml 5.0+
Elixir 1.15+
Bash 4.0+

Full Development (to modify proofs):

Coq 8.18+
Lean 4.3+
Agda 2.6.4+
Isabelle/HOL 2024
Z3 4.12+
Just (command runner)
Nix (recommended)

Installation

With Nix (Recommended)

# Clone repository
git clone https://github.com/Hyperpolymath/valence-shell.git
cd valence-shell

# Enter development environment
nix develop

# Build all proof systems
just build-all

# Run comprehensive demonstration
just demo

With Containers

# Build container
podman build -t valence-shell .

# Run verification
podman run valence-shell just verify-proofs

# Interactive shell
podman run -it valence-shell bash

Manual Setup

# Install proof assistants (per their documentation)
# Then:
git clone https://github.com/Hyperpolymath/valence-shell.git
cd valence-shell

# Build Coq proofs
just build-coq

# Build Lean 4 proofs
just build-lean4

# Run tests
just test-all

Basic Usage

# Verify all proofs compile
just verify-proofs

# Run demonstration showing all proven theorems
./scripts/demo_verified_operations.sh

# Build specific proof system
just build-coq      # Coq proofs
just build-lean4    # Lean 4 proofs
just build-agda     # Agda proofs
just build-isabelle # Isabelle proofs

# Show available commands
just --list

What’s Proven?

Core Theorems (All 5 Manual Proof Systems)

Theorem mkdir_rmdir_reversible :
  forall p fs,
    mkdir_precondition p fs ->
    rmdir p (mkdir p fs) = fs.

Theorem create_delete_file_reversible :
  forall p fs,
    create_file_precondition p fs ->
    delete_file p (create_file p fs) = fs.

Theorem write_file_reversible :
  forall p fs old_content new_content,
    write_file_precondition p fs ->
    read_file p fs = Some old_content ->
    write_file p old_content (write_file p new_content fs) = fs.

Composition (Proven in 5 Systems)

Theorem operation_sequence_reversible :
  forall ops fs,
    all_reversible ops fs ->
    apply_sequence (reverse_sequence ops)
                   (apply_sequence ops fs) = fs.

Equivalence (Proven in 4 Systems)

Theorem cno_identity_element :
  forall op fs,
    reversible op fs ->
    apply_op (reverse_op op) (apply_op op fs) ≈ fs.

Tip	CNO = Certified Null Operation: A reversible operation followed by its reverse provably does nothing (identity element). This connects to Absolute Zero’s composition theory.

Architecture

Proof Systems

Valence Shell uses polyglot verification across 6 proof systems:

System	Foundation	Lines
Coq	Calculus of Inductive Constructions	~1,200
Lean 4	Dependent Type Theory	~900
Agda	Intensional Type Theory	~700
Isabelle/HOL	Higher-Order Logic	~650
Mizar	Tarski-Grothendieck Set Theory	~400
Z3 SMT	First-Order Logic + Theories	~150

Why 6 systems?

• Different logical foundations increase confidence

• Cross-validation catches errors

• Industry standard (seL4, CompCert)

Trust Boundaries

┌─────────────────────────────────────┐
│ Formal Proofs (HIGH TRUST)          │ ← Mathematical guarantees
│ ~250+ theorems, ~4,280 lines         │
└─────────────┬───────────────────────┘
              │ Extraction (GAP) ⚠️
┌─────────────▼───────────────────────┐
│ OCaml Implementation (MEDIUM TRUST) │ ← Type safe, memory safe
│ FFI to POSIX, audit logging         │
└─────────────┬───────────────────────┘
              │ FFI (GAP) ⚠️
┌─────────────▼───────────────────────┐
│ POSIX Syscalls (LOW TRUST)         │ ← Kernel guarantees only
│ mkdir, rmdir, open, read, write     │
└──────────────────────────────────────┘

Warning

Verification Gap: The formal proofs operate on abstract models. The implementation (OCaml FFI + POSIX) is not formally connected to the proofs. This means: Proofs guarantee model correctness ✅ Implementation may have bugs ⚠️ Extraction may introduce errors ⚠️ To reach production: Close extraction gap (Coq → OCaml verification).

Verification Status

✅ What IS Guaranteed (by proofs)

• If preconditions hold, rmdir(mkdir(p, fs)) = fs

• If preconditions hold, write(p, old, write(p, new, fs)) = fs

• Operations on p1 don’t affect p2 (when p1 ≠ p2)

• Composition: sequences of operations reverse correctly

• ~250+ theorems proven across 6 verification systems

❌ What Is NOT Guaranteed

• Implementation matches proofs (manual review required)

• POSIX compliance beyond modeled operations

• Performance (not optimized)

• Concurrent access from multiple processes

• File system integrity after crashes

• Protection against malicious inputs to unverified code

MAA Framework

Mutually Assured Accountability: Every action has a provable audit trail.

RMR (Remove-Match-Reverse)

Status: ✅ Proven for directories and files

RMR primitives:
- mkdir/rmdir (proven reversible)
- create_file/delete_file (proven reversible)
- write_file (proven reversible)

Use Case: Safe operations with guaranteed rollback

RMO (Remove-Match-Obliterate)

Status: 🔄 Planned (not yet implemented)

Use Case: GDPR "right to be forgotten" with mathematical guarantee of complete removal

Contributing

We welcome contributions across three perimeters:

🔴 Perimeter 1: Core (Maintainers Only)

• Formal proofs

• Security-critical code

• Requires: Proof assistant expertise

🟡 Perimeter 2: Extensions (Trusted Contributors)

• Implementations

• Optimizations

• New features

• Requires: Track record, review

🟢 Perimeter 3: Community (Open to All)

• Examples

• Tutorials

• Documentation

• Tools

• Requires: Basic testing, clear docs

See CONTRIBUTING.md for details.

Documentation

File	Description
CLAUDE.md	START HERE - Comprehensive AI assistant context
proofs/README.md	Proof documentation, how to read proofs
SECURITY.md	Security policy, vulnerability reporting
CONTRIBUTING.md	Contribution guidelines, TPCF framework
CODE_OF_CONDUCT.md	Community standards, emotional safety
CHANGELOG.md	Version history, what’s changed
RSR_COMPLIANCE.md	RSR Framework compliance report (PLATINUM)
PROGRESS_REPORT.md	Phase 1 detailed report
PHASE2_REPORT.md	Composition & equivalence theory
PHASE3_INITIAL_REPORT.md	File content operations

Roadmap

Version 0.15.0 (Next Release)

• ❏ Glob expansion (.txt, ?.rs, [a-z])

• ❏ Quote processing (proper escaping, single/double quotes)

• ❏ Variables in redirections (edge case fix)

• ❏ Expanded correspondence tests (15 → 25+)

Version 0.16.0

• ❏ Echidna validation pipeline

• ❏ Property-based build validation

• ❏ Continuous fuzzing in CI/CD

Version 0.17.0

• ❏ RMO (obliterative deletion) proofs

• ❏ GDPR compliance primitives

• ❏ Secure overwrite guarantees

Version 1.0.0 (Production Ready)

• ❏ Close extraction gap (Lean → Rust formal verification)

• ❏ Verify FFI layer

• ❏ Full POSIX compliance (subset)

• ❏ Performance optimization

• ❏ Security audit complete

• ❏ Fuzzing campaign complete

Licensing

License: Palimpsest-MPL 1.0 or later (SPDX: PMPL-1.0-or-later)

See LICENSE for full text and usage rights. Third-party notices: THIRD_PARTY_NOTICES.md.

RSR Compliance

Valence Shell achieves PLATINUM-level Rhodium Standard Repository (RSR) compliance (105/100):

• ✅ Complete documentation (7 required files + 20 additional)

• ✅ .well-known/ directory (RFC 9116 compliant)

• ✅ Build systems (Just + Nix + Container + CI/CD)

• ✅ TPCF (Tri-Perimeter Contribution Framework)

• ✅ Formal verification (6 proof systems, ~250+ theorems)

• ✅ Zero runtime dependencies

• ✅ Offline-first verification

• ✅ Security guarantees (formal proofs + memory safety)

See RSR_COMPLIANCE.md for full report.

Community

• Issues: https://github.com/Hyperpolymath/valence-shell/issues

• GitLab: https://gitlab.com/non-initiate/rhodinised/vsh (primary development)

• Security: See .well-known/security.txt

• Code of Conduct: CODE_OF_CONDUCT.md

• Humans: .well-known/humans.txt

FAQ

Why 6 proof systems?

Different logical foundations increase confidence. If all 6 systems prove the same theorem, it’s highly unlikely all have the same bug.

Is this production-ready?

No. Version 0.14.0 is an advanced research prototype with a working shell (82% complete), but the extraction gap (Lean → Rust → POSIX) is not formally verified. The Rust CLI is functional and extensively tested (177 tests), but lacks formal proof of correspondence to the Lean theorems. Use for research, education, and experimentation only.

Can I use this in my project?

For research/education: Yes!
For production: Not yet (wait for v1.0.0)
License: Palimpsest-MPL 1.0 or later (PMPL-1.0-or-later)

How do I verify the proofs?

# Install proof assistants (via Nix or manually)
nix develop  # if using Nix

# Verify all proofs compile
just verify-proofs

# This compiles ~4,280 lines of proofs and checks:
# - Coq: generates .vo certificate files
# - Lean 4: compiles to executable
# - Agda: type-checks and generates interface files
# - Isabelle: builds heap image
# - Z3: checks SMT assertions

What’s the difference between algorithmic and thermodynamic reversibility?

Algorithmic (what we have): F⁻¹(F(s)) = s - operations can be undone, information preserved

Thermodynamic (what we DON’T have): Energy → 0 (Landauer limit), Bennett’s reversible computing

We prove the former, not the latter.

How does this relate to Absolute Zero?

Absolute Zero provided the CNO (Certified Null Operation) theory showing that reversible operations create identity elements. Valence Shell implements this theory for filesystem operations.

Citation

If you use Valence Shell in academic work:

@software{valence_shell_2025,
  title = {Valence Shell: Formally Verified Shell with MAA Framework},
  author = {{Valence Shell Contributors}},
  year = {2025},
  url = {https://github.com/Hyperpolymath/valence-shell},
  note = {Polyglot verification across 6 proof systems},
  version = {0.14.0}
}

Acknowledgments

• Software Foundations - Benjamin Pierce et al.

• seL4 Verified Kernel - NICTA/Data61

• CompCert Compiler - Xavier Leroy

• Absolute Zero - CNO composition theory

• Coq, Lean 4, Agda, Isabelle, Mizar, Z3 teams

• RSR Framework - Repository standards

See humans.txt for complete attribution.

License

Copyright (c) 2025 Valence Shell Contributors

Licensed under Palimpsest-MPL 1.0 or later (SPDX: PMPL-1.0-or-later). See LICENSE for full text.

---

Made with ❤️ by humans and AI, for humans who value formal correctness.

Status: Advanced Research Prototype (v0.9.0) | RSR: PLATINUM (105/100) | Proofs: ~250+ theorems | Tests: 602 passing

"Every operation reversible. Every claim proven. Every contributor valued."

Architecture

See TOPOLOGY.md for a visual architecture map and completion dashboard.