Verification & reproducible builds
Flux ships nothing it has not first proven equal to its own reference. This page is the single home of the machinery that proves it: the verification harness and its blocking sub-suites, the hostile corpus they run on, the reproducible-build gate that seals a distributable module, and the formal properties the grammar and its semantics are frozen against. The contract all of this verifies — the two engines, the I6/I7 byte-identity invariants, the pinned routines and the pinned toolchain — is specified in Compiler and runtime; this page restates it only as far as the checks need.
The determinism these checks assert is bit-identical compute and a deterministic scene: the same numbers and the same draw-list on every machine, never identical pixels. The GPU and the compositor are outside the oracle by design; verification is over the values a program produces and the geometry it emits, not over the rendered frame.
New here? Start with Guide §11 — Determinism, replay and trust → — the same machinery, told for the reader who has to decide whether to trust it.
The contract under test
Flux runs on two engines: a graph interpreter serves the editor, the live preview and the debugger; a compiled WebAssembly module serves the run and distribution. Together they are one abstract machine — the FVM — and the pipeline, the engine roles and the runtime surface that binds them are specified in Compiler and runtime. What this page owns is the machinery that checks their agreement, at every compilation and at every build. The two invariants under test, each in one line:
- I6 — a leaf is byte-identical to its kernel. A node that maps to a native kernel produces exactly the bytes that kernel produces, warm-up included.
- I7 — the interpreter and the module agree, byte for byte. At every compilation the interpreter (the oracle) and the instantiated module (the candidate) are compared byte-wise on every sink column — first in batch, then live, bar by bar through the incremental step, then on any real data supplied. Any divergence blocks the compilation: the module is not shipped, and the interpreter keeps serving.
Figure — the gate compares the two engines on adversarial data, in batch and live, before a single byte is allowed out.
The comparison is only as strong as the data it runs on, so the corpus is hostile, deterministic and adaptive: series longer than the program’s resolved maximum lookback, seeded with holes, ±infinity, negative zero, raw non-canonical NaN patterns, exact half-integers, flat runs, monotone runs, magnitudes at 1e±9. The zones are chosen to land on the inputs where two correct-looking engines genuinely disagree — NaN payloads, signed zeros, rounding ties — and the same corpus drives the optimizer’s translation validation, whose oracle is the canonical evaluation of the unoptimized graph (optimizer).
The rest of the contract is summarized here and defined elsewhere, deliberately: the gate mechanics — why the live path is checked as well as batch, and how the browser compiles in a worker so divergent bytes are never handed back — sit with the pipeline in Compiler and runtime, alongside the pinned routines (one shared implementation of the transcendentals, rounding, na, decimal, strings, calendar and rand, on both engines) and the pinned Binaryen toolchain that make the emitted bytes a pure function of (program, toolchain). The harness below verifies exactly that mechanism; it does not re-specify it.
The verification harness
The harness is a first-class deliverable, not a folder of tests. Each sub-suite declares its oracle, its corpus, and whether it blocks the ship:
| Suite | What it asserts | Blocking |
|---|---|---|
| Goldens | every example is a deterministic golden; an unchanged golden stays byte-identical | yes |
| Properties | principality, confluence (the kind is invariant under any topological order), incremental re-typing ≡ full inference, totality, causality, the memory plan is a deterministic function of the graph with peak ≤ sum | yes |
| Fuzz + a well-typed generator | the parser and the type checker are total (any input yields one tree or a clean rejection); the generator samples the frozen grammar and the lattice to emit type-correct, causal graphs that feed the oracle | yes, once it feeds the oracle |
| Differential oracle (three ways) | interpreter ↔ WASM ↔ native kernel — covering I6, optimized ≡ reference, and I7 | yes |
| Metamorphic | the enumerated semantics-preserving relations: optimized ≡ reference · interpreter ≡ WASM ≡ server · 1 ≡ N workers · peak-plan ≡ sum-plan · confluence under any topological order · recompile ≡ recompile, byte-identical · the absolute draw-list is invariant to target and sequence | yes |
| Stress 1 ≡ N | the same graph under one worker and under many, with randomized adversarial assignment: identical output bytes, and no concurrent slot write | yes |
| Lattice enumeration | the laws and every admissibility judgment, enumerated per family | yes |
| Capability monitor | “no command outside the manifest is ever executed” — the one component that earns a model check | yes |
| Bench / budget | calibrates the cost model with measurements; guards the idle-compile budget; checks that the runtime peak equals the planned peak | advisory |
The Bench suite is advisory by intent: it calibrates the cost model against measurement and confirms the runtime peak equals the planned peak, but it never gates a ship. The certified speed numbers live with the benchmark, in Compiler and runtime §Performance — reported there, never asserted here.
One subtlety is worth stating: the three-way oracle calls the same pinned routine on all three sides, so it is blind to a bug inside a pinned routine. That is why each pinned routine also carries a second, independent reference implementation, compared bit for bit on fuzzed input. The oracle catches disagreement; only a second implementation catches a shared mistake.
Reproducible builds
The build hash is a pure function of: the source, the lockfile (the transitive closure of dependency hashes), the compiler version, the pinned routines, and the canonical memory plan.
Pinning the inputs is necessary but not sufficient, so the rebuild gate closes the gap: it recompiles the same source and lock twice, on different machines and with different thread counts, and asserts the emitted module is byte-identical to the stored hash. A non-reproducible build would break replay silently, because a value-level oracle cannot see the bytes emitted across two compilations.
Figure — three independent evaluations of one run must land on the same bytes; two legs ship in v1, and the server’s re-execution is the deferred third.
Server-side replay — a server re-running a client’s work to catch a forged result — rests on exactly this reproducibility. The determinism that makes server re-execution meaningful is real and verified; in v1 the native/server leg is verified client-side, and re-execution on the server lands with the server port of the grader.
Formal properties
Byte-identity is the runtime half of verification; the frozen grammar and its semantics are the other half. The grammar is frozen against six criteria, each with a machine verification — designing the bad states out, then checking by machine, rather than being careful:
| Property | Meaning | Guaranteed by | Verified by |
|---|---|---|---|
| Complete | every intended program parses; every construct has a surface form | the grammar is corpus-driven: each catalogued construct contributed a form | the full example corpus parses to valid ASTs |
| Correct | exactly the intended language; trees mirror structure (a-b-c = (a-b)-c) |
one normative grammar; total precedence & associativity | conformance suite: positives with expected tree, negatives with expected diagnostic; round-trip parse → canonical format → re-parse yields the identical AST |
| Consistent | no contradictory or dead rules | a single grammar artifact; every non-terminal reachable | the grammar generator’s linter reports zero warnings |
| Unambiguous | every valid input has exactly one tree | an LR grammar class whose build fails on any conflict; each potential conflict resolved by a named device | the build completes with zero unresolved conflicts; fuzzing finds no input with two trees |
| Decidable parsing | the parser always terminates; linear and incremental | LR(1) by stratification; no unbounded lookahead anywhere | complexity profile; the incremental parser serves live preview within its frame budget |
| Semantically coherent | every parsed program gets a defined meaning or a precise error — no gaps | decidable analyses on the tree: kind inference on a finite-height lattice, clock-calculus causality, the plane firewall, totality by construction | the typed corpus asserts expected kinds; negatives assert the exact diagnostic ([ErrDim], repaint attempts, …) |
Three of these verifications deserve a sentence each:
- The build is the ambiguity proof. The normative grammar is expressed once, as a Lezer LR grammar; an LR generator reports every conflict at build time, so “the build is green” is a machine check of non-ambiguity — not a review claim. (An ordered-choice formalism was rejected for exactly this reason: it does not detect ambiguity, it silently hides it.) The same artifact drives the compiler, the editor’s syntax services and the documentation tooling, so there is nothing to drift.
- The corpus round-trips. Every example in the corpus is parsed, printed by the canonical formatter, and re-parsed; the two trees must be identical. A grammar bug and a formatter bug break the same gate. (The corpus is also the golden suite, so an example cannot rot without a test going red.)
- The parser is total. Fuzzing asserts that any byte sequence either parses to a unique tree or is rejected with clean diagnostics — never a crash, never a hang. Malformed input is part of the language’s domain.
Semantic coherence extends beyond parsing: for every kind, the admissibility of each operator, comparison, fill and plot is enumerated over the finite-by-family kind set, so no kind/construct pair is left without either a meaning or a named error. Totality is part of the same discipline — accept or reject is a pure function of the source, decided by counters on the graph rather than by a clock, so the same script compiles the same way on every machine. The grammar and its planes are specified in grammar; the guarantees they underwrite are stated for the reader in guarantees.
Additivity is a build gate
The grammar evolves under strict additivity: a valid script stays valid indefinitely, the semantics of an existing construct is never altered, and the surface only grows. Every extension must itself prove zero conflicts at the grammar build before it lands — additivity is a build gate, not a promise. Keywords destined for future surface are reserved ahead of need, so no program written today can shadow tomorrow’s syntax. This is the syntactic half of a total, deterministic language’s promise about the future of a program; the pinned-routine and byte-identity invariants are the semantic half.
See also
- Compiler and runtime — the two engines, the gate mechanics, the pinned routines and the pinned toolchain this harness verifies.
- Memory model — the layout the plan produces, and why the plan itself is pinned.
- Optimizer — the correctness law, the tiers, and translation validation against the unoptimized graph.
- Concurrency — the scheduler, and the 1 ≡ N proof the stress suite exercises.
- Packages — content addressing, the lockfile, and what the rebuild gate seals.
- Guarantees — the same properties, stated for the reader who must trust them.