Sail turns ISA manuals into emulators, proofs and test generators

A language for instruction semantics rather than for programs

Sail describes what a processor actually does when it executes an instruction. The project calls it the ISA specification language, and the definition of the ISA is given as the architectural specification of the behaviour of machine instructions. That is a narrow and serious subject: the output is a description of a silicon interface, not an application.

The project positions the language against vendor pseudocode, which is how processor manuals have traditionally written behaviour down. Sail is described as engineer friendly, much like earlier vendor pseudocode, but more precisely defined and with tooling to support a wide range of use cases. That pairing is the point of the project. The manual prose is readable but not executable, so it cannot be type checked, cannot generate an emulator, and cannot feed a theorem prover.

Who uses it, then. The model list includes Arm-A, Morello for CHERI-Arm, RISC-V, CHERI-RISC-V, CHERIoT, x86, CHERI x86, MIPS, CHERI-MIPS and IBM Power. Sail RISC-V has been adopted by the RISC-V Foundation. The Arm models are automatically translated from the Arm internal ASL reference used in the Arm reference manual, and they are provided under a BSD 3-Clause Clear licence by agreement with Arm.

The audience is therefore architecture and hardware verification teams, security researchers, and the maintainers of instruction set specifications who want a single machine readable source for the manual, the emulator and the proofs.

Dependent typing on bitvector lengths, checked by Z3

The language is essentially a first-order imperative language with lightweight dependent typing for numeric types and bitvector lengths. Those types are checked automatically using the Z3 SMT solver.

This is the single most valuable property of the language for its audience, and it is worth being concrete about what it buys. An ISA specification is full of widths: register fields of 5 bits, immediates of 12 bits, sign extension from one width to another. Writing that in pseudocode is easy to get wrong, because nothing enforces that a 5 bit field is compared against a 32 bit value, or that a concatenation produces the width the designer intended. A type checker driven by an SMT solver can reject unintended mismatches of bitvector lengths, and the project lists that type checking as the first thing the tool does with a specification.

The solver is a real dependency rather than a stylistic choice. Z3 is used at the front end for type checking, and it also appears in the packaging story: the Makefile notes that Z3_EXE can be used to bundle a z3 binary into a release tarball, so the solver ships with the tool rather than being left to the user's package manager.

For a reader deciding whether Sail is overkill, this is the place to look. If your specification is small enough that width mistakes would be caught by review, the solver buys you little. If the model will later be used to generate an emulator and proofs, the type checker is the cheapest possible place to catch the errors that would otherwise surface as mysterious emulator failures.

One specification, many backends

The set of backends is what separates Sail from a documentation tool, and the repository layout shows how many there are.

The package manifest files name them. There is a sail_coq_backend.opam, a sail_doc_backend.opam, a sail_latex_backend.opam, a sail_lean_backend.opam, a sail_lem_backend.opam, a sail_ocaml_backend.opam, a sail_output.opam, a sail_smt_backend.opam and a sail_sv_backend.opam, alongside libsail.opam and sail_maker.opam for the library and the packaging tool itself. The compiler's own library package is libsail.opam, and sail_maker.opam covers the packaging tool, while sail_output.opam and sail_smt_backend.opam cover output and solver support.

What each backend does is documented in the README. Documentation snippets can be generated using either LaTeX or AsciiDoc and included directly in ISA documents, with examples cited from the CHERI ISAv9 specification, the CHERIoT specification and a RISC-V AsciiDoc document. Executable emulators can be generated in C or OCaml, and are meant to be used as an authoritative reference in sequential-code testing and for early software bring-up. Theorem-prover definitions can be generated in Coq, Isabelle or HOL4 to support interactive proof of properties such as security properties, with the Arm Morello ISA proofs given as the worked example.

