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

• URL: http://arxiv.org/abs/2606.02651v1
• Date: Sun, 31 May 2026 21:14:54 GMT
• Title: From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware
• Abstract summary: In this article, we show how formally verified firmware is achievable today.<n>We built Encore!, a bare-metal Continuation Passing Style virtual machine (VM) that runs Rocq-extracted Scheme on microcontrollers.<n>We also show how to structure firmware as a pure state-transition function, making its core fully provable in Rocq.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• DeepRepro: State-Aware Subplanning for Paper-to-Code Reproduction in Evolving Repositories [116.27249583403871]
  We propose a state-aware framework for paper-to-code reproduction based on execution-state-aware subplanning.<n>DeepRepro transforms evolving repository states and runtime feedback into fine-grained implementation subplans.<n>Experiments on PaperBench Code-Dev show that DeepRepro consistently outperforms strong scientific and commercial code-agent baselines.
  arXiv  Detail & Related papers  (2026-08-27T02:54:30Z)
• Show Me The Money: An Exercise in Proof-Driven Software Understanding [1.678913049066618]
  We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book.<n>We produce artifacts that make it easy for code changes to be checked against established invariants.<n>This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.
  arXiv  Detail & Related papers  (2026-07-17T20:39:40Z)
• Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering [40.048798975817924]
  Vibe coding is fast and may be adequate for low-criticality consumer software.<n>For safety-critical systems governed by DO-178C, IEC 61508, or ISO 26262, it offers no path to certification.<n>We present Forge, a closed-loop pipeline that guides vibe coding through formal verification.
  arXiv  Detail & Related papers  (2026-06-21T10:01:45Z)
• ChipMATE: Multi-Agent Training via Reinforcement Learning for Enhanced RTL Generation [55.947962672433675]
  ChipMATE is the first self-trained multi-agent framework for RTL generation.<n>Inspired by industrial practice, ChipMATE pairs a Verilog agent with a Python reference-model agent that mutually verify each other's outputs.<n>ChipMATE achieves 75.0% and 80.1% pass@1 on VerilogEval V2 with 4B and 9B base models.
  arXiv  Detail & Related papers  (2026-05-13T01:04:21Z)
• Autoformalizing Memory Specifications with Agents [3.897906533095668]
  We show how to formalize memory chip specifications into a formal representation called DRAMPyML.<n>This can be used for the generation of SystemVerilog assertions, stimulus, and functional coverage.<n>We also release our benchmarking dataset, DRAMBench, which can be used to evaluate the evolution of model capabilities.
  arXiv  Detail & Related papers  (2026-04-30T02:01:48Z)
• Residual Context Diffusion Language Models [90.07635240595926]
  Residual Context Diffusion (RCD) is a module that converts discarded token representations into contextual residuals and injects them back for the next denoising step.<n>RCD consistently improves frontier dLLMs by 5-10 points in accuracy with minimal extra computation overhead.
  arXiv  Detail & Related papers  (2026-01-30T13:16:32Z)
• HardSecBench: Benchmarking the Security Awareness of LLMs for Hardware Code Generation [24.138048137437078]
  Large language models (LLMs) are being increasingly integrated into practical hardware and firmware development pipelines for code generation.<n>This research gap motivates us to design a benchmark for assessing security awareness under realistic specifications.<n>We introduce HardSecBench, a benchmark with 924 tasks spanning Verilog Registers Transfer Level (RTL) and firmware-level C, covering 76 hardware-relevant Common Weaknession (CWE) entries.
  arXiv  Detail & Related papers  (2026-01-20T11:27:40Z)
• From Completion to Editing: Unlocking Context-Aware Code Infilling via Search-and-Replace Instruction Tuning [81.97788535387286]
  We propose a framework that internalizes the agentic verification-and-editing mechanism into a unified, single-pass inference process.<n>With minimal data, SRI-Coder enables Chat models to surpass the completion performance of their Base counterparts.<n>Unlike FIM-style tuning, SRI preserves general coding competencies and maintains inference latency comparable to standard FIM.
  arXiv  Detail & Related papers  (2026-01-19T20:33:53Z)
• SwingArena: Competitive Programming Arena for Long-context GitHub Issue Solving [90.32201622392137]
  We present SwingArena, a competitive evaluation framework for Large Language Models (LLMs)<n>Unlike traditional static benchmarks, SwingArena models the collaborative process of software by pairing LLMs as iterations, who generate patches, and reviewers, who create test cases and verify the patches through continuous integration (CI) pipelines.
  arXiv  Detail & Related papers  (2025-05-29T18:28:02Z)
• LLM4EDA: Emerging Progress in Large Language Models for Electronic Design Automation [74.7163199054881]
  Large Language Models (LLMs) have demonstrated their capability in context understanding, logic reasoning and answer generation. We present a systematic study on the application of LLMs in the EDA field. We highlight the future research direction, focusing on applying LLMs in logic synthesis, physical design, multi-modal feature extraction and alignment of circuits.
  arXiv  Detail & Related papers  (2023-12-28T15:09:14Z)
• AIM: Automatic Interrupt Modeling for Dynamic Firmware Analysis [14.623460803437057]
  We present AIM, a generic, scalable, and hardware-independent dynamic firmware analysis framework. AIM covers interrupt-dependent code in firmware by a novel, firmware-guided, Just-in-Time Interrupt Firing technique. Our framework covered up to 11.2 times more interrupt-dependent code than state-of-the-art approaches.
  arXiv  Detail & Related papers  (2023-12-02T18:06:22Z)
• HIVE: Scalable Hardware-Firmware Co-Verification using Scenario-based Decomposition and Automated Hint Extraction [2.977255700811213]
  Hardware-firmware co-verification is critical to design trustworthy systems. There are promising avenues to reduce the state space during firmware verification through manual abstraction of hardware or manual generation of hints. In this paper, we effectively combine the scalability of simulation-based validation and the completeness of formal verification.
  arXiv  Detail & Related papers  (2023-09-14T19:24:57Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.