Tools for building digital hardware with machine-checked proofs of correctness
We're developing tools to turn the Coq proof assistant into the ideal digital-hardware IDE. We support writing hardware designs at a variety of levels of abstraction, proving them correct, and synthesizing to RTL. We generally build processors implementing the RISC-V instruction-set family.
Our first round of work centered on the Kami framework and led up to an embedded-systems case study with a single Coq theorem covering both the hardware and software parts ("everything digital").
Our second round of work centers on the redesigned Kôika framework, which allows cycle-accurate timing reasoning despite its high level of abstraction. As a result, we can do modular proofs of protection from timing-side-channel attacks. Kôika also supports interesting software-style tools for debugging and simulation.
