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.
Getting a model running on novel silicon is largely a solved problem. SambaNova's SambaFlow ships an O0 operator mode whose documented purpose is initial bring-up and model testing, and Meta reports that KernelEvolve takes kernel work that previously required weeks of specialist effort down to hours. That progress is real, and any account of this problem that ignores it isn't worth reading.
The question that remains is not whether a model runs. It's whether what it computes is what the reference computes.
Those methods establish correctness empirically. They generate candidate lowerings and select among them by measurement, which is a search scored by testing. The result is fast and it's not a proof.
The distinction matters because the failure mode is silent. The PolyJuice study found 84 miscompilation bugs, 49 confirmed, across seven tensor compilers including PyTorch Inductor, ONNX Runtime, TVM, TensorRT, and XLA. Such faults produce incorrect results without raising an error, and no quantity of passing tests establishes their absence.
Where more testing stops helping
This is not a problem specific to model compilation. It's a property of any lowering step whose correctness is established by sampling inputs rather than by proof, and that happens twice in this industry.
Neither end is short of formal tooling. Logic equivalence checking proves that a netlist implements the RTL it came from, over every input, and it's ordinary signoff practice. It works because both sides are the same kind of object. Nothing in production does the same for a tensor program and the kernel a compiler lowered it to, or for a specification written in prose and the RTL somebody wrote from it.
Those are the two steps testing has to close, one at each end, and both stop at the same limit.
Model bring-up
Design signoff
Model bring-up lowers: A trained model onto an existing fabric
Design signoff lowers: RTL onto a mask set
Model bring-up costs: Weeks to months before the fleet earns
Design signoff costs: The most expensive phase of the project
Model bring-up fails as: Silent miscompilation
Design signoff fails as: A respin
Method
Testing, in both cases. Run the artifact on inputs somebody chose, and compare what comes out against a reference. One side calls that differential testing, the other calls it simulation and coverage closure. The tools have different names. What the evidence can support does not.
The Verification Wall
Reached from both directions, because the method is the same one.
Proved silicon
A lowering established for every input, not the inputs somebody chose. No quantity of testing reaches it.
The verification gap is a throughput problem. It describes verification consuming 60 to 70% of engineering effort in chip projects, the figure reported from Wilson Research Group functional verification study data, and it responds to additional engineers, better methodology, and improved tooling.
The Verification Wall is a limit on what testing can establish in principle. It does not respond to either. The two terms are frequently conflated, and treating them as interchangeable is the most common mistake made in this area.
Both terms are written out side by side, with the ones they get used alongside, in the glossary.
Keeping the terms apart is not a reason to address only one of them. They have the same root cause, which is the method used to establish correctness, and that is what the toolchain replaces.
The gap is measured in effort spent establishing correctness: testbenches, coverage closure, regression campaigns, and the engineering judgment about when enough is enough. The wall is the limit on what that effort can conclude no matter how much of it you buy.
A proof addresses both, for the same reason. It establishes what the campaign could not, which is the wall. And it removes the need to run the campaign in order to be confident, which is most of what the gap was counting. The proof is produced once and re-verified on every build, so the cost moves from a phase in the schedule to a step in CI.
What makes such a proof stateable at all is an old result. The Futamura projections relate interpreters, compilers, and compiler generators by specialization, and specializing against a spatial dataflow fabric rather than against an instruction set yields an arrangement of hardware rather than another program. The specification the interpreter runs is the one the tiles are placed from, so there is a single artifact for the obligation to be about instead of three that have to be kept in agreement.
The distinction is definitional. A throughput limit closes with resources, and a limit on what testing can establish does not. A proof addresses both, because it replaces the work of establishing that a lowering is correct, which is the largest line item in the campaign.
There is a wave building behind this wall. Model releases arrive on a shorter cycle than they used to, and each one lands on a wider spread of targets than the release before it.
The wall does not move. That is what makes it a wall, and it's why the work piles up behind it rather than breaking through. The obligation reopens on every model release and on every new target, so the number of lowerings a team has to establish is the product of two lists that are both getting longer, not the sum.
A verification campaign is scoped to one model on one target. Nothing it concludes carries to the next pair, which is why adding engineers moves the gap and leaves the wall where it was. The difficulty is not that any single campaign is hard. It's that campaigns do not amortize, and the number of them grows on both axes at once.
A proof changes that shape. It's established against the specification rather than against one pair, and it re-runs in CI rather than being rebuilt by hand. The timing argument is not that the wall became worse. It's that everyone now meets it far more often.
If testing cannot establish it, what can?