Establishing it once, then re-checking on every build

Correctness is established by proof rather than by measurement. The obligation is discharged once, and re-verified automatically on every build.

One specification, carried down to the fabric

The Futamura projections establish that interpreters, compilers, and compiler generators are not different kinds of artifact. They are points on one continuum, connected by specialization, a result set out by Yoshihiko Futamura in 1971. LOGOS acts as a single executable specification at every level, so each lowering step is a transformation between representations of the same specification rather than a translation between unrelated languages.

One specification, lowered through four levels to the chipAn inverted pyramid, apex down, cut into four layers. The LOGOS source is the wide base at the top. Below it the interpreter, then the register virtual machine, each layer narrower by exactly the ratio its height is lower, because every cross-section of a pyramid is similar to the base. The dataflow tiles are the tip, and from the tip a beam lands on a chip drawn as an eight by eight grid of tiles, the spatial compute fabric. Each transition between layers carries a discharged proof obligation that semantics are preserved.01020304

  1. Source

    LOGOS, the executable specification

    Proof obligation dischargedsemantics preserved

  2. Interpreter

    Reference semantics, software

    Proof obligation dischargedsemantics preserved

  3. Register VM

    Sequential execution model

    Proof obligation dischargedsemantics preserved

  4. Dataflow tiles

    Spatial placement, physical fabric

    The tip lands on the chip.

ProvenZero counterexamples

Every lowering discharges its proof obligation in our proof kernel, and the 8x8 run of the int8 matmul primitive matches an independent reference oracle, checksum 510,720. The kernel behind that proof finishes families Z3 and Kissat do not.

The specification is lowered through four levels, from the LOGOS source to the dataflow tiles, and the tip of that lowering lands on the spatial compute fabric. Each lowering carries a discharged proof obligation that semantics are preserved, which is what makes the bottom level something to rely on rather than something to test.

Evidence

Four vectors that fail independently

Correctness is established by four independent validation vectors, one at each layer of the lowering above, all served by one toolchain. The independence is the point: each can fail without the others noticing, so agreement across all four is evidence no single method provides.

LOGOS Supercompiler

one language, English. one tool, LOGOS.

  1. Specify

    One executable source

  2. Compile

    Placement onto the fabric

  3. Prove

    Obligations discharged

  4. Check

    Re-derived independently

Four layers of one chip, pulled apart, each checked by its own vectorFour square layers seen from a low camera, pulled apart so each can be read: the source, drawn as lines of English; the interpreter, drawn as an evaluation tree; the register virtual machine, drawn as a register file; and the dataflow tiles, drawn as an eight by eight grid. One beam drops from the toolchain through the center of every layer, glowing where it lands, and dashed guides between the corners show that the layers stack into one chip. From the right, four probes touch the four layers, one each, numbered to match the list below.01020304

  1. Layer 01.

    Source

    LOGOS, the executable specification

    checked by Formal SAT solving

    Exhaustive across the primitive's input boundaries

    from the toolchain: the specification parsed to logic, and the obligations the lowering opens

  2. Layer 02.

    Interpreter

    Reference semantics, software

    checked by Reference oracle

    Continuous comparison, independent implementation

    from the toolchain: the interpreter's run of the same source, held against a separately written implementation

  3. Layer 03.

    Register VM

    Sequential execution model

    checked by Soft core RTL

    Simulated against the same reference

    from the toolchain: the same program in its sequential form, and the reference to hold it to

  4. Layer 04.

    Dataflow tiles

    Spatial placement, physical fabric

    checked by Physical fabric

    Executed on hardware, results read back over UART

    from the toolchain: the placement onto the fabric, flashed over JTAG

one language, one toolThe specification is written in English. LOGOS carries it down through every layer, and the meaning does not change on the way. What every layer computes is the int8 quantized matmul primitive: the same program, in another form.

agreementFour layers, four independent readings of one primitive. The methods share no failure mode, so agreement across them is evidence that no single method establishes on its own.

One chip pulled apart into its four layers, from the English source down to the dataflow tiles, with one toolchain serving one check at every layer: exhaustive solving at the source, a separately written implementation against the interpreter, RTL simulation against the sequential model, and execution on hardware for the fabric. Because none of the checks shares a failure mode with another, agreement across all four is stronger evidence than any one of them repeated. The scope is the int8 quantized matmul primitive, not arbitrary programs.

What the four vectors establish

For the int8 quantized matmul primitive, lowering preserves the semantics of the reference, verified across four independent vectors. Manufacturing signoff comes back with zero DRC, LVS, antenna and routing violations under Sky130 signoff parameters.

The prover

Certificates in milliseconds, not Z3

An obligation is only worth stating if it can be discharged inside a build. LOGOS carries its own prover, written in Rust with no Z3 dependency, and it runs the same in a browser as it does in CI. Every verdict it returns is a certificate that is re-checked, not a result taken on trust.

On structured problems it's not competing on tuning. Resolution based solvers inherit a lower bound proved by Haken in 1985: certain families require proofs of exponential size, so no amount of engineering finishes them. The prover works in proof systems where those families are small, which is a difference in kind rather than in speed.

Measured on an Intel Core i9-14900K against byte identical input, median of five runs, with each competing solver writing its proof to disk. Kissat 4.0.4, CaDiCaL 3.0.0, CryptoMiniSat 5.11.21.

The same benchmark set includes a control: random 3-SAT, where there is no structure to exploit.

Source: LOGOS prover benchmarks, full families and methodology, logicaffeine.com(opens in a new tab)

Pigeonhole principle at 16 holes, time to decide and certificate size by solver
SolverPigeonhole, 16 holes
LOGOS13.7 ms, with a 25 KB certificate
SaDiCaL56.5 ms, with a 242 KB proof
Z3did not finish within 10 s
Kissat, CaDiCaL, CryptoMiniSatdid not finish within 15 s

Not a novel idea, a novel target

Formally verified compilation is an established qualification credential. CompCert, a formally verified C compiler commercialized by AbsInt, is used to earn certification credit under DO-178C in avionics. The proposition that a compiler can carry a proof is settled. Applying it to spatial dataflow architectures is the contribution here.

Source: CompCert, AbsInt Angewandte Informatik(opens in a new tab)

Does this apply to the silicon you are building?

Who we build for