Most of the terms below belong to the field rather than to us. One does not: the Verification Wall, which sits beside the verification gap, an established EDA term, and gets merged with it. Each entry here stands on its own, so a definition quoted away from this page still says what it means.
The Verification Wall is the point past which more testing stops raising confidence that a compiled model computes the same numbers as its reference. It is not the verification gap, which is a shortfall in verification throughput that closes with more engineers and better methodology. More testing does not move this limit, because testing cannot show the absence of silent miscompilation. It reopens on every model release and every new target.
The argument behind this definition, the objections it raises, and the sources under them are set out on the Verification Wall.
The verification gap is the established EDA term for the shortfall between how much design capacity a team can produce and how much of it they can verify in the time available. Verification consumes 60 to 70% of engineering effort in chip projects, per Wilson Research Group functional verification study data, and the gap responds to additional engineers, better methodology, and improved tooling. Not all of that effort is testing. Logic equivalence checking proves a netlist implements the RTL it came from. Formal property verification proves a stated property holds on every input. Both are ordinary practice, and both need something written down to check against, an earlier design or a property somebody wrote. A trained model's numerics are neither, which is where the Verification Wall sits. The gap is a throughput problem and it closes with more people. The wall doesn't: it's a limit on what testing can establish in principle.
Both terms are worth keeping. A team that closes its gap verifies more design per quarter, which is real and worth paying for, and it then arrives at the same limit on what any amount of that verification can conclude. Closing the gap is how you reach the wall sooner.
Silent miscompilation is a compiler fault that produces incorrect results without raising an error. Wrong numbers, no crash, no stack trace, so a passing test campaign is evidence about the inputs somebody chose and nothing more. The PolyJuice study found 84 miscompilation bugs, 49 confirmed, across seven tensor compilers including PyTorch Inductor, ONNX Runtime, TVM, TensorRT, and XLA. It's the failure mode testing cannot rule out.
Model lowering is translating a trained model into an executable form for a target, in this case placing it onto an existing fabric. It's established correct today by differential testing against a reference implementation, coverage over representative inputs, and engineering judgment about sufficiency. Getting the model running is largely a solved problem. Bringing one up on non-standard silicon is measured in weeks to months, and most of that window goes to establishing that the lowering is correct rather than making it run.
What that window is actually spent on, and which part of it a proof takes away, is on model bring-up on new silicon.
A settled datapath is a spatial arrangement in which a result is available once signals settle, rather than after a sequence of fetch and decode steps. A conventional core fetches, decodes, and sequences; the compiler places computation onto routing tiles instead, so the datapath settles rather than stepping through instructions. Correctness then becomes a property of the placement, which is something a compiler can be made to prove.
The Futamura projections establish that interpreters, compilers, and compiler generators are not different kinds of artifact. They're points on one continuum, connected by specialization, a result set out by Yoshihiko Futamura in 1971. Specialize an interpreter to a program and you get an executable; specialize the specializer to an interpreter and you get a compiler; specialize the specializer to itself and you get a compiler generator. Specializing against a spatial dataflow fabric rather than an instruction set yields a circuit rather than an executable.
The three constructions, what each one yields, and where the projections are already load bearing in production systems are set out on Futamura projections in silicon.
Datacenter.Dev Supercompiler is a compile to silicon pipeline for spatial dataflow architectures. It places computation onto a routing fabric and produces a machine checkable argument that the placement preserves the semantics of the reference. The name is the algorithm's: a supercompiler drives a program symbolically one step at a time, folding when it meets a configuration it has seen before and generalizing when it detects a homeomorphic embedding. Driving is ahead of time only, so no run time figure is attributable to it.
What the pipeline does at each stage, and what it emits at the end, is on the Supercompiler platform.
The LOGOS Proof Kernel is the trusted core of the toolchain: a Calculus of Constructions type checker in pure Rust that re-checks every proof the rest of the stack proposes. The parser, the proof search, the arithmetic normalizer, and the English front end propose; the kernel disposes. A certificate carries a proof term, its claimed type, and a prelude version, serialized as JSON, so a party who trusts none of our code can re-check it.
The layers the kernel checks, and the one place its trusted base is assumed rather than proven, are on the LOGOS Proof Kernel.
If a definition is the short form, where is the argument?