MRiscX: Certified RISC-V interpreter with Hoare logic as a DSL in Lean

Abstract: This talk introduces MRiscX, a domain-specific language (DSL) designed to lower the barrier to entry into the world of formal methods. Embedded in Lean, MRiscX allows RISC-V assembly code to be easily annotated with formal specifications, which can then be interactively verified. By enabling the correctness of assembly code to be proven with minimal effort, MRiscX makes it significantly easier for newcomers to get started with formal methods.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

Lean Together 2026