#Guarantees

Flux makes seven guarantees. This page is the one place that states each in a sentence, draws the exact line between what it covers and what it does not, and names the machine check that enforces it — because a guarantee whose only enforcement is a promise in a document is not a guarantee. The harness and the reproducible-build gate that run those checks are specified in full in Verification & reproducible builds; what follows is the reader’s-eye summary of what each guarantee means for you.

Nothing here is aspirational. Where a limit is real, it is stated as a limit.

New here? Start with Guide §11 — Determinism, replay and trust →

#The seven guarantees

Figure — the seven guarantees, each wired to the single blocking machine check that enforces it.

#What each one actually means

#Totality

Every window, every loop, every collection carries a constant bound, under a cap. A program that cannot state its bound does not compile.

What it covers. Termination, and a cost per step that is computable at compile time. There is no per-bar timeout, because there is nothing to time out: an over-budget program is rejected, not killed.

And the verdict itself is deterministic. Accept or reject is a pure function of the source, decided by counters alone — never by a clock. The editor’s build timeout (on the order of two seconds) is an interactive cancellation, a matter of keeping the UI responsive; it is never a verdict.

Why this rule exists. A wall-clock verdict would be machine-dependent — the same script accepted on a fast machine and rejected on a slow one. Two users would then not be running the same language, and replay, which assumes that what compiled there compiles here, would break; anti-cheat would break with it. Determinism has to start at the compiler’s answer, or it does not hold anywhere downstream.

What it does not cover. It does not make your algorithm fast. It makes its cost knowable.

#Causality — “no-repaint”

Delays reach backwards only. A resample reads the last closed unit of a coarser clock, never the one still forming. Every feedback cycle must cross a unit delay.

What it covers. The value a bar showed yesterday is the value it shows today. Live and historical evaluation produce the same bytes. Repaint is not discouraged — it is inexpressible: there is no syntax for a negative index, and no name for the forming unit inside analysis.

The one exception, and its wall. live(e) reads the forming bar, and it may flow only to display sinks. Feeding it into an alert, an assertion or a calculation is [ErrFirewall]. A script that uses it is flagged non-replayable, visibly, in the guarantees panel.

#Byte-determinism

Scalar f64. No SIMD in the deterministic domain. No floating-point reassociation. Every transcendental, every decimal operation, every Unicode fold, every calendar addition, every random draw, and every sort over absent values goes through one pinned routine, shared by the interpreter, the compiled module and the server.

What it covers. Two engines agree bit for bit. A golden holds. Replay reconstructs a model exactly.

Server re-execution — a server re-running a client’s work to catch a forged result — rests on exactly this determinism, and is designed. In v1 the native/server leg is verified client-side: re-execution on the server lands with the server port of the grader.

What it does not cover. Presentation. The GPU, the compositor, unseeded randomness and wall-clock time are outside the oracle by design — and the firewall guarantees they never enter it.

#Dimensional soundness

A price is not a volume; a BTC price is not an ETH price; an exact decimal is not a float. Adding them is a compile error, not a runtime surprise and not a silently wrong number.

What it covers. A whole class of bugs that other systems find in production, if at all.

What it does not cover. It is not a proof system. An osc(0,100) bound is a presentation claim, not a runtime invariant — only clamp makes a bound real. Flux deliberately has no solver, and says so.

#The firewall

Four things may never reach analysis: screen space, the wall clock, unseeded randomness, and the forming bar. All four raise [ErrFirewall].

What it covers. A stranger’s animated, random, interactive scene can run next to the number your decision rests on, and cannot touch it. This is what makes user-generated content a routine act rather than a risk assessment.

#Capability security

A script holds no capability object. It emits a request; the host, the only holder of the resource, executes it — and only if the manifest declared it and the user granted it.

What it covers. No ambient authority. No token in the script. No re-delegation. A transitive manifest that surfaces a dependency’s appetite for the network before install, capped by the user’s grant. A revocation mid-session is journaled, so a re-fold reproduces it and commands issued after it fail closed.

The honest limit. The language is safe by construction; the capability monitor and the view sanitizer are ordinary code, and they are the residual attack surface. That is precisely why they are the one component that earns a model check, and why the view primitives are a closed, typed set rather than a string.

#Verified optimization

The reference semantics of a program is the evaluation of its unoptimized graph. Every compilation checks the optimized module against it, bit for bit, on hostile data.

What it covers. A miscompilation cannot ship. If the optimizer diverges, the compile serves the unoptimized path and raises a diagnostic that turns the test suite red.

The honest limit. The gate proves equality over the corpus’s value coverage and up to a sweep ceiling of periods. A rule whose divergence only appears beyond that ceiling would pass — which is why rules touching kernels or state carry an explicit proof obligation at the real maximum period.

#How the guarantees are checked

Each guarantee above is backed by a blocking sub-suite, and each sub-suite declares its own oracle and corpus: goldens that must stay byte-identical, a well-typed fuzzer that proves the parser and type checker total, a three-way differential oracle (interpreter ↔ WASM ↔ native kernel), the enumerated metamorphic relations, the 1 ≡ N concurrency stress, lattice enumeration per family, and the capability monitor. Only the cost-model bench is advisory. Alongside the harness, a rebuild gate recompiles the same inputs twice — different machines, different thread counts — and asserts a byte-identical module, because server-side replay would break silently under a non-reproducible build.

One subtlety a careful reader will ask about: the three-way oracle calls the same pinned routine on all three sides, so a bug inside a pinned routine is invisible to it — which is why each pinned routine also carries a second, independent reference implementation, compared bit for bit on fuzzed input.

Canonical, in full — the suite table, its blocking column, the second-implementation rule and the rebuild gate live at Verification & reproducible builds.

#The guarantees panel

After a compile, the editor states what your program actually earned:

✓ No-repaint     ✓ No look-ahead     ✓ Deterministic
✓ Bounded memory ✓ Byte-identical    ⚠ contains live() → non-replayable

It is not decoration. A guarantee you traded away should be visible at the moment you traded it.

#What is not guaranteed

Stated plainly, because a trust page that only lists strengths is a sales page:

• Presentation is not deterministic, and does not try to be. The GPU, the compositor and unseeded randomness are outside the oracle — contained by the firewall, never eliminated.
• Replay proves coherence, not truthfulness. A host-pushed payload journaled as data — a pick result, a pre-computed outcome — is re-folded verbatim; replay does not re-run the ray-cast to attest it. A score that depends on such an outcome needs the server to re-derive it, or must be excluded from a shared leaderboard (server — the grader). This is a named open problem, not a hidden one.
• Server re-execution is designed; the determinism that lets a server re-run a client’s work and catch a forged result is real and verified, but in v1 it is verified on the client. The server leg lands with the server port of the grader (server — the third leg).
• Bounds are claims, not invariants. osc(0,100) says what a value conventionally is, not what it provably is. Only clamp makes it real.
• The sandbox rests on two pieces of ordinary code — the capability monitor and the view sanitizer. Everything else is safe by construction; those two are safe by review, by model checking, and by fuzzing.

#See also

• Verification & reproducible builds — the harness and the rebuild gate, in full.
• The seven design pillars — the same properties, from the design side.
• Compiler & runtime — the gate and the pinned routines.
• The optimizer — the correctness law, and the rewrites that look sound and are not.
• The App plane — capabilities, journals, and replay.
• FAQ — the questions this page provokes.