Authors constructed a bare-metal CPS VM called Encore! that runs Rocq-extracted Scheme on microcontrollers and demonstrated structuring firmware as a pure state-transition function whose core is fully provable in Rocq.
Formal verification of a realistic compiler.Communications of the ACM, 52(7):107–115, July 2009
19 Pith papers cite this work, alongside 1,127 external citations. Polarity classification is still indexing.
19
Pith papers citing it
1,127
external citations · external index
citation-role summary
background 2
citation-polarity summary
roles
background 2representative citing papers
Full verification of compiler optimizations requires roughly an order of magnitude more development effort than credible compilation when implemented by a coding agent.
Machine-checked model in Rocq establishes that governance is coterminous with expressibility via four primitive constructors in a symmetric monoidal category with capability bounds and verified coherence.
HELIX is an end-to-end verified code generator from mathematical formulations of cyber-physical systems to LLVM IR, using Coq, algebraic transformations, term rewriting, and sparse vector abstractions.
Analysis of 4,913 C projects found 37% use at least one GCC builtin, 10 builtins cover over 30% of projects, 110 cover 90%, builtins are still being added, and many tools have incomplete or incorrect support.
Hardware-faithful verification with a HAL descriptor eliminates all 54 false 16-bit overflow alarms on 123 real IEC 61131-3 programs while preserving robustness proofs.
Quarry splits Rocq proof automation into LLM-proposed decompositions and CoqHammer execution, ranking candidates by learned difficulty, improving success by 7–13 points.
A large open crowdsourced effort verifies substantial parts of the Rust standard library for memory safety properties by integrating complementary verification tools into CI on a forked repository.
Defines formal semantics for C with OpenMP directives extending CompCert, with a guarantee that successful executions are race-free.
A 12,000-line Rocq development proves that effect-level governance on AI workflows is semantically transparent, preserves expressivity, and separates decidable governance predicates from undecidable semantic properties.
WybeCoder interleaves code generation, invariant synthesis, and proof construction to produce verified imperative programs, solving 74% of Verina tasks and 62% of Clever tasks while surpassing prior results.
ReCent-Prover achieves a 22.58% relative improvement over prior state-of-the-art in proved theorems on the CoqStoq benchmark by using reasoning-centric techniques under a fixed LLM invocation budget.
CopilotVerifier generates bisimulation proofs via Crucible symbolic execution and What4 SMT to establish output equivalence and identical crash behavior between Copilot monitors and their compiled forms.
Proposes cryptographic certificates of validity by translating logical policy predicates into succinct proof systems for verifying AI agent actions.
SEMBridge uses a tagless-final interface in a Python prototype to derive executable state transformers and verification conditions from the same loop-free imperative program definitions, tested on five examples up to 729 states.
Human-Certified Module Repositories (HCMRs) are proposed as a new architectural model blending human oversight with automated analysis to certify reusable software modules for safe assembly by humans and AI agents.
The body derives a polynomial-time matroid upper bound on Shannon capacity for affine coordinate-view graphs and a transitivity criterion, while the abstract's NP-completeness and exact-formula claims are absent from the text.
Describes integrating symbolic code reasoning into CS1 and discrete math courses at Haverford and Grinnell, introduces the Orca proof assistant, and poses research questions on effectiveness.
Authors describe designing a compiler course that uses Why3 to teach certified compilation, leading to a verified simple imperative language compiler, along with student and teacher evaluations.
citing papers explorer
-
From Rocq to Metal: A Pipeline for Formally Verified Microcontroller Firmware
Authors constructed a bare-metal CPS VM called Encore! that runs Rocq-extracted Scheme on microcontrollers and demonstrated structuring firmware as a pure state-transition function whose core is fully provable in Rocq.
-
Quantitative Comparison of Credible Compilation and Verification In Coding Agent Compiler Development
Full verification of compiler optimizations requires roughly an order of magnitude more development effort than credible compilation when implemented by a coding agent.
-
Algebraic Semantics of Governed Execution: Monoidal Categories, Effect Algebras, and Coterminous Boundaries
Machine-checked model in Rocq establishes that governance is coterminous with expressibility via four primitive constructors in a symmetric monoidal category with capability bounds and verified coherence.
-
HELIX: Verified compilation of cyber-physical control systems to LLVM IR
HELIX is an end-to-end verified code generator from mathematical formulations of cyber-physical systems to LLVM IR, using Coq, algebraic transformations, term rewriting, and sparse vector abstractions.
-
Understanding GCC Builtins to Develop Better Tools
Analysis of 4,913 C projects found 37% use at least one GCC builtin, 10 builtins cover over 30% of projects, 110 cover 90%, builtins are still being added, and many tools have incomplete or incorrect support.
-
ESBMC-Arduino: Closing the Deployment Gap for Formal Verification of Open-Hardware PLCs
Hardware-faithful verification with a HAL descriptor eliminates all 54 false 16-bit overflow alarms on 123 real IEC 61131-3 programs while preserving robustness proofs.
-
Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
Quarry splits Rocq proof automation into LLM-proposed decompositions and CoqHammer execution, ranking candidates by learned difficulty, improving success by 7–13 points.
-
Verifying the Rust Standard Library
A large open crowdsourced effort verifies substantial parts of the Rust standard library for memory safety properties by integrating complementary verification tools into CI on a forked repository.
-
A Formal Semantics of C with OpenMP Parallelism (Extended Version)
Defines formal semantics for C with OpenMP directives extending CompCert, with a guarantee that successful executions are race-free.
-
Effect-Transparent Governance for AI Workflow Architectures: Semantic Preservation, Expressive Minimality, and Decidability Boundaries
A 12,000-line Rocq development proves that effect-level governance on AI workflows is semantically transparent, preserves expressivity, and separates decidable governance predicates from undecidable semantic properties.
-
WybeCoder: Verified Imperative Code Generation
WybeCoder interleaves code generation, invariant synthesis, and proof construction to produce verified imperative programs, solving 74% of Verina tasks and 62% of Clever tasks while surpassing prior results.
-
On Reasoning-Centric LLM-based Automated Theorem Proving
ReCent-Prover achieves a 22.58% relative improvement over prior state-of-the-art in proved theorems on the CoqStoq benchmark by using reasoning-centric techniques under a fixed LLM invocation budget.
-
Trustworthy Runtime Verification via Bisimulation (Extended Experience Report)
CopilotVerifier generates bisimulation proofs via Crucible symbolic execution and What4 SMT to establish output equivalence and identical crash behavior between Copilot monitors and their compiled forms.
-
Cryptographic certificates of validity for trustworthy AI
Proposes cryptographic certificates of validity by translating logical policy predicates into succinct proof systems for verifying AI agent actions.
-
SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
SEMBridge uses a tagless-final interface in a Python prototype to derive executable state transformers and verification conditions from the same loop-free imperative program definitions, tested on five examples up to 729 states.
-
Human-Certified Module Repositories for the AI Age
Human-Certified Module Repositories (HCMRs) are proposed as a new architectural model blending human oversight with automated analysis to certify reusable software modules for safe assembly by humans and AI agents.
-
Coordinate-View Confusability Graphs and Matroid Rank Certificates
The body derives a polynomial-time matroid upper bound on Shannon capacity for affine coordinate-view graphs and a transitivity criterion, while the abstract's NP-completeness and exact-formula claims are absent from the text.
-
A Bridge Anchored on Both Sides: Formal Deduction in Introductory CS, and Code Proofs in Discrete Math
Describes integrating symbolic code reasoning into CS1 and discrete math courses at Haverford and Grinnell, introduces the Orca proof assistant, and poses research questions on effectiveness.
-
Introducing Certified Compilation in Education by a Functional Language Approach
Authors describe designing a compiler course that uses Why3 to teach certified compilation, leading to a verified simple imperative language compiler, along with student and teacher evaluations.