Miralis

Virtual firmware monitor for RISC-V with formal verification via Kani.

Virtual firmware monitor for RISC-V running below M-mode firmware, providing isolation and policy enforcement via sandbox and Keystone policies. Includes a Rust RISC-V ISA translator, benchmark scripts, and formal verification via Kani. Supports Docker and manual setup. SOSP'25 artifact.