The Auditable Machine

Why critical software is structurally unauditable, and what homoiconicity has to do with it

The Problem Nobody Names

When ML-KEM — the post-quantum key encapsulation mechanism standardised by NIST — needed to land in OpenSSH, it took a path that should alarm anyone who thinks carefully about trust in critical software.

Cryspen wrote the implementation in Rust, constrained to the subset that the hax toolchain can process. hax extracted that code to F*, a proof assistant, where the proof was written and verified. The deployed code remains the original Rust — the proof establishes properties about it, but does not generate it. That Rust was then translated to C and integrated into OpenSSH by a different team, for a different codebase, with different assumptions.

Each step is defensible. The people involved are excellent. The result is probably correct.

But the trust chain is long, opaque, and polyglot. To audit the full pipeline you need to read Rust, F*, C, and assembly — four languages, four mental models, four sets of tooling. The auditor pool for all four simultaneously is vanishingly small. In practice nobody audits the full chain. They audit the parts they can read and trust that the translations are correct.

This is not a problem with Cryspen. It is a problem with how we build critical software.

Translation Is Where Trust Dies

Every translation between formalisms is a trust event. You are asserting that the thing on the left means the same as the thing on the right. Sometimes that assertion is mechanically verified. Often it is not. Even when it is, the verifier is itself a piece of software that someone had to trust.

The current crypto toolchain is a sequence of trust events:

At each step, something can go wrong in a way that is invisible to anyone looking at only one layer. The specification might not capture the real threat model. The extraction might introduce a subtle difference. The optimisation might break a timing invariant the proof never considered.

Formal verification is valuable. But formal verification of a model of your software is not the same as verification of the software that ships. The gap between the model and the artifact is exactly where the interesting failures live.

What Auditable Actually Means

An auditable system is one where a qualified person can read the source and develop justified confidence that the deployed artifact does what the source says it does.

By that definition, most critical software is not auditable. Not because it is poorly written, but because the path from source to artifact passes through too many transformations, too many languages, and too many teams for any one person to hold in their head.

The polyglot problem compounds this. Cryptographic audits are expensive precisely because you need rare people who understand the full stack. Firms charge accordingly. Governments and hospitals pay it, or skip it.

The solution is not better auditors. The solution is software that is structurally easier to audit.

Lisp as a Solution to a Problem It Did Not Know It Had

John McCarthy did not design Lisp with auditable cryptography in mind. He designed it around the lambda calculus and recursive function theory. The syntax — S-expressions, nested lists — followed from a mathematical formalism, not from engineering requirements.

But homoiconicity, the property that Lisp code and Lisp data have the same representation, turns out to be the key property you need to collapse the trust chain.

If code is data, then:

All of it is S-expressions. All of it lives in one language. All of it is manipulable by the same tools, readable by the same people, verifiable by the same passes.

A Lisp macro system is a program that writes programs. Which means it can write verifiers for the programs it writes. The proof is not a separate artifact in a separate language — it is a macro that runs at compile time and either passes or the whole thing does not compile.

The Two-Layer Architecture

The design this points toward has a clean boundary at its centre.

The compile-time layer is full Lisp. Expressive, dynamic, garbage collected, macros all the way down. This layer never ships. It is the construction environment — the place where you write the NTT butterfly network generator, the test vector emitter, the proof obligation checker. You can do anything here because none of it runs in production.

The value layer has Lisp syntax but completely different semantics. No garbage collection. No dynamic dispatch. Explicit integer widths. Flat memory. Constant-time primitives as first-class builtins. It is a typed portable assembler with parentheses. Macros in the compile-time layer expand into it. It compiles to IR and then to binary.

The compiler enforces that nothing from the compile-time layer leaks into the value layer. The boundary is a type-theoretic wall, not a convention.

This is not a new idea in isolation. Racket has a version of it with its phase system. The novelty is applying it specifically to the problem of auditable critical software, and making the boundary the security boundary.

