Kami is a library that turns Coq into an IDE for digital hardware development, based on a clean-slate reimplementation of a core of the Bluespec language. We span the gap from mathematical specifications to hardware circuit descriptions (RTL netlists). We support specifying, implementing, verifying, and compiling hardware, reasoning at a high level about particular hardware components but in the end deriving first-principles Coq theorems about circuits. No part of Kami need be trusted beside the formalization of low-level (Verilog-style) circuit descriptions; all other aspects have end-to-end correctness proofs checked by Coq. Hardware designs are broken into separately verified modules, reasoned about with a novel take on labeled transition systems. Furthermore, Coq provides a natural and expressive platform for metaprogramming, or building verified circuit generators, as for a memory caching system autogenerated for a particular shape of cache hierarchy, or a CPU generated given a number of concurrent cores as input.

We have been developing a candidate official formal specification for RISC-V, which stands a good shot at being ratified soon as such by the RISC-V Foundation.  The spec now includes virtual memory and is able to pass all the official RISC-V machine-code tests that aren't marked as specific to particular extensions.  We should be able to boot Linux on the specification soon, running as a simulator.

A verified processor exists providing all that functionality, though we are still working on debugging the specification, since the current version isn't quite able to boot an operating system (so the specification must be out-of-synch with software expectations somehow).