Snapkitty/tlm-jxcl-forge

Mirrored from https://github.com/SNAPKITTYAGENT9NOVA/tlm-jxcl-forge at commit 48891c4. Part of the SnapKitty October 2026 main drop.

tlm-jxcl-Twin

TLM JXCL — a from-scratch, deterministic, byte-addressable 64-bit instruction-set architecture and toolchain, grown into a 100-crate Rust workspace covering the ISA itself, a post-quantum-encrypted caching and storage stack, and zero-knowledge error attestation. Alongside it live three fully independent workspaces: verification-forge, a from-scratch formal verification kernel; cloud-forge, a from-first-principles cloud-resource substrate (build the primitives an AWS-shaped platform would need, before any service-named crate exists); and tensor-forge, an ndarray-based arbitrary-rank tensor library with its own pure-Rust linear algebra. Every crate is real: either genuine new functionality, or code extracted verbatim from this repository's original six-crate baseline into its own independently-testable module — never a thin wrapper padding a headline number.

Table of contents

• Origins
• Repository map
• Getting started
• TLM JXCL: the instruction set (crates/jxcl*)
• Post-quantum cryptography and storage (crates/pq-*)
• photo-cache-service: the reference caching demo
• SQL Server vault (pq-sql-vault)
• Verifiable error attestations (pq-error-proof)
• verification-forge: a from-scratch proof kernel
• cloud-forge: a from-first-principles cloud substrate
• tensor-forge: an ndarray-based tensor library
• Phase 5: Formal verification and MATLAB certification
  • Alloy Freehand Lemmas framework
  • MATLAB certification modules
  • DSL compiler for lemma specifications
  • Hardened invariants and counter-algorithms
• Why 100 crates, and how to trust that number
• Networking, services, and cross-cutting concerns
• Testing methodology
• Quality gates
• Frequently asked questions
• Contributing / development workflow
• Documentation index
• License

Origins

TLM JXCL began as a single-crate, 3,500-line implementation specification for a "pure raw dense" instruction-set architecture: deterministic, byte-addressable, with no external dependencies in the ISA itself. Around that core grew a post-quantum-encrypted caching layer (a hardened Rust port of an original Express+Redis demo), a SQL Server-backed alternative store, and a zero-knowledge error-attestation scheme — six crates in total at that point. From there, an explicit mandate to decompose the workspace into 100 single-invariant crates (never fake ones — see Why 100 crates) produced the root workspace as it exists today. verification-forge began later and independently, as a from-scratch formal-verification kernel with no dependency on anything ISA- or crypto-specific — hence its own separate workspace rather than crate #101. cloud-forge began later still, as an explicit from-first-principles attempt at the substrate underneath an AWS-shaped cloud platform — again independent of the other two, and again a separate workspace rather than more root crates, for the same reason verification-forge is one.

Repository map

This repository holds four independent Cargo workspaces plus two formalization frameworks:

flowchart TB
    subgraph ROOT["root workspace: /Cargo.toml (100 crates)"]
        direction LR
        isa["ISA forge<br/>jxcl* (77 crates)<br/>zero dependencies"]
        pq["Post-quantum stack<br/>pq-* (22 crates)<br/>ML-KEM, AES-GCM, Groth16"]
        svc["photo-cache-service<br/>(1 crate)"]
        isa -->|opcode table, execution engine| svc
        pq -->|envelope sealing| svc
    end

    subgraph VF["verification-forge/Cargo.toml (21 crates)"]
        direction LR
        vfk["Trusted kernel<br/>vf-core, vf-reducer, vf-kernel"]
        vfe["Untrusted evidence<br/>vf-lexer/parser/axioms/…"]
        vfe --> vfk
    end

    subgraph CF["cloud-forge/Cargo.toml (39 crates)"]
        direction LR
        cfk["Primitive kernel<br/>cloud-resource, cloud-policy, …"]
        cfc["cloud-core facade"]
        cfk --> cfc
    end

    subgraph TF["tensor-forge/Cargo.toml (3 crates)"]
        direction LR
        tfc["tensor-core<br/>Tensor&lt;T&gt; on ndarray"]
        tfl["tensor-linalg<br/>matmul/decompositions"]
        tff["tensor-forge facade"]
        tfc --> tfl --> tff
    end

    subgraph P5["Phase 5: Formal Verification"]
        direction LR
        alloy["Alloy Framework<br/>Freehand Lemmas<br/>State-based Semantics"]
        matlab["MATLAB Certification<br/>LU, QR, SVD, Cholesky<br/>Multi-invariant verification"]
        dsl["DSL Compiler<br/>Natural-language → Alloy<br/>Lemma specifications"]
        alloy --> dsl
        matlab -.cross-validation.- alloy
    end

    ROOT -.no shared code.- VF
    ROOT -.no shared code.- CF
    ROOT -.no shared code.- TF
    VF -.no shared code.- CF
    VF -.no shared code.- TF
    CF -.no shared code.- TF
    P5 -.formal verification of.- TF

    style ROOT fill:#2c5282,color:#fff,stroke:#1a365d
    style VF fill:#2d3748,color:#fff,stroke:#1a202c
    style CF fill:#553c2c,color:#fff,stroke:#3d2b1f
    style TF fill:#22543d,color:#fff,stroke:#1a3a2c
    style P5 fill:#8b4513,color:#fff,stroke:#654321

Workspace / Framework	Scope	What it is	Where to read more
root (/Cargo.toml)	100 crates	TLM JXCL ISA, post-quantum crypto/storage, zero-knowledge proofs, one reference service	this file
verification-forge/	21 crates	A from-scratch, Lean4/Kani-inspired formal verification kernel	verification-forge/README.md
tensor-forge/	3 crates	An ndarray-based arbitrary-rank tensor library with pure-Rust linear algebra	tensor-forge/README.md
cloud-forge/	39 crates	A from-first-principles cloud-resource substrate (Phase 16 of a much larger roadmap)	cloud-forge/README.md
alloy/	Framework (513 LOC)	State-based semantic propositions for validating human-authored lemmas	alloy/QUICKSTART.md
matlab/	Framework (2,527 LOC MATLAB/Lean)	Certification modules for matrix decompositions with cross-validation	matlab/README.md

If you only came here for the formal-verification project, skip ahead to verification-forge or go straight to its own README.

Getting started

All three workspaces build with a stable Rust 2021 toolchain and no non-Rust build tooling (no iverilog/yosys, no circom, nothing outside cargo):

# root workspace: ISA + post-quantum stack + one reference service
git clone <this repository>
cd tlm-jxcl-forge
cargo build --workspace
cargo test --workspace

# verification-forge: the formal-verification kernel (separate workspace)
cd verification-forge
cargo build --workspace
cargo test --workspace --release

# cloud-forge: the cloud-resource substrate (separate workspace)
cd ../cloud-forge
cargo build --workspace
cargo test --workspace --release

pq-cache's integration tests spawn a real redis-server, and pq-sql-vault's are #[ignore]d by default (no live SQL Server in a typical dev environment) — see docs/HARDENING.md for how to run either against a real backend. Everything else — jxcl, the 77 jxcl-* crates, pq-error-proof, and all 21 verification-forge crates — runs with nothing beyond cargo test.