Two more outputs are worth singling out. Specification coverage can be shown, meaning which parts of the specification the tests running in the generated C emulator actually exercise. And versions of the ISA can be generated in the form needed by relaxed memory model tools, isla-axiomatic and RMEM, to compute the allowed behaviour of concurrent litmus tests with respect to architectural relaxed memory models.

The honest caveat is in the README itself: not all of these are currently supported for all models, and you need to check the current status as needed.

Emulators, coverage and the sequential testing path

The practical workflow that most users start with is the emulator.

A specification is compiled to an emulator in C or OCaml. The generated emulator is then treated as an authoritative reference, which means it is used as the oracle in sequential-code testing rather than as a toy. The same workflow supports early software bring-up, the phase where an operating system or firmware is expected to boot on hardware that does not exist yet in a usable state, and the emulator gives you a specification-accurate target to boot against.

Coverage is the feedback loop that makes this worth doing. The project can show specification coverage, of tests running in that generated C emulator. In practice that means you can tell which instruction behaviours your test suite has actually reached, which is a different question from line coverage of the emulator code and a closer proxy for the part of the ISA that has been checked at all.

Specification coverage is also the bridge to the more advanced features. Automated instruction-sequence test generation from the specification is supported, in ways that get good specification coverage, using the Isla SMT-based symbolic evaluation engine for Sail. The idea is that the specification itself tells you which instruction sequences would exercise interesting behaviour, so test generation is guided by the model rather than by fuzzing blind.

The cost of that route is real. Isla is a separate component with its own repository, and using it means working inside a symbolic evaluation engine rather than a straightforward test runner. For a team that just wants an emulator to boot an OS, that is unnecessary weight. For a team chasing a specific corner of the ISA, it is the only realistic way to get there.

Concurrency, relaxed memory and theorem provers

Three of the backends exist because an instruction set specification is not enough on its own once the machine has more than one core.

The relaxed memory side works by generating a version of the ISA in the form that relaxed memory model tools understand. isla-axiomatic and RMEM are named, and both are used to compute the allowed behaviour of concurrent litmus tests with respect to architectural relaxed memory models, treating the specification as an authoritative reference for the concurrency behaviour. The practical difference from a test that just runs on hardware is that the answer is derived from the model rather than observed, so a litmus test result becomes a property of the specification rather than a fact about one particular machine.

The proof side generates theorem-prover definitions in Coq, Isabelle or HOL4. The point is interactive proof, and the example given is proving that the ISA satisfies intended security properties, with the Arm Morello proofs as the reference work. This is the path taken when the argument you need is not a test result but a theorem: that a capability scheme behaves correctly, or that some instruction sequence cannot escape its permitted behaviour.

There is also a system under construction for interactive proof about sequential binary code, which integrates the Isla symbolic evaluator with the Iris program logic in Islaris. And a SystemVerilog reference model generation is listed as in progress, intended as a reference for hardware verification work such as JasperGold.

In progress is doing a lot of work in that list, and it is where the risk sits for anyone planning work. The SystemVerilog backend has an opam manifest in the repository, but the README marks that capability as in progress rather than finished.

Building from source with dune, and the Docker route

Sail is not distributed as a single pip style package. The build is an OCaml project driven by dune, and the Makefile at the top of the repository is the entry point.

The core targets are short. Building the compiler and installing it are two commands:

dune build --release
dune install

The Makefile wraps these as the sail and install targets, with all defaulting to the sail target. There is also a separate isail target, an executable form of the tool. The repository contains a dune-project file, a .ocamlformat file with a matching .ocamlformat-ignore, and an editors/ directory, which is where language server support for Sail source would live, and the Makefile has an lsp target that descends into src/sail_lsp.

For a reproducible environment, the repository ships Dockerfile.nightly and Dockerfile.release alongside a docker_entry_point.sh and a .dockerignore, and the Makefile exposes a docker target. The project also supports releasing binary tarballs: the tarball target builds a relocatable dune installation, runs sail_maker to assemble it, and optionally bundles a z3 binary through Z3_EXE and, on Windows, a libgmp DLL through GMP_DLL. The release naming on the project's releases page follows that pattern, with the most recent tags being 0.20.3 and 0.20.3-binary.

