Tools for building software with machine-checked proofs of correctness
We're developing tools to turn the Coq proof assistant into the ideal software IDE. We support writing programs at a variety of levels of abstraction and proving them correct. We also support proof-generating compilation from higher-level languages to lower-level languages.
Our second round of work centers on the redesigned Bedrock2 framework and bottoms out in RISC-V machine code, with connections to verified hardware as well. A recent milestone is a single Coq theorem covering both the hardware and software parts ("everything digital") of a simple embedded system.
