{"ID":3009285,"CreatedAt":"2026-06-03T04:17:48.870468959Z","UpdatedAt":"2026-06-03T20:38:10.546707057Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2606.02651","arxiv_id":"2606.02651","title":"From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware","abstract":"Enforcing invariants in safety-critical systems is increasingly urgent as AI-generated code becomes widespread. Unfortunately, the runtimes required to support high-level specification languages are too large for most embedded targets. In this article, we show how formally verified firmware is achievable today. We built Encore!, a bare-metal Continuation Passing Style (CPS) virtual machine (VM) that runs Rocq-extracted Scheme on microcontrollers. We also show how to structure firmware as a pure state-transition function, making its core fully provable in Rocq while keeping the unverified host layer constant regardless of firmware complexity. Large Language Model (LLM)-assisted tactic synthesis fits naturally into this workflow: formal theorem statements replace manual code review, allowing AI-generated firmware to prove itself.","short_abstract":"Enforcing invariants in safety-critical systems is increasingly urgent as AI-generated code becomes widespread. Unfortunately, the runtimes required to support high-level specification languages are too large for most embedded targets. In this article, we show how formally verified firmware is achievable today. We buil...","url_abs":"https://arxiv.org/abs/2606.02651","url_pdf":"https://arxiv.org/pdf/2606.02651v1","authors":"[\"Valentin Bergeron\",\"Karolina Gorna\"]","published":"2026-05-31T21:14:54Z","proceeding":"cs.PL","tasks":"[\"cs.PL\",\"cs.LO\",\"cs.SE\"]","methods":"[\"Large Language Model\",\"Language Model\"]","has_code":false}