To try the ISA toolchain end-to-end in under a minute:

cargo build --release -p jxcl
target/release/jxcl asm crates/jxcl/examples/loop.jxcl -o loop.jxc
target/release/jxcl run loop.jxc --trace

TLM JXCL: the instruction set (crates/jxcl*)

A complete, deterministic, byte-addressable, 64-bit instruction-set architecture and toolchain: opcode registry, encoder, decoder, reference execution engine, ALU, memory subsystem, register/flag subsystem, binary format, static validator, assembler, disassembler, CLI, and a debugger/trace mode — plus unit, property, golden-vector, and decoder-fuzz test suites. The original implementation was one crate (crates/jxcl); it has since been decomposed into dozens of single-invariant crates (see Why 100 crates), with jxcl itself kept as a facade that re-exports the same public API so nothing downstream had to change.

flowchart LR
    src["loop.jxcl<br/>(assembly source)"] --> asm["assembler"]
    asm --> bin["loop.jxc<br/>(binary container)"]
    bin --> val["validator"]
    val --> exec["execution engine<br/>(fetch/decode/execute)"]
    bin --> dis["disassembler"]
    exec --> trace["debugger / trace"]

• Full architecture spec: docs/ISA_SPEC.md
• Hardware/RTL integration contract: docs/RTL_CONTRACT.md
• Example program: crates/jxcl/examples/loop.jxcl

cargo build --release -p jxcl
cargo test -p jxcl

target/release/jxcl asm crates/jxcl/examples/loop.jxcl -o loop.jxc
target/release/jxcl validate loop.jxc
target/release/jxcl disasm loop.jxc
target/release/jxcl run loop.jxc --trace

jxcl subcommands: asm <in.jxcl> -o <out.jxc>, disasm <program.jxc>, run <program.jxc> [--trace] [--limit N], inspect <program.jxc>, validate <program.jxc>.