Macros Are Compiler Passes

In a conventional compiler, you have a frontend that parses source into an AST, one or more middle-end passes that transform and optimise the AST, and a backend that emits code. Each pass is a separate program, usually in a different file, sometimes in a different language.

In the homoiconic model, macro expansion is the compilation. Each macro takes S-expressions and emits IR fragments directly. There is no separate AST representation, no lowering passes, no translation. The macro expansion is the compilation.

This works because assembly — and LLVM IR, its typed intermediate cousin — is already the most data-like form of code that exists. It is a flat list of operations with explicit operands. No implicit control flow, no hidden state, no syntactic sugar.

mov rax, rbx
xor rdi, rdi
ret

Is just:

(mov rax rbx)
(xor rdi rdi)
(ret)

Mechanically. No information lost. The structure is already there, waiting for a syntax that makes it explicit.

A compiler is fundamentally a program that transforms one list of instructions into another list of instructions. Homoiconicity means your transformation language and your target representation are the same thing. You are not translating between formalisms. You are rewriting lists.

The Audit Trail Is the Expansion Trace

Every macro expansion in a Lisp system can be printed. You can ask the compiler to show you every step — what the source looked like, what each macro produced, what the final IR was. This is standard Lisp tooling.

In the homoiconic critical software model, that expansion trace is the audit trail. An auditor does not need to understand the macro system in depth to audit a specific primitive. They read the source macro, they read the expansion, they read the IR, they read the certificate. All in one language. All traceable. All checkable.

This is a different audit than reading a proof in F* — arguably more practical, because it covers the artifact that actually runs rather than a model of it, but weaker in the formal sense because it does not provide mathematical guarantees over all possible inputs. It is a weaker audit than full formal verification. For most practical purposes it is the right point on the tradeoff curve — checkable by people who are not proof assistant specialists, grounded in the binary that ships.

Closing the Loop: Binary Taint Validation

IR-level correctness is necessary but not sufficient. LLVM's optimizer is aggressive. It will transform your carefully constant-time IR into variable-time machine code because from its perspective a branch is faster than a branchless select. Both are correct from a performance standpoint. One is catastrophic from a timing standpoint.

The guarantee you want lives at the binary level, not the IR level.

Binary taint analysis tracks which values in the compiled binary are derived from secret inputs, and verifies that no secret-tainted value ever reaches a branch condition or a memory address computation. If it does, you have a timing leak. If it does not, you have a constant-time proof for that binary on that architecture.

In the homoiconic pipeline, this validation pass runs after compilation and emits a certificate — a machine-checked proof over the actual binary that ships, not a model of it. That certificate is itself an S-expression. It is part of the same artifact as the source.

The full pipeline:

source → macro expansion → IR → binary → taint certificate

Four steps. One language for the first three. The certificate closes the loop between the source-level proof obligations and the deployed artifact.

Why This Is Bigger Than Cryptography

Post-quantum cryptography is the domain that made this problem visible. But the problem is general.

Any critical system where the gap between specification, implementation, and verification is bridged by translation across languages and teams has the same structural vulnerability. Voting systems. Medical device firmware. Financial settlement logic. Electronic patient record systems.

The pattern is always the same: a critical system where correctness matters enormously, verified by translating across multiple formalisms and trusting each translation, audited by people who can only see part of the chain.

The homoiconic model is a general answer to that problem. The Lisp is the vehicle. The property it delivers — one language, one artifact, one trust boundary, machine-checked end to end — is what critical software has always needed and never had a clean path to.

What Does Not Exist Yet

This is a thesis, not a system. The pieces exist in isolation:

What does not exist is a system that composes them under a single homoiconic roof, with the compile-time/value-layer boundary enforced by the type system, and the expansion trace as the primary audit artifact.

That is the thing worth building.

Draft. Written to capture the shape of an argument before it fades.