The correctness isn't just measured. It's machine-proven.
Every verdict and LOI on this site commits to one property: the merged result is byte-identical regardless of arrival order or parallelism. That property is the definition of an abelian group — and ATOMiK's delta-state algebra is formally verified as one in Lean 4: 108 theorems, zero sorry, depending only on Lean's standard axioms. The guarantee is mathematical, not just observed on one chip.
What “machine-proven” actually means here
The Lean 4 kernel type-checks every proof. We don't ask you to trust that — you can ask Lean what each theorem rests on. Every result depends only on Lean's two standard axioms (propext, Quot.sound) — no custom axioms, and critically no sorryAx, which would appear if any proof were stubbed. Reproduce it yourself:
$ lake build Build completed successfully (10 jobs). $ #print axioms delta_self_inverse 'ATOMiK.delta_self_inverse' depends on axioms: [propext, Quot.sound] $ #print axioms delta_comm 'ATOMiK.delta_comm' depends on axioms: [propext, Quot.sound]
The theorems
The headline results, by the group axiom they establish. Names are the actual Lean identifiers in math/proofs/ATOMiK/.
delta_assocAssociativity — grouping of merges does not change the result.
theorem delta_assoc (a b c : Delta) : compose (compose a b) c = compose a (compose b c)
delta_commCommutativity — arrival order does not change the result. This is the order-independence your contract rests on.
theorem delta_comm (a b : Delta) : compose a b = compose b a
delta_identity_uniqueIdentity is unique — there is exactly one no-op delta (zero).
theorem delta_identity_unique (e : Delta) (h : ∀ d, compose d e = d) : e = Delta.zero
delta_self_inverseSelf-inverse — applying a delta twice cancels it. The architectural basis of the security model.
theorem delta_self_inverse (d : Delta) : compose d d = Delta.zero
atomik_deterministicDeterminism — the same deltas always reconstruct the same state (no hidden nondeterminism).
theorem atomik_deterministic … (Transition.lean)
computational_equivalenceEquivalence — the delta model computes exactly what the traditional stateful model does (encode/transition/decode round-trips).
theorem computational_equivalence : (∀ s₁ s₂, transition s₁ (encode s₁ s₂) = s₂) ∧ …
All 108 theorems, by module
Scope — what is proven vs. what is measured
The Lean proofs verify the delta-state algebra — the mathematical model. They do not, on their own, verify the FPGA gateware. The bridge is empirical and independent: the hardware engine produces a byte-identical result across 1/2/4/8 banks, measured on silicon. So the order-independence is proven in the math and observed in the hardware — two independent lines of evidence for the same property, which is exactly what a correctness-critical commitment should rest on.
See the measured side on the benchmark tool (the recorded reference run and the byte-identical result hash). The full Lean source (math/proofs/ATOMiK/) is available for review under evaluation.