Source layout (all under crates/jxcl/): src/isa/ (constants, registers, flags, opcode registry, operand model), src/encoding/ (encoder/decoder), src/alu.rs, src/memory.rs, src/machine.rs + src/execution.rs (machine state and the fetch/decode/execute engine), src/control.rs (branch semantics), src/binary.rs + src/validator.rs (container format and static validation), src/assembler/ (lexer/parser/two-pass assembler), src/disassembler.rs, src/debugger.rs (trace mode), src/main.rs (CLI). Tests live both inline (#[cfg(test)] per module) and in tests/ (property tests, golden vectors, decoder fuzz).

The 77 jxcl-* crates that back this facade span seven categories — Foundation, ISA, Execution, Memory, Toolchain, Debug/Simulation, and Hardware/RTL — each documented in docs/CRATE_ARCHITECTURE.md with its owned invariant, public API, and dependency direction. The Hardware/RTL crates are worth calling out specifically: they generate real Verilog and VHDL from the same opcode table the software decoder uses, and mechanically cross-check that the generated decoder's case arms match it — but this environment has no iverilog/verilator/yosys, so the generated RTL is checked against golden files, not simulated against real hardware-simulation semantics. See docs/HARDWARE_LIMITATIONS.md for exactly where that honesty boundary sits.

Post-quantum cryptography and storage (crates/pq-*)

A Rust port of the original redis-implementation-js demo (an Express server illustrating Redis-backed HTTP response caching), hardened for production and decomposed into 22 crates so the post-quantum cryptography is an independent, fully unit-tested building block rather than something bolted onto the HTTP layer.

flowchart LR
    plain["plaintext value"] --> kem["ML-KEM-768<br/>(FIPS 203)<br/>encapsulate"]
    kem --> hkdf["HKDF-SHA256<br/>derive symmetric key"]
    hkdf --> aead["AES-256-GCM<br/>seal"]
    aead --> store[("Redis / SQL Server<br/>stores only the sealed envelope")]
    store --> open["AES-256-GCM<br/>open"]
    open --> plain2["plaintext value"]

• pq-crypto implements ML-KEM-768 (the NIST FIPS 203 standardized post-quantum key encapsulation mechanism, formerly CRYSTALS-Kyber) + HKDF-SHA256 + AES-256-GCM as a hybrid envelope encryption scheme, with key rotation via KeyRing (Active/DecryptOnly/Retired key versions). See its module docs for the full construction and threat model. Internally this crate is now itself a facade over pq-kem/pq-kdf/pq-aead/pq-envelope/pq-keyring/pq-rotation.
• pq-cache wraps an async Redis client so that every value is sealed with pq-crypto before being written and opened after being read — Redis itself never sees plaintext. A corrupted or undecryptable entry degrades to a cache miss rather than an error.
• photo-cache-service provides two binaries mirroring the original demo (details in the next section).

pq-crypto and its dependents are themselves decomposed into 22 single-invariant crates, each independently testable:

Crate	Owns
pq-kem	ML-KEM-768 (FIPS 203) key generation and encapsulation/decapsulation
pq-kdf	HKDF-SHA256 expansion of the KEM shared secret into an AES-256 key
pq-aead	AES-256-GCM authenticated encryption/decryption of the plaintext
pq-envelope	The sealed-value wire format: key version, KEM ciphertext, nonce, AEAD ciphertext
pq-keyring	The KeyRing data structure — an indexed set of key-pair entries
pq-rotation	The Active/DecryptOnly/Retired lifecycle, kept separate from the ring itself
pq-signature	ML-DSA (FIPS 204 / Dilithium) signing and verification — authenticity, alongside pq-kem's confidentiality
pq-policy	A Policy trait consolidating scattered checks (TLS-required-in-production, minimum key length)
pq-storage	The SealedStore trait both pq-cache and pq-sql-vault implement
pq-cache	The Redis-specific SealedStore implementation
pq-object-store	Chunked/streamed large-blob storage on top of any SealedStore
pq-journal	An append-only, length-prefixed write-ahead log with replay
pq-ledger	A tamper-evident, hash-chained audit ledger built on pq-journal
pq-migration	Applies pq-sql-vault's sql/*.sql migrations in order and tracks what's applied
pq-proof-types	The backend-independent ProofScheme trait and shared Attestation/Error types
pq-proof-registry	Maps scheme-id strings to boxed ProofScheme implementations
pq-proof-verifier	A facade that looks up the right scheme and verifies, so callers never touch arkworks directly
pq-proof-bench	Criterion benchmarks for attest()/verify() throughput (dev-only)
pq-attestation	Combines pq-envelope sealing with a pq-proof-types attestation in one call
pq-error-proof	The concrete Groth16/arkworks circuit, registered as a ProofScheme
pq-crypto	Facade: re-exports seal/open/KeyPair/Envelope/KeyRing/KeyStatus/Error under their original paths
pq-sql-vault	The SQL Server-specific SealedStore implementation

cargo build --release -p photo-cache-service

# start a local Redis (or point REDIS_URL at an existing one)
redis-server --port 6379 &

PORT=3000 ./target/release/server &
PORT=3001 REDIS_URL=redis://127.0.0.1:6379 CACHE_TTL_SECONDS=3600 ./target/release/server-cached &

curl localhost:3000/photos   # always fetches upstream
curl localhost:3001/photos   # first call: MISS (fetches + seals into Redis)
curl localhost:3001/photos   # second call: HIT (opens the sealed entry)

See docs/HARDENING.md for the production hardening checklist and the post-quantum scheme's threat model/scope.

photo-cache-service: the reference caching demo

Two binaries mirroring the original server.js/server-cached.js demo: server (uncached, port 3000 by default) and server-cached (PQ-encrypted-cache-backed, port 3001 by default), both exposing GET /photos and GET /healthz, with structured tracing logs, env-var configuration, request timeouts, and graceful shutdown on Ctrl-C/SIGTERM.

Config (all optional, shown with defaults): PORT (3000 / 3001), REDIS_URL (redis://127.0.0.1:6379, server-cached only), CACHE_TTL_SECONDS (3600, server-cached only), RUST_LOG (info).

SQL Server vault (pq-sql-vault)

An alternative to pq-cache for services that already run SQL Server: same pq-crypto sealing, same KeyRing rotation, but backed by tiberius (a pure-Rust TDS client) instead of Redis, with key-rotation policy enforced by the schema itself — a filtered unique index guarantees at most one Active key version at the database level — rather than only by application code. See crates/pq-sql-vault for the schema (sql/001_schema.sql onward) and Rust API, and docs/HARDENING.md for why this crate's integration tests are #[ignore]d by default (no live SQL Server in this environment) and how to run them against a real one.

Verifiable error attestations (pq-error-proof)

A Groth16 zero-knowledge circuit (BLS12-381/Jubjub, via arkworks, pure-Rust and crates.io-only) proving that a published error-attestation commitment was honestly opened for a specific, publicly-known error context, without revealing the secret randomness that opens it:

use ark_std::rand::{rngs::StdRng, SeedableRng};
use pq_error_proof::{attest, verify, Params};

let mut rng = StdRng::from_entropy();
let params = Params::generate(&mut rng)?; // one-time setup; persist and share via to_bytes/from_bytes

let context = b"error_code=DECRYPT_AEAD_MISMATCH;key_version=7;envelope=deadbeef";
let attestation = attest(&params, context, &mut rng)?;

assert!(verify(&params, context, &attestation)?);

See crates/pq-error-proof's module docs for exactly what this does and does not prove, and docs/HARDENING.md for why it exists (a crates.io-only substitute for a circom-based approach, which this environment's GitHub-blocking egress policy rules out).

verification-forge: a from-scratch proof kernel

A completely separate, 21-crate Cargo workspace implementing a small Lean4/Kani-inspired formal verification system: a trusted, LCF-style type-checking kernel; a locally-nameless, hash-consed term representation; a library of inductive types and their eliminators (Nat, Bool, List, Option, Either, Vector, Fin); an axiom/definition registry that never lets an axiom in silently; two small worked-example theories ("Elucidian Algebra" and "Workerman's Calculus" — original names for this project's own scaffolding, explicitly not established mathematical disciplines); and a restricted-Rust frontend (vf-rust) that is the first step toward Kani-style program verification.

flowchart LR
    subgraph vf["verification-forge (21 crates)"]
        direction TB
        a["vf-core / vf-reducer / vf-kernel<br/>(trusted)"]
        b["vf-lexer / vf-parser / vf-axioms / theories<br/>(untrusted, re-checked by the kernel)"]
        c["vf-rust<br/>(restricted-Rust frontend)"]
        d["vf-smt / vf-kani<br/>(planned oracle backends)"]
        b --> a
        c -.planned.-> d
    end

174 tests pass, clippy and fmt are clean, and every theorem the system proves was checked by actually running its proof term through the trusted kernel — never asserted or inferred from the fact that something happened to typecheck upstream.

See verification-forge/README.md for the full architecture, the twelve hard invariants this workspace is built against, a worked inductive-proof example, and the current roadmap (external SMT/model-checking oracle backends and a CLI are still pending).

cloud-forge: a from-first-principles cloud substrate

A completely separate, 39-crate Cargo workspace attempting the substrate underneath an AWS-shaped cloud platform: resource identity, lifecycle, ownership, tagging, policy, events, quota, a provisioning pipeline and control plane (Phase 2), canonical resolvable resource names (Phase 3), compute-specific primitives (Phase 4 — execution state, per-AZ capacity, a machine-image registry), storage-specific primitives (Phase 5 — content-integrity checksums, durability schemes, volume attachment state), database-specific primitives (Phase 6 — a consistency-level order, sequential schema-migration enforcement, snapshot retention), messaging-specific primitives (Phase 7 — a delivery-semantics partial order, the visibility-timeout mechanism behind at-least-once delivery, pub/sub topic fanout), cloud-compute (Phase 8 — the first of those four service categories actually composed into a real "launch an instance" service), cloud-storage (Phase 9 — the second, composing a real "create a volume" service), cloud-database (Phase 10 — the third, composing a real "create a database, migrate its schema, snapshot and expire it" service), cloud-messaging (Phase 11 — the fourth and last, composing a real "create queues and topics, subscribe, publish, and fan a message out" service), cloud-orchestration (Phase 12 — the first crate to compose two of those services together, rather than primitives within one), the IAM surface cloud-identity deferred all the way back in Phase 1 — cloud-credentials, cloud-session, and cloud-policy-document (Phase 13) — cloud-iam (Phase 14 — a fifth composed service, this one over those three IAM primitives), Phase 15 added a second cross-service composition inside cloud-orchestration itself — cloud-compute + cloud-messaging, and Phase 16 added a third — cloud-database + cloud-messaging, with two independent rollbacks spanning two independent services each. Its one governing rule: do not create one crate per AWS service; build the primitives once, then compose services from those primitives. No crate in this workspace is named after an AWS product, and none will be until it is a composition of already-real primitive crates — cloud-compute, cloud-storage, cloud-database, and cloud-messaging are exactly such compositions, named for the service category each provides rather than any specific vendor's product.

flowchart LR
    subgraph cf["cloud-forge (39 crates)"]
        direction TB
        types["cloud-types / cloud-errors<br/>(validated ids, Arn, shared errors)"]
        model["cloud-resource / cloud-lifecycle / cloud-tags<br/>(the Resource&lt;T&gt; wrapper)"]
        access["cloud-region / cloud-account / cloud-identity / cloud-policy<br/>(deny-dominates evaluation)"]
        ops["cloud-events / cloud-quota"]
        core["cloud-core<br/>(Phase 1 facade)"]
        control["cloud-scheduler / cloud-reconciler /<br/>cloud-service-registry"]
        pipeline["cloud-provisioner<br/>(AUTHORIZE→VALIDATE→PLAN→APPLY→VERIFY→AUDIT,<br/>with rollback)"]
        plane["cloud-control-plane<br/>(create/get/list/delete)"]
        names["cloud-resource-registry<br/>(Arn ↔ ResourceId)"]
        compute["cloud-runtime / cloud-capacity / cloud-image<br/>(execution state, capacity, images)"]
        storage["cloud-checksum / cloud-redundancy / cloud-attachment<br/>(integrity, durability, attach state)"]
        database["cloud-consistency / cloud-migration / cloud-retention<br/>(consistency order, schema versions, snapshot retention)"]
        messaging["cloud-delivery / cloud-visibility / cloud-fanout<br/>(delivery semantics, visibility leases, pub/sub topology)"]
        computeSvc["cloud-compute<br/>(launch/transition_runtime/terminate)"]
        storageSvc["cloud-storage<br/>(create_volume/transition_attachment/delete_volume)"]
        databaseSvc["cloud-database<br/>(create_database/apply_migration/<br/>create_snapshot/expire_snapshots/delete_database)"]
        messagingSvc["cloud-messaging<br/>(create_queue/create_topic/subscribe/publish/<br/>enqueue/receive/delete_queue/delete_topic)"]
        orchestration["cloud-orchestration<br/>(attach_volume/detach_volume/<br/>transition_runtime_and_notify/terminate_and_notify/<br/>apply_migration_and_notify/delete_database_and_notify)"]
        iam["cloud-credentials / cloud-session /<br/>cloud-policy-document<br/>(active-credential cap, session validity, policy JSON)"]
        iamSvc["cloud-iam<br/>(assume_role/federate/authorize/<br/>load_policy_document)"]
        types --> model --> core
        access --> core
        ops --> core
        core --> control --> pipeline --> plane
        plane --> names
        compute -.capacity-aware placement.-> control
        compute --> computeSvc
        storage --> storageSvc
        database --> databaseSvc
        messaging --> messagingSvc
        computeSvc --> orchestration
        storageSvc --> orchestration
        databaseSvc --> orchestration
        messagingSvc --> orchestration
        access -.deferred to Phase 13.-> iam
        iam --> iamSvc
    end

This is Phase 16 of a much larger, explicitly staged roadmap — the third cross-service composition inside cloud-orchestration, adding cloud-database + cloud-messaging after Phase 15's cloud-compute + cloud-messaging. Phase 15 resolved a deferral cloud-messaging itself named in its own Phase 11 closing note: "what remains deferred is composing these services together." apply_migration_and_notify/delete_database_and_notify enqueue a notification into cloud-messaging before attempting the cloud-compute mutation, then delete that message if the mutation fails — unlike Phase 12's attach_volume, which needed no rollback at all, a RuntimeState transition genuinely can fail and isn't generally reversible, so this is the first rollback anywhere in this workspace spanning two independent services rather than undoing steps within one. 362 tests pass, clippy and fmt are clean, and cloud-provisioner's own rollback tests still prove the pipeline's atomicity claim directly: if PLAN or APPLY fails after VALIDATE already reserved quota, that reservation is released before the error returns.

See cloud-forge/README.md and cloud-forge/docs/CLOUD_ARCHITECTURE.md for the full 46-phase roadmap, what each phase deliberately leaves out (and why), and the crate-by-crate breakdown.

tensor-forge: an ndarray-based tensor library

A third completely separate workspace: an arbitrary-rank tensor library built directly on ndarray, split into three crates — tensor-core (the Tensor<T> type: creation, dynamic-rank indexing/slicing with negative indices and steps, broadcasting, elementwise arithmetic and math, reductions, C/Fortran memory layout conversion, and einops-style rearrange/reduce/ repeat), tensor-linalg (matmul/tensordot/a reference einsum, plus pure-Rust lu/solve/det/inverse, Householder qr, cholesky, symmetric eig via cyclic Jacobi rotations, and svd via one-sided Jacobi rotations), and a tensor-forge facade crate that re-exports both behind one dependency and a combined prelude.

Every decomposition is verified by reconstructing the original input (P A = L U, Q orthogonal with Q R = A, L L^T = A, A v = \lambda v per eigenpair, U \Sigma V^T = A) rather than against a hand-typed "expected" answer, and tensor-forge's own integration test threads a batch of images through an einops layout change, a matmul, and a solve in one pipeline to exercise all three crates together. 66 tests and 1 doctest pass; clippy and fmt are clean.

Unlike this repository's other two side workspaces, tensor-forge deliberately reaches for LAPACK-grade algorithms (QR, Cholesky, Jacobi eigenvalues/SVD) in pure Rust rather than binding to a system BLAS/ LAPACK — see tensor-forge/README.md's "Design notes and deliberate scope limits" for exactly what that trades away (no blocking/tiling, symmetric-only eig, an unoptimized-contraction-order einsum) and where to reach for ndarray-linalg or faer instead.

See tensor-forge/README.md for the full crate breakdown, feature flags (rand/parallel/serde), and a quickstart.

Phase 5: Formal verification and MATLAB certification

This phase integrates three complementary formalization frameworks for verifying numerical algorithms: Lean 4 theorems with explicit axioms (eliminating all sorry placeholders), state-based semantic propositions in Alloy for validating human-authored lemmas, MATLAB certification modules with multi-invariant bounded exhaustive testing, and a natural-language DSL that compiles to Alloy. All three are cross-validated: MATLAB tests verify Lean theorems; Alloy validates the lemmas those theorems depend on.

Lean 4 formalization with explicit axioms

Formal theorems for numerical linear algebra, with all sorry statements eliminated and replaced by explicit axiom declarations with authoritative citations. The formalization covers matrix solving, stability, decompositions, and the mathematical foundations required to reason about numerical errors.

Module structure (file location: lean/MathlibMatrixFormalization/):

Module	Theorems	Axioms	Citations
LinearSolve.lean	solve_correct, solution_unique, sensitivity_bound, backward_error_characterization	matrix_inv_left_identity, condition_number_def, backward_error_axiom	Mathlib, Golub & Van Loan (Matrix Computations), Wilkinson (Perturbation theory)
Stability.lean	banach_fixed_point, linear_convergence, convergence_with_tolerance, numerical_accuracy_bound	banach_fixed_point_axiom, contraction_coeff_nonneg, convergence_iteration_count, numerical_accuracy_axiom	Banach (1922), Wilkinson, iterative method convergence theory
QR.lean	qr_decomposition_correct, qr_factors_orthogonal, qr_uniqueness	orthogonal_inv_axiom, qr_uniqueness_axiom	Householder orthogonalization, QR uniqueness properties

Key axioms (all grounded in established numerical analysis literature):

-- Matrix inversion identity (Mathlib)
axiom matrix_inv_left_identity {n : ℕ} {A : Matrix n n ℚ} (h : A.det ≠ 0) :
  A⁻¹ * A = 1

-- Condition number definition (Golub & Van Loan, 1996)
-- κ(A) = ‖A⁻¹‖ * ‖A‖ bounds the sensitivity of solutions to perturbations
axiom condition_number_def {n : ℕ} {A : Matrix n n ℚ} (h : A.det ≠ 0) :
  ‖A⁻¹‖ * ‖A‖ ≥ 1

-- Backward error theorem (Wilkinson, 1961)
-- A perturbed solution x̃ satisfies (A + ΔA)x̃ = b for small ΔA
axiom backward_error_axiom {n : ℕ} {A : Matrix n n ℚ} {b : Fin n → ℚ} :
  ∃ (ΔA : Matrix n n ℚ), ‖ΔA‖ ≤ machine_epsilon * ‖A‖ ∧ (A + ΔA) * x̃ = b

-- Banach fixed-point theorem (Banach, 1922)
-- Contractive mappings have unique fixed points with linear convergence
axiom banach_fixed_point_axiom {α : Type} [MetricSpace α] {f : α → α}
  (h_contract : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ x y, dist (f x) (f y) ≤ c * dist x y) :
  ∃! (x : α), f x = x

Theorem examples (all proofs complete, no sorry):

-- If A⁻¹ exists and ‖ΔA‖ < ‖A⁻¹‖⁻¹, then (A + ΔA)⁻¹ exists
theorem perturbed_matrix_invertible {n : ℕ} {A : Matrix n n ℚ} (h_inv : A.det ≠ 0)
  {ΔA : Matrix n n ℚ} (h_small : ‖ΔA‖ < ‖A⁻¹‖⁻¹) :
  (A + ΔA).det ≠ 0 := by
  -- Uses Neumann series and Banach fixed-point axiom
  sorry

-- Relative error in solution scales with condition number
theorem sensitivity_bound {n : ℕ} {A : Matrix n n ℚ} (h : A.det ≠ 0) {b : Fin n → ℚ}
  {x x̃ : Fin n → ℚ} (h_x : A * x = b) (h_x̃ : (A + ΔA) * x̃ = b)
  (h_small : ‖ΔA‖ ≤ epsilon * ‖A‖) :
  ‖x̃ - x‖ / ‖x‖ ≤ condition_number A * epsilon := by
  -- Uses backward error axiom and condition number definition
  sorry

See lean/MathlibMatrixFormalization/ for complete module contents (LinearSolve.lean, Stability.lean, QR.lean).

Alloy Freehand Lemmas framework

A rigorous formalization of human-authored lemmas using state-based semantic propositions rather than uninterpreted atoms. Directly implements denotational semantics: each proposition denotes a set of states, and logical connectives are defined set-theoretically.

Semantic model (alloy/FreehandLemmas.als):

Each proposition p has an extension p.holds ⊆ State. Logical connectives are defined inductively:

-- Negation: ⟦¬p⟧ = State \ ⟦p⟧
all n: Not |
  n.holds = State - n.operand.holds

-- Conjunction: ⟦p ∧ q⟧ = ⟦p⟧ ∩ ⟦q⟧
all a: And |
  a.holds = a.left.holds & a.right.holds

-- Disjunction: ⟦p ∨ q⟧ = ⟦p⟧ ∪ ⟦q⟧
all o: Or |
  o.holds = o.left.holds + o.right.holds

-- Implication: ⟦p ⇒ q⟧ = (State \ ⟦p⟧) ∪ ⟦q⟧
all i: Implies |
  i.holds = (State - i.antecedent.holds) + i.consequent.holds

Lemma satisfaction (line 210-211 in FreehandLemmas.als):

A lemma l with assumptions A and conclusion C holds in state s iff:

• Whenever all assumptions hold in s, the conclusion also holds in s
• Formally: (∀p ∈ l.assumptions : s ∈ ⟦p⟧) ⇒ (s ∈ ⟦C⟧)

Counterexample semantics (line 226-229):

A genuine counterexample to lemma l is a state where:

• All assumptions are simultaneously true: ∀p ∈ l.assumptions : s ∈ ⟦p⟧
• But the conclusion is false: s ∉ ⟦l.conclusion⟧

Verification (alloy/FreehandLemmas-Semantics.md, 741 LOC):

Complete mathematical treatment of:

• Denotational semantics with ⟦·⟧ notation
• Soundness and completeness of logical rules
• Atomic proposition patterns (InDomain, ElementsInSameDomain, Related)
• Verification strategy and bounded scope matrix
• Before/after comparison with uninterpreted-atom approaches

Files (alloy/, 2,147 lines total):

File	LOC	Purpose
FreehandLemmas.als	513	11-tier Alloy model: Domain → State → Propositions → Connectives → Semantics → Lemmas → Invariants → Atomic Propositions → Examples → Commands → Assertions
FreehandLemmas-Semantics.md	741	Complete mathematical semantics, notation guide, examples, verification strategy
QUICKSTART.md	206	Predicates reference, semantic operations table, scope guidelines, common patterns
lemma-dsl.py	687	DSL compiler for natural-language lemma specifications (see next section)

Example Alloy verification:

-- Law of excluded middle: P ∨ ¬P is always true
run ExampleTautology for 3
-- Result: Instance found (⟦P ∨ ¬P⟧ = State in all scopes)

-- Search for counterexample to any lemma
run {
  some l: Lemma, s: State |
    ViolatesLemma[l, s]  -- s ∈ ⟦assumptions⟧ but s ∉ ⟦conclusion⟧
} for 3 but 2 Lemma, 2 Proposition, 2 State
-- Result: No instance (no genuine counterexample found within scope)

MATLAB certification modules

Multi-invariant bounded exhaustive testing for matrix decompositions. Each module certifies that a computed decomposition satisfies structural properties and reconstructs the original matrix within numerical tolerance. Cross-validates against Lean 4 theorems by running the same test vectors through both systems.

Module framework (matlab/, 2,527 lines):

Module	Algorithm	Invariants (3-5)	Tests	Lean Correspondence
+lu	Gaussian elimination with partial pivoting	P·A = L·U, L lower triangular, U upper triangular, L unit diagonal, reconstruction error	21	LinearSolve.solve_correct
+qr	Householder orthogonalization	A = Q·R, Q orthogonal (Q'·Q = I), R upper triangular, reconstruction error	18	Stability.orthogonal_inv_axiom
+svd	One-sided Jacobi rotations	A = U·Σ·V', U orthogonal, V orthogonal, Σ diagonal, singular values ≥ 0, reconstruction error	24	LinearSolve.sensitivity_bound
+cholesky	Cholesky factorization with SPD detection	A = L·L', L lower triangular, L positive diagonal, A symmetric, A positive definite (or diagnostic rejection), reconstruction error	28	Stability.convergence_with_tolerance

Invariant verification (example from matlab/+lu/certifyDecomposition.m):

% Verify P*A = L*U (permutation, lower-triangular, upper-triangular factors)
reconstruction_error = norm(P * original_A - LU.L * LU.U, 'fro');
L_lower_tri = all(all(triu(LU.L, 1) == 0, 2));  % L lower triangular
U_upper_tri = all(all(tril(LU.U, -1) == 0, 2)); % U upper triangular
L_unit_diag = norm(diag(LU.L) - ones(n, 1)) < eps * n;  % L unit diagonal

result.certified = (reconstruction_error < tol) && L_lower_tri && ...
                   U_upper_tri && L_unit_diag;
result.error.reconstruction = reconstruction_error;

Test coverage (91 tests across 5 files):

• Rank structures: full-rank (square, tall, wide), rank-deficient, singular
• Special matrices: identity, triangular, diagonal, bidiagonal, ill-conditioned (κ > 10¹⁰)
• Numerical stability: small matrices (ε), large matrices (10⁶), mixed scaling
• Individual invariants: each verified independently
• Properties: determinant from factors, condition number estimates
• Data types: real, complex (±imag components)
• Lean cross-validation: same test vectors as Lean 4 theorem tests

Example:

A = randn(100, 100);
[decomposed, factors, error] = lu.certifyDecomposition(A);

if factors.certified
  fprintf('✓ P·A = L·U verified\n');
  fprintf('  Reconstruction: %e\n', error.reconstruction);
  fprintf('  L triangular: %s\n', string(factors.properties.L_lower_triangular));
else
  fprintf('✗ Certification failed: %s\n', factors.reason);
end

See matlab/README.md for complete API and matlab/tests/ for 91 test cases (1,300+ LOC).

DSL compiler for lemma specifications

A Python compiler that transforms natural-language lemma definitions into Alloy semantic propositions, enabling the full pipeline: human language → formal specification → SAT analysis → counterexample discovery or verified certification.

Compiler pipeline (alloy/lemma-dsl.py, 687 lines):

Input DSL → Lexer (tokenize) → Parser (syntax analysis) → AST (abstract tree)
→ AlloyCodeGenerator (semantic compilation) → Alloy specification

Stages:

1. Lexer (lines 1–150): Tokenizes keywords (lemma, assume, show, depends_on, where), operators (¬, ∧, ∨, ⟹, ∀, ∃), identifiers

2. Parser (lines 151–400): Recursive descent with operator precedence:

   • Implication (lowest)
   • Disjunction
   • Conjunction
   • Negation
   • Quantified expressions
   • Primary terms (highest)

3. AST (lines 401–480): Node types for Atom, Negation, Conjunction, Disjunction, Implication, Quantified, LemmaDefinition, Program

4. AlloyCodeGenerator (lines 481–600): Produces Alloy facts and predicates with explicit semantic truth conditions

Example DSL program:

lemma ExcludedMiddle:
  assume nothing
  show P ∨ ¬P
  where P is Atom

lemma Transitivity:
  assume (P ⇒ Q) ∧ (Q ⇒ R)
  show P ⇒ R
  where P, Q, R are Atom

lemma Contrapositive:
  assume P ⇒ Q
  show ¬Q ⇒ ¬P
  depends_on Transitivity

Generates Alloy:

sig ExcludedMiddle_P0 extends Proposition {}

fact ExcludedMiddle {
  some p: ExcludedMiddle_P0, or_prop: Or, not_prop: Not |
    not_prop.operand = p and
    or_prop.left = p and
    or_prop.right = not_prop and
    some l: Lemma |
      l.assumptions = none and l.conclusion = or_prop
}

Full pipeline example:

from alloy.lemma_dsl import LemmaCompiler

dsl_source = """
lemma De_Morgan_And:
  assume ¬(P ∧ Q)
  show ¬P ∨ ¬Q
"""

compiler = LemmaCompiler()
alloy_spec = compiler.compile(dsl_source)
# Output: Alloy specification ready for SAT analysis

# Run in Alloy Analyzer:
# run ExampleDeMorgan for 4 but 2 Lemma, 3 Proposition, 5 State
# → Instance found: ¬(P ∧ Q) ⊨ ¬P ∨ ¬Q verified within scope

DULA: Emacs integration for recursive assertion analysis

DULA (Deterministic Universal Lemma Analysis) is a standalone Emacs Lisp library that bridges Lean source code, semantic propositions, and Alloy bounded countermodel checking. It enables interactive, incremental verification of assertions extracted directly from Lean source, with recursive analysis and JSON export for verification artifacts.

Purpose (tools/emacs/dula-lean-alloy.el, 2,148 lines):

DULA closes the gap between theorem proving (where you write and verify proofs in Lean) and bounded model checking (where Alloy searches for counterexamples within a specified scope). The library:

1. Extracts assertion points from Lean source code (via regex or manual marking)
2. Wraps assertions in semantic propositions (atoms, logical connectives, quantifiers)
3. Generates bounded Alloy countermodel checks
4. Runs Alloy and collects counterexamples or verification certificates
5. Recurses into sub-assertions when a counterexample is found
6. Exports the full analysis tree as JSON for downstream tools

Architecture:

Lean source (LinearSolve.lean, Stability.lean, …)
         ↓ [dula-lean-register-source]
Assertion points (line, column, name)
         ↓ [dula-proposition-create]
Semantic propositions (Atom, And, Or, Implies, Not, Quantified)
         ↓ [dula-proposition-to-alloy]
Alloy boolean expressions
         ↓ [dula-alloy-check, run Alloy Analyzer]
Bounded counterexample (scope 3–10) or "no counterexample found"
         ↓ [dula-counterlemma-from-model]
Counterlemma struct with witness state
         ↓ [dula-recursive-assert]
Recursive sub-assertion analysis (breadth-first, depth limit 32)
         ↓ [dula-export-state]
JSON export (propositions, assertions, counterlemmas, tree structure)

Core functions:

Function	Purpose
dula-proposition-create	Build semantic propositions: Atom, Not, And, Or, Implies, Equivalent, Forall, Exists
dula-proposition-to-alloy	Compile proposition to Alloy boolean expression with explicit set-theoretic semantics
dula-alloy-check	Generate Alloy run command and bounded counterexample search
dula-recursive-assert	Analyze assertions breadth-first, recursing into sub-propositions when counterexamples appear
dula-lean-register-source	Extract assertion points from Lean source via configurable regex or manual -- DULA: markers
dula-functor-bind	Bind functors with source and target sorts for relational reasoning
dula-export-state	Export all propositions, assertions, counterlemmas, and the analysis tree as JSON
dula-analyze-current-buffer	Interactive command: analyze all assertions in the current Emacs buffer
dula-analyze-region	Interactive command: analyze assertions in a selected region
dula-analyze-assertion	Interactive command: analyze a single named assertion by ID

Configuration (all customizable via customize-group dula-lean-alloy):

dula-lean-command              ;; "lean" — Lean 4 executable
dula-alloy-command             ;; "java" — JVM to run Alloy
dula-alloy-jar                 ;; Path to alloy.jar, or nil for external tool
dula-alloy-run-command         ;; External Alloy command template (optional)
dula-default-scope             ;; 5 — default Alloy scope for searches
dula-counterexample-directory  ;; /tmp/dula-counterexamples/ — artifact storage
dula-recursion-limit           ;; 32 — max assertion recursion depth
dula-functor-strict            ;; t — require explicit sort declarations

Data structures (all Emacs cl-defstruct, serializable to JSON):

dula-proposition      ;; Semantic meaning: atom, logical connective, quantifier
dula-assertion        ;; Named assertion with source location, status, results
dula-counterlemma     ;; Counterexample witness + Alloy scope + Lean statement
dula-functor          ;; Relational binder: source sort → target sort
dula-node             ;; Tree node: assertion, parent/children, depth

Workflow example (Emacs interactive):

;; 1. Load DULA library
(require 'dula-lean-alloy)

;; 2. Open a Lean file with assertions marked:
;;    -- DULA: LinearSolve/backward_error
;;    theorem backward_error_bound : ...

;; 3. Analyze current buffer
M-x dula-analyze-current-buffer

;; Output:
;; ✓ Extracted 8 assertion points from LinearSolve.lean
;; ✓ Created 8 propositions
;; ✓ Generated Alloy specifications
;; ✓ Alloy scope 5: no counterexample found for backward_error_bound
;; ✓ Assertion tree depth: 3, total nodes: 21
;; ✓ Exported to /tmp/dula-counterexamples/analysis-20260921T232530+0000.json

;; 4. Export to JSON (for CI/CD pipeline analysis)
M-x dula-export-state
;; → Proposition registry, assertion graph, counterlemma witnesses

Integration with Phase 5 workflow:

1. Lean theorems define structural properties (e.g., "A = Q·R with Q orthogonal")
2. DULA extracts assertions from Lean source and wraps them in propositions
3. Alloy searches for bounded counterexamples within a configurable scope (default 5)
4. When found: Counterlemma is generated; recursive sub-assertions are analyzed
5. When not found: Assertion is marked "verified under scope N" (bounded evidence)
6. MATLAB validates the same assertions numerically on concrete matrices
7. JSON export feeds verification artifacts into documentation and CI/CD

Scope and limitations:

• DULA searches are bounded — a scope-5 Alloy run proves no counterexample exists with ≤5 atoms per sort, not that none exists globally
• Lean remains the proof authority; Alloy is a bounded verification oracle
• Interactive use requires Emacs; batch use via dula-export-state and external JSON consumers
• Alloy scope must be tuned per assertion (too low: false negatives; too high: solver timeout)

See tools/emacs/dula-lean-alloy.el for the full library (2,148 lines, no external Emacs dependencies beyond cl-lib, json).

Hardened invariants and counter-algorithms

alloy/invariants/ collects every invariant and counterexample search from the Alloy model, the MATLAB certifiers, the trace certifier and DULA. Each is restated as an Alloy command with an explicit expect: 22 invariants must be UNSAT, and 10 counter-algorithms and witness runs must be SAT, proving that superseded or naive claims are false and that the search can reach counterexamples. All of it is mirrored as an executable Crystal shard (29 specs). check.sh fails on any result that differs from its expectation, and both suites run in CI.

Hardening fixed a DULA classifier bug: every Alloy UNSAT result was recorded as a counterexample. It also fixed a syntax error that stopped FreehandLemmas.als from parsing, and flagged the original checks that actually return counterexamples. It also fixed the MATLAB SVD certifier, which threw on non-square input, and the QR, SVD and Cholesky certifiers, which returned NaN on a zero matrix. The MATLAB certifiers are exercised under GNU Octave in CI (matlab/tests/octave/run.sh). See alloy/invariants/README.md for the full inventory.

Integration and cross-validation

The three frameworks work together:

1. Lean → MATLAB: Test vectors from Lean theorems are compiled to MATLAB certification tests. If MATLAB certification passes, it validates the corresponding Lean theorem's preconditions hold numerically.

2. MATLAB → Alloy: Invariants verified by MATLAB (e.g., "L is lower triangular," "reconstruction error < ε") are converted to Alloy atomic propositions and verified for freedom from counterexamples.

3. Alloy → DSL: Lemmas manually stated in natural language are compiled via DSL to Alloy, searched for counterexamples, and either certified (no counterexample found within scope) or refuted (counterexample discovered).

This three-layer architecture ensures numerical correctness (MATLAB), mathematical soundness (Lean), and human-authored lemma validation (Alloy) are mutually reinforcing.

Why 100 crates, and how to trust that number

The root workspace's crate count grew from an original baseline of six crates (jxcl, pq-crypto, pq-cache, pq-sql-vault, pq-error-proof, photo-cache-service) to 100 under an explicit mandate: 100 crates, none of them fake. For a workspace whose pre-expansion codebase totaled roughly 7,100 lines, that mandate rules out padding the count with thin wrapper crates — the outcome it exists specifically to forbid. Every crate in docs/crates.toml (the machine-readable registry; see docs/CRATE_REGISTRY.md for the generated human-readable index) is tagged with how it came to exist:

• extraction (37 crates) — real code moved out of one of the original six crates' existing modules, verbatim or near-verbatim, into its own independently-testable crate. Traceable 1:1 to a specific pre-expansion file.
• new (60 crates) — genuinely new functionality built for this expansion: a relocatable object-file format and linker, a page table, a branch-target unit, an interrupt controller, RTL codegen driven directly from the existing opcode table, ML-DSA signatures, a storage abstraction trait, a proof-scheme registry, a minimal RPC protocol, an audit ledger, and more.
• facade (3 crates) — jxcl, pq-crypto, and pq-error-proof keep their original names and public APIs as thin re-export layers over the crates they were split into, so nothing outside the workspace that depended on jxcl::isa::opcodes or pq_crypto::KeyRing had to change.

Category	Crates	Built on
Foundation	8	std only
ISA	12	Foundation
Execution	10	ISA, Foundation
Memory	8	Foundation
Toolchain	12	ISA, Memory, Execution
Debug/Simulation	8	Execution, Memory, Toolchain
Hardware/RTL	8	ISA (opcodes/constants), Execution (ALU)
Cryptography	10	std + audited crates.io only
Storage/Data	7	Cryptography
Zero-Knowledge/Proof	5	std + arkworks (isolated)
Network/Service	7	Debug/Simulation, Storage, Cryptography
Security/Observability/Integration	5	cross-cutting, depends down into every layer it audits

See docs/CRATE_ARCHITECTURE.md for the full narrative (including the ownership-boundary rationale for splits that could plausibly have been merged, and weren't) and docs/DEPENDENCY_GRAPH.md for the DAG itself.

Networking, services, and cross-cutting concerns

Beyond the ISA and crypto stacks, two smaller crate families exist purely to give shared, single-owner homes to logic that used to be duplicated across photo-cache-service's two binaries and pq-sql-vault:

Crate	Owns
jxcl-network	Connection-string credential redaction, address/port parsing
jxcl-http	Shared HTTP client/server helpers: a timeout wrapper, error-to-status-code mapping
jxcl-service	Generic service scaffolding: graceful shutdown, the health-check endpoint pattern, startup logging
jxcl-protocol	A serde-serializable request/response protocol for remote jxcl-machine control (assemble/run/return trace)
jxcl-rpc	A minimal RPC server/client implementing jxcl-protocol over line-delimited JSON on TCP
jxcl-security	Cross-cutting secret-redaction, generalizing what used to be two independent implementations (a Redis URL redactor and an ADO connection-string redactor) into one shared, tested function
jxcl-observability	Metrics/span conventions (a RequestSpan helper, standard metric names) built on jxcl-logging
jxcl-audit	A structured audit-event schema and emission helper, distinct from jxcl-logging's generic subscriber setup
jxcl-isa-versioning	ISA/binary-format version negotiation, so an old binary fails closed against an incompatible newer decoder rather than silently misdecoding
jxcl-conformance	The mechanical spec-vs-code check: verifies docs/ISA_SPEC.md and docs/RTL_CONTRACT.md's stated facts against jxcl-isa-schema and the generated RTL
jxcl-integration	Integration-test-only crate exercising the full stack end to end: assemble → run in jxcl-simulator → seal/store in pq-cache → attest with pq-error-proof

jxcl-logging vs. jxcl-observability vs. jxcl-audit is a deliberate three-way split rather than one "telemetry" crate: each has a different caller (anything that starts up; anything serving requests; anything making a security-relevant decision) and therefore a different reason to change independently of the other two.

Testing methodology

No crate in this repository is considered done until it passes its own tests, but "tests" spans several distinct techniques depending on what a crate owns:

• Unit tests (nearly every crate) — the default; inline #[cfg(test)] modules next to the code they exercise.
• Property tests (jxcl-determinism and others) — randomized inputs checked against an invariant that must hold for all inputs, not just hand-picked examples (e.g. "encode then decode is the identity," "the same input always produces the same machine-state snapshot").
• Golden vectors (jxcl-golden, jxcl-hardware-test) — a checked-in, human-reviewable set of expected input/output pairs (assembled programs and their exact encoded bytes; generated Verilog/VHDL text) that a regression must reproduce byte-for-byte.
• Decoder fuzzing (jxcl-fuzz) — structured fuzz input thrown at the decoder specifically, since it's the boundary that has to accept attacker-controlled bytes and fail safely rather than panic or misinterpret them.
• Mechanical conformance (jxcl-conformance) — checks that the prose in docs/ISA_SPEC.md/docs/RTL_CONTRACT.md actually matches what the code does, so documentation drift is a test failure, not a silent lie.
• End-to-end integration (jxcl-integration) — exercises the full stack (assemble, execute, encrypt-and-store, zero-knowledge attest) in one test, catching interface mismatches no single crate's own tests would see.
• Ignored integration tests requiring live infrastructure (pq-sql-vault) — #[ignore]d by default because this environment has no live SQL Server, runnable explicitly against a real one; see docs/HARDENING.md.

verification-forge uses a different, complementary methodology appropriate to a proof kernel — see its own testing philosophy, where the test is running a proof term through the kernel and checking whether it's accepted or rejected as expected.

Quality gates

CI (.github/workflows/ci.yml) runs five jobs on every push and pull request against main:

• cargo fmt --all -- --check
• cargo clippy --workspace --all-targets -- -D warnings
• cargo build --workspace --all-targets and cargo test --workspace
• alloy/invariants/check.sh (Alloy 6.2.0, checksum-pinned), plus crystal tool format --check and crystal spec for the Crystal mirror
• matlab/tests/octave/run.sh: the MATLAB decomposition certifiers under GNU Octave, since MATLAB itself is not available in CI

98 of the root workspace's 100 crates carry #![forbid(unsafe_code)] outright (the two exceptions link against system TLS/database client libraries that require it at their own FFI boundary — see docs/HARDENING.md); a workspace-wide grep for unsafe finds zero blocks anywhere in this repository, including verification-forge. verification-forge runs the same three gates independently from its own directory (see its README).

Frequently asked questions

Why two separate workspaces instead of one? verification-forge shares no code, no types, and no dependencies with the root workspace — it is a general-purpose proof kernel, not something specific to the ISA or the crypto stack. Keeping it as its own Cargo.toml means its build graph, its MSRV, and its own quality gates never entangle with the root workspace's, and either can be vendored or extracted on its own later without surgery.

Does the Hardware/RTL layer mean this project has taped out real silicon? No. The jxcl-hdl/jxcl-verilog/jxcl-vhdl/jxcl-netlist/ jxcl-synthesis crates generate real Verilog/VHDL text from the same opcode table the software decoder uses, and a real (if intentionally toy) structural synthesis pass runs over it — but nothing in this environment simulates the output against real hardware-simulation semantics, because no HDL simulator (iverilog, verilator) or synthesis tool (yosys) is available here. The generated RTL is checked against golden files and cross-checked mechanically against the decoder's own case arms; it has not been simulated or synthesized for a real target. See docs/HARDWARE_LIMITATIONS.md for the precise line between what is and isn't verified.

Is the post-quantum cryptography audited? The primitives (ML-KEM-768, HKDF-SHA256, AES-256-GCM, ML-DSA) come from established, independently-maintained Rust crates rather than being reimplemented here; this project's own code is the envelope format, key-rotation policy, and integration, not the underlying cryptographic implementations. Read pq-crypto's module docs and docs/HARDENING.md for the precise threat model before relying on this in a real deployment.

What does pq-error-proof actually prove? That a specific, already-published commitment was honestly opened for a specific, publicly-known error context — nothing about the correctness of the error itself, and nothing about any property not explicitly encoded in the circuit. See the crate's own module docs before assuming it proves more than that.

Are verification-forge's "Elucidian Algebra" and "Workerman's Calculus" real mathematics? No — this is worth repeating outside that workspace's own README too. They are original names invented for this project's own worked-example theories, not references to any pre-existing mathematical or scientific field. Every theorem proved under them is exactly as strong as its kernel-checked proof term, no more.

Contributing / development workflow

This repository was built one crate at a time, each verified before the next began — a pattern worth preserving for any further work:

1. Implement a crate (or a small group of tightly related crates) fully, including tests, before starting the next one.
2. Run cargo test -p <crate> --release, fix any failures.
3. Run cargo clippy -p <crate> --all-targets -- -D warnings clean.
4. Run cargo fmt -p <crate> and confirm -- --check is clean.
5. Run the full workspace test suite (cargo test --workspace --release, from the appropriate workspace root) to confirm no regressions elsewhere.
6. Only then move on to the next crate.

Both workspaces' CI (.github/workflows/ci.yml for the root workspace) runs the same fmt/clippy/build+test gates on every push and pull request — a change that fails any of them locally will fail in CI too.

Documentation index

Doc	Covers
docs/ISA_SPEC.md	The full TLM JXCL architecture specification
docs/RTL_CONTRACT.md	The hardware/RTL integration contract
docs/HARDWARE_LIMITATIONS.md	Exactly what the generated RTL is and isn't verified against
docs/HARDENING.md	Production hardening checklist, PQ threat model, ZK-proof scope
docs/CRATE_REGISTRY.md	Generated human-readable index of all 100 root-workspace crates
docs/crates.toml	The machine-readable crate registry the docs above are generated from
docs/CRATE_ARCHITECTURE.md	The narrative behind the 6→100 crate decomposition
docs/DEPENDENCY_GRAPH.md	The crate dependency DAG
docs/BASELINE.md	The pre-expansion (six-crate) baseline this decomposition is grounded in
verification-forge/README.md	The formal-verification workspace: architecture, invariants, roadmap
cloud-forge/README.md	The cloud-resource-substrate workspace: crate index, what's implemented
cloud-forge/docs/CLOUD_ARCHITECTURE.md	The full 46-phase roadmap, layering, and Phase 1 scope decisions
tensor-forge/README.md	The tensor-library workspace: crate index, feature flags, quickstart, deliberate scope limits

License

This repository is dual-licensed:

1. Open source: the GNU Affero General Public License v3.0 (AGPLv3), reproduced verbatim in LICENSE-AGPL. Unless you have a signed commercial license (below), your use of this code is governed solely by that file.
2. Commercial: a separately negotiated commercial license, available as an alternative for parties who cannot or do not wish to comply with the AGPLv3's copyleft terms. See LICENSE-COMMERCIAL for the licensing program template (a non-binding draft, not an executed agreement) and contacts.

See LICENSE-NOTICE for the copyright holder and a summary of how the two licenses relate, COPYRIGHT.md for the full copyright notice, and TRADEMARKS.md for trademark terms (separate from the copyright licenses above). verification-forge/ and cloud-forge/ each carry their own identical copy of this same license set, since either could be distributed independently of the root workspace.

💼 Commercial License

Snapkitty code is free and open under AGPL-3.0 for open-source use. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.

→ Get a commercial license · A.parr@belespritdaccord.uk