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 first round of work centered on the Bedrock framework and led up to the first proof-generating automatic pipeline from relational specifications to assembly.
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.