Formally Verified Certification of Constraint Programming Proofs

How Powerful are LLMs in Generating Formal Program Specifications?

Coins is introduced, a Rocq based evaluation framework that assesses specification quality by instantiating specifications under evaluation on trusted test cases and generating concrete proof obligations, and finds that accurate specification evaluation, rather than model scaling alone, is central to understanding the power of LLMs for specification synthesis.

Proof Production for Satisfiability Modulo Finite Fields with Proof Checking in Pacheck and Lean

LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean

This work introduces a framework that addresses both verification levels in the Lean theorem prover, and can be used to prove formulation-level properties, such as equivalence, equisatisfiability, and the correctness of symmetry-breaking constraints, parametrically for entire problem families.

A Natively Parallel Proof Framework for Clause-Sharing SAT Solving

PalRUP is introduced – an LRUP -based proof format and a bottleneck-free, decentralized parallel checking procedure that only uses the (parallel) file system and is composed of a set of small, sequential trusted components.

Lazy Proof Automation for Separation Logic

The key idea is to implement an entailment checker as a combination of an efficient but unverified prover, suitable for fast-paced interactive proofs, and a proof reconstruction procedure that takes the prover’s trace and produces a certificate of entailment validity that can be checked a posteriori.

Foundational Refinement Proofs for Deployed Bytecode, at the Price of Tokens

Relating low-level executable code to a high-level account of its behavior has been a central concern of programming-language research for decades. From formally verified compilers to translation validators, certifying compilers, and proof-carrying code, each approach chooses between laborious but foundational mechanized proofs and automation that costs completeness, generality, and an increased trusted base. Recently, large language models (LLMs) have begun to change the economics of formal verification. Agentic proof development is now capable of producing machine-checked proofs at a scale and speed that were previously out of reach. In this paper, we evaluate the capabilities of LLMs to produce foundational, machine-checked proofs of refinement between executable code and its high-level specification, as post hoc, per-artifact certificates. We study this in the context of the Ethereum Virtual Machine (EVM), a low-level virtual machine that executes smart contracts on the Ethereum blockchain. We build EquiVM, a foundational framework in Lean comprising an executable EVM semantics and a specification language that characterizes the intended behavior of smart contracts, but commits to no source language or compilation toolchain. In EquiVM, refinement is stated for deployed bytecode of arbitrary provenance, interaction with unknown code is part of the semantics, and each proof is a replayable, machine-checked certificate. No previous technique achieves this combination. Using frontier commercial LLMs, twenty-three real-world contracts are proved end to end with minimal human guidance, among them most of the MakerDAO stablecoin system, at up to a hundred million tokens and a hundred hours of proof time per contract. We conclude that foundational mechanized proofs can now be bought at the price of tokens, and that this shift can reshape how verification frameworks are architected.