Architecture

Architecture

Three layers, loosely coupled.

1. Proof layer (proofs/)

The load-bearing verification. Six prover backends prove the same CNO properties from different angles:

Prover	Strength	What we prove with it
Coq	Constructive, mature	Core CNO theory, statistical mechanics (Landauer), category, lambda, quantum, filesystem
Lean 4	Mathlib + tooling	Modern restatement, cross-validation
Z3	Automated SMT	Decidable fragments — fast counterexample search
Agda	Dependent types	Type-level CNO certificates
Isabelle/HOL	Production-grade	Industrial-style verification
Mizar	Mathematical library	Connection to standard maths corpus

Multi-prover is intentional: each catches what the others miss. See Proof Systems for the choice rationale.

2. Interpreter + ABI layer (src/, ffi/)

• src/abi/ — Idris2 type declarations for the C ABI, with formal alignment + size proofs. See ABI.
• src/brainfuck/, src/whitespace/ — interpreter crates in Rust. The former interpreters/affinescript/ Malbolge interpreter (AffineScript) was removed in the estate-policy sweep (PR #42); AffineScript was banned by the language policy on 2026-04-30.
• ffi/zig/ — Zig FFI shim that the Idris2 ABI binds to.

3. Examples + tooling (examples/, verification/, Justfile)

• examples/<lang>/ — CNOs in 23+ languages (ada, brainfuck, c, clojure, cobol, cpp, csharp, elixir, erlang, fortran, fsharp, haskell, javascript, lisp, malbolge, ocaml, php, prolog, rust, scala, scheme, special-ops, whitespace). Banned-language examples (go, java, kotlin, swift, ruby, perl) were removed 2026-05-25 per project policy.
• verification/ — top-level verify scripts (verify-proofs.sh, setup-and-verify.sh, run-local-verification.sh).
• Justfile — recipes for everything; just build-all, just verify, etc.

ECHIDNA integration (external)

ECHIDNA is the estate-wide neurosymbolic prover gateway, separate repo. absolute-zero calls into it via the echidna-llm-mcp BoJ cartridge — never directly. See ECHIDNA.adoc.

┌──────────────────────────┐         ┌──────────────────────────┐
│   absolute-zero          │ calls   │   ECHIDNA (separate)     │
│   - proofs/              ├────────►│   - neural tactics       │
│   - src/                 │ via BoJ │   - 105 prover backends  │
│   - examples/            │         │   - 66,674-proof corpus  │
└──────────────────────────┘         └──────────────────────────┘

Data flow on just verify

proofs/verify-active-provers.sh
  ├── proofs/agda        → agda --safe --without-K (CNO, OND, EchoBridgeScaffold, EchoBridgeCNO)
  ├── proofs/z3          → proofs/z3/verify.sh (expect-annotated bounded checks)
  └── src/abi            → idris2 --build absolute-zero-abi.ipkg

The Coq, Lean 4, Isabelle/HOL and Mizar trees were archived on 2026-10-10 under archive/proofs/ (coq/, lean4/, isabelle/, mizar/) and are not run. The former six-prover gate is archive/proofs/verify-all-provers.six-prover.sh.

Why this taxonomy

The directory layout follows the RSR-template-repo convention. Compliance state is tracked in RSR_COMPLIANCE.adoc.