KamiA Coq framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components with high developer productivity. Kami is a Coq framework to support implementing, specifying, verifying, and compiling Bluespec-style hardware components with high developer productivity. The core of the approach is modular proofs of hardware components. We aim for specifications and p
