Five concrete implementations of the valence-shell semantics, each serving a distinct role in the polyglot verification stack.
| Path | Role |
|---|---|
|
PRIMARY — the interactive Rust shell. Daily-driver development
target (v0.9.0; see |
|
Reference implementation in Elixir. The NIF build is currently
broken (declared low-priority in |
|
Extraction target for the Coq proofs in |
|
ReScript-based MCP (Model Context Protocol) bindings. Uses Deno
+ ReScript per the hyperpolymath language policy in |
|
Zig FFI implementation targeting ~5ms cold start. Builds cleanly
but is not yet integrated with the Rust CLI. See
|
Polyglot implementations cross-validate the formal Lean 4 / Coq specs
in ../proofs/: the Rust CLI is the "is" (running code), the OCaml
extraction is one "ought" path (extracted from Coq), the Elixir / Zig
variants test portability of the same operational semantics.
The audit report ../docs/governance/CRG-AUDIT-2026-04-18.adoc is the
authoritative cross-implementation status snapshot.