Open Source Correctness Proof for Ibex

By lowRISC C.I.C.

January 14, 2026

Explaining the entirely open source flow for proving correctness of Ibex with respect to the Sail specification.

In recent years, lowRISC has developed a formal proof of correctness for Ibex, in which equivalence of Ibex against the RISC-V specification is proved, with up to some caveats. This proof previously had been run exclusively with a commercial model checker, but has now been entirely reproduced with a fully open source toolchain, using a combination of Slang, Yosys and rIC3. The open source proof now runs in Continuous Integration (CI) for Ibex, with all properties converging in under 45 minutes on a good machine, far faster than initially anticipated.

The proof establishes that the Ibex RTL and the Sail RISC-V specification will produce the same sequence of memory operations in the same order forever, provided equivalent inputs. This transitively implies that any security property of RISC-V itself is implicitly proved of Ibex. There are naturally some caveats for this proof, most notably surrounding instruction fetch, unspecified behaviours, and the precise configuration of Ibex used in the proof, though they are relatively minor.

Ibex formal verification pipeline at the time of writing

By reproducing this correctness proof with entirely free and open source tools, anyone, even those without access to commercial tools, may verify our claims straightforwardly. The full toolchain can be found here.

RISC-V is specified both as traditional prose, and in the Sail architecture definition language, which formally describes the semantics of everything that an implementation of RISC-V, such as Ibex, must do. In our flow, this Sail specification is first compiled to a combinational SystemVerilog module, representing the execution of one ‘event’ (one instruction, fetch error or interrupt), which maps one architectural state (e.g. the register files) to the next, given some inputs. This is done almost identically as for commercial tools, with small changes to the Sail compiler to improve output size.

Bundled with the formal properties, and Ibex itself, this can be loaded into commercial tools straightforwardly, where verification can begin.

Alternatively, for the open source flow, the design is loaded into Yosys, which is a popular open source hardware synthesis framework. This is done via Slang, an entirely open source parser for SystemVerilog of steadily increasing popularity, which can operate as a frontend for Yosys in the form of yosys-slang. Yosys-slang lacks out of the box support for SVA (the SystemVerilog Assertion language), and so lowRISC extended it to lower a subset of SVA to RTLIL (the internal representation of circuits in Yosys). Since then, new work has begun on a more complete implementation of SVA for Yosys-slang.

Once loaded, Yosys can optimise and map the design, eventually producing an Aiger file, which is a simple and highly compact representation of logic circuits. Unfortunately, while powerful, Yosys can be slow on larger designs (the compiled specification in particular is very large, even after work to help reduce the size). Just one Aiger file containing all ~900 properties is therefore generated, which can then be modified straightforwardly to allow for separateseperate proofs of individual properties or property groups. This allows us to use assume-guarantee logic, where each proof step is granted the properties of all the previous steps as assumptions.

These specialised files are passed to rIC3, an open source model checker which performs well under even large designs. rIC3 will either find a counterexample and return a trace, or will find a proof, where it can provide a verifiable certificate. The Ibex correctness properties prove quickly under rIC3, largely due to their heavily optimised nature, with most proving by 1 or 2-induction.

Specialisation and the handling of many concurrent invocations of rIC3 is handled by a proof conductor program, which makes up the ‘frontend’ of our flow. It also handles the breaking down of the many properties into fast-to-prove-together groups, the caching of proof strategies, and efficient scheduling of the model checker.

In the event of a counterexample, a VCD file (suitable for use in gtkwave or tools similar) can also be extracted by analysing the Aiger witness file rIC3 produces. In practice, most trace analysis should likely still be done in a tool such as Cadence’s Jasper, which at this time still has far better debugging capabilities than any open source tool does (though this would make for an excellent future project).

Together, this pipeline is a complete, coherent flow for efficiently running large formal setups with exclusively open source software, especially those with assume-guarantee setups such as that in our Ibex verification. We hope that this work will help further the use of formal in open source hardware, and that it will help provide confidence in the correctness and security of Ibex.

If you’re interested in finding out more, email us at info@lowrisc.org.