Two housekeeping targets are worth knowing about because they explain how the standard library stays consistent. The externs target regenerates src/lib/externs.json from the externs declared in lib/, and check-externs runs in CI to fail the build if that recorded file is out of date.

The model library is uneven, and the README says so

The gallery of Sail models is the project's real world footprint, and it is worth reading carefully because the entries differ in ways that affect what you can do with them.

The README states the split directly. Most models are full definitions, able to boot an OS in the Sail generated emulator, but x86, CHERI x86 and IBM Power are core user-mode fragments, and the IBM Power one is in an older legacy version of Sail. The legacy Sail x86 model is likewise a handwritten user-mode fragment in an older version of Sail, while the Sail x86 from ACL2 entry is a version of the X86isa formal model of a substantial part of the x86 ISA in ACL2, automatically translated into Sail.

Within Arm there is a similar layering. The Sail Arm-A models are complete ISA specifications for Armv9.4-A, Armv9.3-A and Armv8.5-A, automatically translated from the Arm-internal ASL reference, and they are the current ones. The older Sail Armv8.3-A model, the public model described in the POPL 2019 paper, is still available but is largely superseded, and a separate handwritten Sail Armv8-A model exists for a user-mode fragment.

The consequence for a new user is straightforward. Choosing an architecture does not tell you which capabilities you get. A full model supports emulator booting and sequential testing; a user-mode fragment supports analysis of user-space behaviour only, and a model in a legacy version of Sail may not build with the current toolchain or the current backends.

A second lesson is about provenance. Several models are automatically translated from another formal specification, ASL for Arm, ACL2 for x86, IBM XML for Power. That gives you a large model quickly and with the authority of the source, but it also means the translation step is part of the trust chain and the model inherits the coverage of its origin.

Versions, the licence file, and what a new model costs

The version numbers show a project on a steady but not fast cadence. Release 0.20.2 was published on 2026-06-22, then 0.20.3 on 2026-09-23, with a separate binary release tag 0.20.3-binary on the same day. The last push to the repository was on 2026-10-19, and the repository is not archived. The default branch is sail2, and the CHANGELOG.md file at the top level records the history.

The licence needs a careful note. The repository carries a custom licence in its LICENSE file, which is why it is not one of the licences GitHub can classify automatically. Read that file before using Sail in a product. The separate BSD 3-Clause Clear grant that applies to the Arm-A models is an agreement with Arm covering those translated models, and it does not by itself tell you the terms for the Sail tool itself. THIRD_PARTY_FILES.md sits at the top level, which is where the provenance of the bundled components is recorded.

The cost of adding a new model is where the tooling earns its keep. A CHERI extension or a RISC-V variant is a difference in instruction semantics, and writing that as executable, type checked code gives you the emulator, the documentation and the proof obligations at once. The reverse is also true. If your ISA description is prose with a few diagrams, the first thing you have to do is decide what can be expressed in a first-order imperative language with dependent numeric types, and anything outside that subset will not get the tooling. For an architecture with complex microarchitectural behaviour rather than architectural behaviour, that boundary is where the work stops.

Editorial conclusion

Sail suits hardware and architecture teams that need one executable, checkable source of truth for an ISA, and it suits security researchers who want to reason about instruction semantics rather than read prose. It is the wrong tool for application developers, for anyone who only needs to emulate a CPU, and for architectures whose behaviour cannot be captured in the imperative subset the language covers. Before starting a model, check which backends you actually need against the current status of each one, since the README notes that support is not uniform across models, and read INSTALL.md and the Makefile targets because the repository builds with dune and OCaml rather than shipping a single installable package.

Frequently asked questions

Official sources

1. Issues
2. README
3. Releases
4. rems-project/sail on GitHub