ArchSem documentation

ArchSem is a Rocq framework to define the semantics of CPU architectures such as Arm-A, RISC-V, and x86, integrating their concurrency models — written in Rocq — and instruction-set semantics — written in Sail.

GitHub repository · POPL 2026 paper

Rocq theories

Generated with coqdoc. The contents link is the table of contents of the theory; index is the alphabetical index of its identifiers.

• ASCommon
  Common infrastructure and definitions for the ArchSem project, including CDestruct and a free monad library.
  contents index
• ArchSem
  The architecture-generic part: the ISA/concurrency interface, candidate executions, and the generic model constructions.
  contents index
• ArchSemArm
  The Arm-A instantiation and its concurrency models.
  contents index
• ArchSemRiscV
  The RISC-V instantiation and its concurrency models.
  contents index
• ArchSemX86
  The x86 instantiation and its concurrency models.
  contents index

OCaml API

Generated with odoc. Only the archsem package ships OCaml code: the extracted models and the litmus-test runner behind the archsem command-line tool. The coq-archsem* package pages exist but are empty.

• archsem
  The extracted models (Archsem) plus the archsem.litmus and archsem.isla libraries.
  contents