IronProof: proofs about the machine code, not the source

Every claim about a cryptographic implementation is, in the end, a claim about machine code. You write the source, the compiler emits something else, and the thing that runs is the second one. A review of the first is evidence about the second only to the extent that you trust every transformation in between.

IronProof removes that gap for the kernels where it matters most. It proves properties of the code that actually runs: the assembly rustc emits for IronCrypto's hand-written kernels, and the PTX that the IronWorks inference engine sends to NVIDIA GPUs. It works by symbolic execution and SMT solving — Bitwuzla, with z3 and cvc5 as cross-checks — and every obligation comes back as one of four answers: proved, refuted with a concrete counterexample, unknown, or unsupported. Results are cached per kernel and reported as machine-readable data, so an agent can act on them instead of reading a PDF.

It started on 18 October and is 268 commits old.

What it actually checks

On x86-64, against IronCrypto's kernels: functional equivalence with a specification, constant time (no secret-dependent branches and no secret-dependent addresses), register and stack hygiene (no secrets left behind on return), and memory bounds.

On the GPU, against IronWorks' PTX: memory bounds, functional behaviour down to the exact bytes written, and freedom from data races between threads.

Why you should believe the prover

A prover is only as good as its model of the hardware, and the honest failure mode is a prover that confidently proves something about an instruction it has subtly wrong. IronProof is built so that this fails loudly instead.

Every instruction rule is tested against real hardware. On x86-64 that is 1,595 rules by mnemonic and operand form, of which 1,594 are compared directly against the CPU; the one exception is ret, which is structural because the harness cannot run a bare ret. On the GPU, 286 PTX rule forms are compared against an RTX 3090 Ti. A proof that would need an untested rule does not come back proved — it comes back unsupported.

Mutation testing checks the other direction. Deliberately broken kernels — a shift off by one, a guard flipped, a buffer one byte short — must come back refuted, and they do. And the bugs the tests found in IronProof itself are written down in the open, in docs/RESULTS.md, rather than quietly fixed.

x86-64: what is proved

The proved kernels include P-256 and P-384 Montgomery arithmetic and point operations; Curve25519 field arithmetic; the AES-NI, VAES and PCLMULQDQ AES-GCM bulk kernels; AVX2 and AVX-512 ChaCha20, Keccak and Poly1305; and the RSA kernels, including AVX-512 IFMA exponentiation.

One full run covered 342 obligations over 112 targets: 335 proved, 7 unknown, none refuted. The seven unknowns are all constant-time results on vector kernels, and they are unknown for a stateable reason rather than a mysterious one — for the whole fe64 multiply and square, it is that andps has no documented timing class in the instruction ontology. An undocumented timing class is exactly the kind of thing that should produce unknown and not a shrug.

The GPU work

The newest results, from the first half of November, are about quantized-weight dequantize kernels: the hot path of LLM inference, where a compressed tensor becomes floats on its way into a matrix multiply. These are IronWorks' GGUF decoders — Q4_0, Q4_1, Q5_0, Q8_0, Q4_K, Q5_K, Q6_K and IQ4_XS.

All of the eight-element-wide variants are now proved for memory safety, exact output values and race freedom, for any tensor size. That last clause is the interesting part: not "for the sizes we tested", but for every size the kernel can be called with. Q4_1 took about six minutes to prove, Q5_0 about ten, Q5_K about forty-five, with Q6_K finished just before them.

IQ4_XS came with an extra: it was proved through a shared-memory barrier, which is a capability result as much as a kernel result. The model carries state across a synchronisation point rather than giving up when it reaches one.

Real bugs, found by proof

The result that justifies the whole exercise is an out-of-bounds GPU write that the solver found in IronWorks' eight-wide decode kernels, for tensor sizes between 2,147,483,641 and 2,147,483,647 — the last seven sizes below the signed 32-bit limit.

The mechanism is worth following, because it is entirely ordinary. The thread at index 2,147,483,640 passes the usual bounds check, idx < n. The kernel then guards its sixteen-byte vector store with idx + 8 <= n, which looks like precisely the right check. But that addition is done in 32-bit arithmetic, where it overflows to INT_MIN — so the guard passes too, and the store writes one element past the end of the buffer.

