Imagine you're writing a program. You assume the CPU runs your instructions in the order you wrote them. That assumption is a comforting lie. Modern processors aggressively reorder instructions to keep their execution units busy — a load might complete before an earlier store, and multiple cores interleave their memory operations in ways that defy any single "timeline" of events. This is called weak memory, and it's why concurrent programming is famously terrifying.

The saving grace is that CPU vendors publish an ISA memory model — a formal contract describing which weird reorderings are allowed and which aren't. Programmers (and compilers) rely on this contract. But here's the uncomfortable question: does the actual silicon really obey the contract? The hardware is a labyrinth of reorder buffers, store queues, cache coherence protocols, and speculation. Between the tidy ISA specification and the messy microarchitecture lies a huge trust gap.

This paper closes that gap with a machine-checked mathematical proof. The authors formally verify that an out-of-order, multi-core processor design correctly implements a weak-memory ISA. Two things make this hard:

• Intra-core reordering: a single core fires instructions out of program order and later "commits" them, hopefully producing results indistinguishable from in-order execution.
• Inter-core interleaving: multiple cores share memory, and there's no global clock deciding whose write lands first.

Combine these and you get behaviors no sequential trace can explain. Previous verification work usually tackled one dimension in isolation, or verified simpler in-order or single-core designs. Doing both together, against a realistic weak-memory ISA, has been a long-standing open problem.

The key insight is a proof structure that separates the two concerns cleanly: they show each core's out-of-order pipeline is equivalent to an in-order abstraction, and then show the resulting system of in-order cores produces exactly the behaviors the ISA memory model allows. By finding the right "middle" abstraction, they avoid drowning in the combinatorial explosion of tracking every reorder-buffer entry across every core simultaneously.

Practically, this means a piece of hardware you could actually build now has a mathematical guarantee — not just testing, not just simulation — that concurrent programs relying on the ISA's memory model will behave as promised. Bugs in weak-memory hardware are notoriously silent: a race might manifest once every billion cycles under a specific cache state, and no test suite will reliably catch it. Proofs will.