In the world of formal methods for software, proof assistants enable a common workflow that has been used to verify the correctness of a wide variety of systems:
- write programs in the functional language within the proof assistant
- state correctness theorems about those programs
- prove the theorems using a mix of automation and manual steps
- and extract the proved programs automatically into popular functional languages like OCaml.
Among the benefits of the approach are quite effective ways to decompose proofs modularly into lemmas, which may naturally include quantifiers, so that they apply to infinite families of systems, rather than concrete versions.
In contrast, while formal methods have made more headway in industry as applied to hardware systems, it has been rare to verify full systems modularly (e.g., prove processor and memory-cache system separately) or with significant parameterization (e.g., a proof applies for any number of cores in a processor).
Kami is a framework bringing to hardware circuits the benefits of the proof-assistant approach to software verification. With Kami, hardware designs are coded inside of the Coq proof assistant, proved correct, and extracted automatically to circuits that can be synthesized for FPGAs or silicon.
Flexible parameterization comes ``for free'' from adopting Coq as a metalanguage, and modularity comes via application of the ideas of labeled transition systems from the world of process algebra.
