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