RISC-V is an open instruction set architecture designed to be practical. Basically, it’s a cool open standard that also aims for practicality and extensibility.

I’m working with Professor Adam Chlipala and Thomas Bourgeat to develop a formal, friendly, and runnable RISC-V specification. The idea is to clearly define the correct behavior from RISC-V in a format that is both human-readable and machine-readable. At present, this is in the form of an emulator written in Haskell. This project is available on GitHub!

alt text