Datacenter.Dev develops a compile to silicon pipeline for spatial dataflow architectures. The toolchain maps a model onto a routing fabric and produces a machine checkable proof that the mapping preserves the semantics of the reference implementation.
An 8x8 int8 matmul, compiled and executed in this browser.
Point at any tile, or use the arrow keys, to see the eight products it accumulated.
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 all of that work is about making the model run.
Source: KernelEvolve, Meta, arXiv:2512.23236(opens in a new tab)
A bring-up isn't finished when the model runs. It's finished when someone can say the numbers are the reference's numbers, and that is still established empirically, by generating candidate lowerings and selecting them by measurement. 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 testing does not establish their absence.
The Futamura projections established that interpreters, compilers, and compiler generators are not different kinds of artifact. They are points on one continuum, connected by specialization. LOGOS acts as a single executable specification across the software interpreter, the register virtual machine, and the physical dataflow tiles. Specializing it to the fabric yields a circuit rather than an executable.
The compiler places computation onto routing tiles instead of sequencing it through fetch and decode, so the datapath settles rather than stepping. Correctness is established by four independent validation vectors: physical fabric evaluation, formal SAT solving across input boundaries, soft core RTL simulation, and continuous comparison against an independent reference oracle. Their scope is the int8 quantized matmul primitive, not arbitrary programs.
The four validation vectorsFormally verified compilation is already a purchasing credential elsewhere. CompCert, commercialized by AbsInt, is used to earn certification credit under DO-178C in avionics. Applying it to spatial silicon is the new part.
Source: CompCert, AbsInt Angewandte Informatik(opens in a new tab)
| Result | Conditions |
|---|---|
| 8x8 GEMM checksum 510,720 | Byte identical to an independent reference oracle |
| 128-MAC dot product checksum 349,504 | Byte identical to an independent reference oracle |
| 15,725+ passing regression tests | Runs inside existing build pipelines |
| Zero DRC, LVS, antenna, and routing violations | Under Sky130 ASIC signoff parameters |
| Physical validation platform | Nexys A7-100T, Artix-7, JTAG flashed |
A proof you hold is an asset that outlives a vendor relationship. It re-runs on your builds, on your substrate, against your reference, and it does not expire when a support contract does. Describe your target substrate and the properties you need established.