Documentation MRiscX🔗

This documentation provides a brief introduction to the domain-specific language (DSL) MRiscX. MRiscX was designed to lower the barrier to entry into the world of formal methods. Embedded in Lean, MRiscX enables RISC-V assembly code to be easily annotated with formal specifications, which can then be interactively verified. By allowing the correctness of assembly programs to be proven with minimal effort, MRiscX significantly simplifies the process of getting started with formal methods.

We begin with a short introduction to what MRiscX is and what it looks like. Next, the fundamentals are explained to provide the theoretical background on which this DSL is built and to demonstrate how it can be used in practice. Finally, we show how MRiscX can be applied to verify RISC-V assembly code. In particular, we demonstrate how to formulate a specification of a program as a Hoare triple and provide guidance on applying the Hoare rules, along with custom tactics to carry out the process of proving and verify the program’s formal correctness. Finally, some limitations this DSL currently has are be presented.

For an introduction in video form, you can watch this presentation of MRiscX at Lean Together 2026.

If there are any questions, do not hesitate to get in touch: [email protected]