What is claimed, how each claim is discharged, and what is still open.
Nothing is marked ✅ here until mucore/tests/verify.sh proves it. Run it:
cd mucore && make verifyRequires cbmc (brew install cbmc) and clang.
| Clause | Claim | Method | Status |
|---|---|---|---|
| S1 | No undefined behaviour, for any input | CBMC | 🟡 6 of 8 functions |
| S2 | The arena never overruns and blocks never overlap | CBMC | ✅ proven |
| S3a | Only exactly-rounded FP operations are used | LLVM IR check | ✅ proven |
| S3b | Output depends only on the inputs | CompCert | ✅ proven |
| S4a | mu_expf is within 1 ulp of the true result |
exhaustive | ✅ proven |
| S4b | Error bound for the matrix multiply | Rocq proof | ✅ proven |
| S4c | Per-stage bounds compose; error is linear in depth | Rocq proof | ✅ proven |
| S5 | It computes a transformer correctly | Coq | ⬜ deferred |
Claim. For any input accepted by mu_model_init and mu_tok_init, no
execution reads or writes outside an object, overflows a signed integer,
divides by zero, or fails to terminate.
Method. CBMC, bounded model checking. Every loop is fully unwound and
--unwinding-assertions makes an insufficient bound a hard failure, so no
result here is a silent under-approximation.
One substitution is made under CBMC only, and it is load-bearing: mu_sqrtf
normally uses inline assembly (fsqrt on AArch64, sqrtss on x86-64), and CBMC
does not model inline asm — it silently treats the block as having no effect,
which would make any result about a function using sqrt meaningless. Under
__CPROVER__ the function calls sqrtf, which CBMC models as the IEEE-754
square root, exactly what the assembly computes. The shipping build is unchanged
and S3a independently confirms it links no libm.
Proven (mucore/tests/cbmc_units.c, 3023–3099 checks each, all discharged):
| Function | Symbolic over | Result |
|---|---|---|
mu_argmax |
length n ∈ [1,8], all values |
index always in [0,n) |
mu_matmul |
n,d ∈ [1,6] |
no access outside w[n·d), x[n), out[d) |
mu_softmax |
length n ∈ [1,8] |
no out-of-bounds access |
mu_rmsnorm |
length n ∈ [1,8] |
no out-of-bounds access |
mu_tok_decode |
blob bytes, offsets, lengths, out_cap |
never writes more than out_cap |
mu_tok_init |
every byte of a 20-byte blob, blob length | rejects malformed input rather than reading out of bounds; on success every record lies inside the blob |
mu_tok_init is the one that matters most for security: it parses untrusted
length-prefixed records out of a tokenizer file. With the blob fully symbolic,
CBMC proves the off + len > blob_bytes rejection cannot be bypassed for any
byte pattern of that length.
Not yet covered, and why. mu_forward end to end, and mu_tok_encode.
mu_tok_encode was attempted four times with progressively less symbolic state
and does not terminate: 28-byte symbolic blob with 4 bytes of text, then 14/2,
then a concrete blob with 3 symbolic text bytes, then 1 byte with mu_tok_init
bypassed entirely. None produced a verdict inside 13 minutes.
The obstacle is structural rather than a matter of size. The BPE merge loop
rescans every adjacent pair each pass, and each tok_lookup is a binary search
whose branches depend on symbolic bytes, so the path count explodes no matter how
short the input is. Bounded model checking is the wrong tool here; this function
needs Frama-C with a loop invariant on the merge loop. The harness was deleted
rather than left in the tree unrun.
Why mu_forward whole is not done. CBMC encodes IEEE-754 bit-precisely.
One forward pass is thousands of float operations, and the harness did not
finish in ten minutes even on an 8-dimension model. That cost buys nothing for
memory safety, because no index in the engine depends on a float value —
float values reach control flow only through the two > comparisons in
mu_softmax and mu_argmax, and both branches of each are index-safe. Unit
harnesses with symbolic sizes are cheaper and prove more, since each result
holds for a range of shapes rather than one config.
Bound sizes are also a real limit: these results hold for the stated ranges, not
for dim = 4096. Completing S1 needs Frama-C with loop invariants over a
symbolic dim, which would cover all configs. Frama-C is not packaged for
Homebrew and needs an opam toolchain.
One practical note recorded because it cost time: symbolic state is the binding
constraint, not loop count. A 48-byte symbolic tokenizer blob did not finish in
eight minutes; the same harness at 20 bytes finishes in 0.7 s. Per-loop bounds
(--unwindset) matter too — mu_tok_init needs 257 unwindings for its
byte_pieces table, and applying that globally makes the parser intractable.
Claim. mu_arena_alloc returns either NULL or a 64-byte-aligned block lying
wholly inside the arena and not overlapping any earlier block. used never
exceeds size and never decreases.
Method. CBMC over a symbolic arena size and three symbolic allocation sizes. Pure integer arithmetic, so the result is exact. Three allocations is the minimum that can expose an overlap bug: it needs a previous block, a current one, and a following one.
All 3099 checks discharged, including alignment, containment, non-overlap and monotonicity.
Claim. Every floating-point operation the compiler emits for mu_core.c is
one that IEEE-754 clause 5.4.1 requires to be correctly rounded: + − × ÷ √,
plus format conversions and comparisons. No fast-math flags. No FMA. No libm.
Method. Static analysis of the LLVM IR after optimisation, at -O0,
-O1, -O2, -O3 and -Os. Checking the C source would be weaker: the source
says val += w[j]*x[j], but what runs is whatever the optimiser produced, and
the optimiser may fuse, reassociate or vectorise.
What this caught. The core is auto-vectorised — 61
llvm.vector.reduce.fadd calls at -O2 and -O3. That is safe only because
they are the ordered form; LLVM's vector.reduce.fadd is strictly
sequential unless it carries reassoc, at which point the summation order
becomes unspecified and reproducibility is gone. Zero of them carry it, and zero
FP instructions in the module carry any fast-math flag. The check fails if that
ever changes.
Negative control. Building -Ofast -march=native produces 331 fast-math
flagged instructions and is correctly rejected.
Claim. Given S3a, and a compiler whose output provably preserves source-level IEEE-754 semantics, the logits are a function of the inputs alone — identical on every platform conforming to IEEE-754 with round-to-nearest-even.
Method. Build with CompCert 3.17, the formally verified C compiler. CompCert has a machine-checked proof that the assembly it generates behaves as the source semantics prescribe, and it models floating point with Flocq rather than treating it as opaque.
Result. CompCert produces the reference hash at both -O2 and -O0:
clang 21 9b78b92a305dc59611b5c53a04b538ae9c4ae18aea6c1fdbf6e45e9848b23bd2
CompCert -O2 9b78b92a305dc59611b5c53a04b538ae9c4ae18aea6c1fdbf6e45e9848b23bd2
CompCert -O0 9b78b92a305dc59611b5c53a04b538ae9c4ae18aea6c1fdbf6e45e9848b23bd2
What that buys, precisely. The hash is no longer "what clang happens to emit". By CompCert's theorem, a CompCert build computes the semantics of the C program; by S3a, those semantics use only operations IEEE-754 requires to be correctly rounded. So the reference hash is the unique answer the standard permits, and any conforming implementation must produce it. The eight-build agreement stops being a coincidence worth noting and becomes a consequence.
Note this does not prove clang is correct. It proves the answer is, and that clang agrees — which is the more useful direction: it validates the output, not the toolchain.
The one substitution CompCert forces. It rejects inline assembly, correctly,
since its verified semantics cannot cover it. So under __COMPCERT__, mu_sqrtf
uses (float)__builtin_fsqrt((double)x). Double rounding is harmless for sqrt
when the wider format carries at least 2p+2 bits and binary64's 53 exceeds the
50 binary32 needs — but rather than cite the theorem,
tests/exhaustive_sqrtf.c compares it against the hardware instruction over
all 2,139,095,042 non-negative inputs. Zero differences.
What is still assumed. CompCert's theorem covers the compiler, not the assembler, the linker, or the hardware. Its own proof is relative to a model of the target ISA. And the result above is one checkpoint and one prompt; the theorem is general but the check is not exhaustive over inputs.
Building it. vendor/compcert/fetch.sh. Not vendored: it is a source
distribution whose build is a Coq proof check taking tens of minutes. Rocq 9.2
is explicitly supported as of CompCert 3.17. This is why S3b is skipped rather
than failed in CI.
Claim. For every binary32 x in [-103.97, 88.72] whose true exp(x) is a
normal binary32 number, mu_expf(x) is within 1 ulp of the correctly-rounded
result. mu_expf(0) = 1 exactly.
Method. Exhaustive enumeration of all 2³² binary32 bit patterns, compared
against (float)exp((double)x). This is a complete case analysis over the whole
domain — nothing sampled, nothing extrapolated. For a single-argument float32
function it is stronger than an interval bound: it establishes the exact worst
case and where it occurs.
Result (mucore/tests/exhaustive_expf.c, 3.4 s on 8 threads):
inputs in the normal domain 2,237,668,968
bit-exact vs reference 2,236,503,555 (99.9479%)
within 1 ulp 2,237,668,968 (100.0000%)
worst case 1 ulp, at x = 0.0808606073 (0x3da59a3f)
clamp contract violations 0
Documented deviations from exp, both deliberate and both checked:
x < −103.97 returns +0 where exp gives a subnormal, and x > 88.72 returns
FLT_MAX where exp gives +inf. NaN and infinite inputs are out of contract —
the engine never produces them as arguments, because softmax subtracts the row
maximum first and SwiGLU negates a finite activation.
Why not Gappa. Gappa would prove the bound from the polynomial's structure rather than by enumeration, which also extends to binary64. It is not packaged for Homebrew. Worth adding, but it would not strengthen the binary32 claim.
Claim. For the loop for (j=0;j<n;j++) val += w[j]*x[j] under the standard
floating-point model fl(x op y) = (x op y)(1+d), |d| <= u:
|computed - exact| <= gamma_n * sum |a_i b_i|, gamma_n = (1+u)^(n+1) - 1
Method. A machine-checked proof in Rocq 9.2, proofs/DotError.v. Not an
instantiation of LAProof — written directly, because the statement is short
enough that a self-contained proof is easier to audit than a dependency.
Three results, all with no Admitted and no added axioms:
| Theorem | Statement |
|---|---|
dot_error |
the bound, for a right-associated fold |
dot_error_loop |
the bound with a running accumulator, including the accumulator's own error term |
dot_error_loop_from_zero |
corollary at acc = 0, which is the C loop verbatim |
dot_error_loop_from_zero
: forall u : R, 0 <= u ->
forall (l : list (R * R)) (r : R),
computes_from u 0 l r ->
Rabs (r - dot l) <= gamma u (length l) * adot lPrint Assumptions reports exactly two axioms, sig_forall_dec and
functional_extensionality_dep, which are what Rocq's classical reals are built
on. Every proof about R depends on them; nothing was assumed here.
Why two fold directions. The first theorem associates right; the C loop
accumulates left. The bound is the same, but proving one and claiming it covers
the other would be sleight of hand, so computes_from models the loop verbatim
and dot_error_loop_from_zero is the result that actually applies.
Two things the proof forced into the open. The accumulator bound must be
(|acc| + |P|(1+u))(1+u), not (|acc| + |P|)(1+u) — the product is already
rounded before the add, so it carries its own factor, and with the looser form
the induction does not close. And u < 1, which the standard treatment assumes,
turns out to be unnecessary: the bound holds for any u >= 0. The hypothesis
was removed rather than left in place looking load-bearing.
What this does not cover. Underflow. The multiplicative model is exactly what fails for subnormal results, so the bound is conditional on no underflow occurring. This is a property of the model, not of the proof, and it is the one assumption that could bite in practice.
The problem. S4a bounds mu_expf. S4b bounds the dot-product loop. Neither
says anything about a forward pass, because a forward pass is a chain and every
stage feeds the next one an input that is already wrong.
Method. Two Rocq files, proofs/Compose.v and proofs/Depth.v.
Compose.v proves the general machinery. A stage carries its exact function, its
implementation, a Lipschitz constant and its own error bound. Then:
| Theorem | Statement |
|---|---|
chain2 |
two stages: total error ≤ ef + Lf · eg |
chain_n |
a pipeline: total ≤ Σᵢ eᵢ · ∏_{j>i} Lⱼ — each stage's error amplified by everything downstream |
total_err_additive |
if every stage is non-expansive (L ≤ 1), total ≤ Σ eᵢ |
Depth.v instantiates it for the shape a transformer has — the same layer
repeated:
uniform_depth_linear
: forall (s : stage) (n : nat),
wf_stage s -> s_lip s <= 1 ->
forall x, Rabs (run_impl (repeat s n) x - run_exact (repeat s n) x)
<= INR n * s_err sWhat that says. n identical non-expansive layers, each within e of exact,
give a stack within n·e. Error grows linearly in depth, not
exponentially. depth_6 states the stories15M case: within 6·e.
That is the whole reason a multi-layer forward pass is bounded at all. If errors
compounded multiplicatively the bound would be e·Lⁿ and worthless.
lip_tail_repeat proves the accumulated factor really is Lⁿ in general, so
non-expansiveness is doing genuine work here rather than being a convenience.
Both files are axiom-clean — the same two classical-reals axioms and nothing else.
What is still missing for a numeric constant on mu_forward. Two inputs:
a per-layer e, obtained by composing S4a and S4b across the operations in one
layer, and a per-layer Lipschitz constant, which depends on the weight norms of
a specific checkpoint. The theorem is parametric in both, which is the honest
form: supply them and you get a number. Claiming a figure without them would be
made up.
Claim. There is a reference transformer T over ℝ in Coq such that
‖mu_forward(token, pos) − T(weights, tokens)‖∞ ≤ δ for δ from S4c.
Deferred on purpose. This needs a reference transformer written in Coq, which is a project in its own right. S1–S4 are a stronger claim than any inference engine currently has, and S5 without them would not be worth much.
A proof is universally quantified over inputs and checked once, offline. It says nothing about one specific run. To show what happened on a particular request you need attestation or re-execution. Proofs make the engine worth trusting as the thing that re-executes; they are not a receipt.