ArchSem: Reusable Rigorous Semantics of Relaxed Architectures
THIBAUT PÉRAMI, THOMAS BAUEREISS, BRIAN CAMPBELL, ZONGYUAN LIU, NILS LAUERMANN, ALASDAIR ARMSTRONG, PETER SEWELL
2026
The specifications of mainstream processor architectures, such as Arm, x86, and RISC-V, underlie modern
computing, as the targets of compilers, operating systems, and hypervisors. However, despite extensive
research and tooling for instruction-set architecture (ISA) and relaxed-memory semantics, recently including
systems features, there still do not exist integrated mathematical models that suffice for foundational formal
verification, of concurrent architecture properties or of systems software. Previous proof-assistant work has
had to substantially simplify the ISA semantics, the concurrency model, or both.
We present ArchSem, an architecture-generic framework for architecture semantics, modularly combining
ISA and concurrency models along a tractable interface of instruction-semantics effects, that covers a range of
systems aspects. To do so, one has to handle many issues that were previously unclear, about the architectures
themselves, the interface, the proper definition of reusable models, and the Rocq and Isabelle idioms required
to make it usable. We instantiate it to the Arm-A and RISC-V instruction-set architectures and multiple
concurrency models.
We demonstrate usability for proof, despite the scale, by establishing that the Arm architecture (in a
particular configuration) provides a provable virtual memory abstraction, with a combination of Rocq, Isabelle,
and paper proof. Previous work provides further confirmation of usability: the AxSL program logic for Arm
relaxed concurrency was proved sound above an earlier version of ArchSem.
This establishes a basis for future proofs of architecture properties and systems software, above production
architecture specifications.