From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware

Valentin Bergeron, Karolina Gorna

Enforcing invariants in safety-critical systems is increasingly urgent as AI-generated code becomes widespread. Unfortunately, the runtimes required to support high-level specifica…