The RISC-V Foundation (riscv.org) has a task group to develop a Formal Spec for the RISC-V Instruction Set Architecture. The group has been pursuing several approaches: - 3 are written in Haskell - 1 is in SAIL, a DSL with dependent types, intended for ISA specs - 1 is in Kami, a DSL in Coq Most of them are complete enough to boot Linux, i.e., they are not for toy subsets of the ISA. They are expected and intended to become the "official" ISA spec for RISC-V, and to be used in anger, for compliance testing, formal verification of compilers, hardware designs, etc. We would love to get community feedback on these approaches. The following link provides an overview, and links to individual web sites (all on GitHub) for the 5 approaches, and information on how to provide feedback: https://github.com/riscv/ISA_Formal_Spec_Public_Review Thanks very much in advance! Rishiyur Nikhil, Chair, ISA Formal Spec Technical Group