No test caught it, and no test was ever going to: catching it requires allocating a tensor of about two billion elements and then hitting the last eight of them. The search space is not where tests look.

IronWorks changed the guard to n - idx >= 8 in all eight kernels, and the fixed versions were re-proved with no upper limit on n at all. The same old guard was then shown to fail in the K-quant kernels as well. Separately, the GPU kernels were checked bit for bit against reference decodes on an RTX 3090 Ti, with nothing written past n.

Then the solver found a second one, in the Q8_0 decoders. The byte offset in the three Q8_0 dequantize kernels was also an int, and block_idx * 34 passes INT_MAX once n exceeds 2,021,161,080 — a Q8_0 block is 34 bytes for 32 elements, so the byte offset crosses the signed 32-bit limit well before the element count does. Past that point the offset wraps negative and the loads read before the buffer. Computing the offset in 64 bits fixed it, and all three kernels are now proved for memory safety, exact outputs and race freedom with no limit on n at all, in 29 seconds, 21 seconds and 4.6 minutes. The eight-wide kernel also matches the reference decode bit for bit on the RTX 3090 Ti; the two scalar kernels' evidence is the proof alone, with no GPU run behind it.

One relative had the same defect, and now it does not. dequantize_q8_kv_kernel decodes 258-byte blocks of 256 elements, one block per thread block, and computed bid * 258 in an int — which passes INT_MAX from block 8,323,580, after which the loads read before the buffer. Both the source offset and the destination index are now computed in 64 bits. IronProof refutes the old kernel on both of its obligations and proves the new one for any block count, in seconds. The claim is deliberately narrower than the one above: this kernel's target carries no functional specification, so memory safety and race freedom are proved and the output values are not, and it was never run on a GPU. It is reached only by a diagnostic comparison test, never by an inference path.

And the scalar Q4_0 kernel, refuted outright. At 192 threads a block its signed 32-bit index wraps, and all three obligations fail — in nine seconds. The index and offsets are unsigned now, with the guard testing idx >= (unsigned)n_elements, and memory safety, output values and race freedom are proved at 192 threads a block and at 256. At 256 the original would never have wrapped, which is rather the point: the defect was reachable only at a launch geometry nobody had used yet. The fixed text has not been run on a GPU; its evidence is the proof.

The limits, stated plainly

A proof is a statement about a model, and the model's edges are where the real risk lives. Four of them matter here.

The GPU proofs are at the PTX level. ptxas, the SASS it produces and the driver underneath are not covered. PTX is an intermediate representation, not the instruction stream the hardware executes.

Float instructions are modelled as arbitrary functions. The proof establishes that the right inputs reach the right float operations in the right order. It says nothing whatsoever about floating-point accuracy — that remains evidence from GPU testing only.

A proof binds to the exact text that was proved. nvcc and NVRTC emit different PTX for the same kernel, so each is proved separately. Change the compiler and the proof does not come along.

These results are evidence for security controls, not certification. Neither IronProof nor IronCrypto is FIPS 140-3 validated or CMVP certified, and nothing here should be read as implying otherwise.

Why bother

The usual argument for formal methods is that bugs are expensive. The better argument, visible in all four defects above, is that some bugs are unreachable by testing in principle. You cannot sample your way to the behaviour of a kernel at two billion elements, you cannot fuzz your way to a guard that is correct for every input except the eight at the very top of the index range, and you will not stumble on a wrap that needs a launch geometry your code does not yet use. A solver does not sample. It asks whether a counterexample exists, and when one does, it hands you the exact input.

That is also why the output is data rather than prose. "Proved, refuted, unknown, unsupported" per obligation, cached per kernel, is something a build can gate on and an agent can read. A claim that the AES-GCM kernel is constant-time is worth little; a machine-checkable record of which obligations were proved, against which specification, under which instruction rules, each tested against the CPU, is worth something.

IronProof is phase 1, the x86-64 and PTX guarantees above are what is established, and docs/RESULTS.md carries the figures, the counterexamples and the prover's own bugs behind every claim in this post.

Per aspera ad astra.