An LLM Proof-Repair agent writes kernel-checked Lean proofs for Lyapunov/barrier certificate obligations that SMT solvers cannot discharge or cannot encode.
Abstract
Lyapunov functions and barrier certificates give state-space guarantees of stability and safety, but synthesizing and verifying them—especially for nonlinear, high-dimensional systems—remains an open challenge. Existing pipelines verify candidates with numerical solvers (sum-of-squares programs), interval methods, or satisfiability-modulo-theories (SMT) solvers, which often require relaxations, are conservative, or scale poorly with model dimension and nonlinearity. These limitations have also shaped benchmark design: standard test suites are dominated by low-dimensional polynomial systems chosen to suit what solvers can handle rather than what engineering applications require. We address both sides of this challenge. First, we introduce DynaCertBench, a benchmark of 105 instances: 80 non-redundant systems curated from the literature, extended with high-dimensional and control-constrained variants and new nonlinearly coupled systems, comprehensively spanning stability, region-of-attraction, forward-invariance, and safety tasks. Second, we present LLM2Cert, an LLM-driven framework that synthesizes candidate certificates and verifies them against their proof obligations: each obligation is routed to an SMT solver or directly to the Lean Proof-Repair agent. On DynaCertBench, LLM2Cert verifies 81 of 105 instances ($77.1\%$), a $17.1$ percentage point improvement over one-shot proposal without feedback. On the 81 fixed certificates, LLM2Cert verifies 22 that All-SMT leaves unresolved. Code and data are available at https://github.com/FormalCert-AI/llm2cert.
Problem
Synthesizing and verifying Lyapunov functions and barrier certificates for nonlinear, high-dimensional systems is hard. SOS, interval, and SMT verifiers rely on relaxations, are conservative, or scale poorly. Existing benchmarks are biased toward low-dimensional polynomial systems that suit these solvers.
Approach
DynaCertBench contains 105 instances covering stability, region-of-attraction, forward-invariance, and safety tasks, each posed with its exact, unrelaxed conditions. LLM2Cert uses an LLM Proposal Agent to propose candidate certificates and policies, which induce proof obligations and are first screened by sampling. A router sends each obligation to an SMT solver or to a Lean Proof-Repair Agent. Obligations unresolved by SMT, or with no SMT encoding, are escalated to Lean, and counterexamples are fed back to the Proposal Agent.
Figure 1: LLM2Cert framework. The Proposal Agent proposes a candidate certificate (and policy), which induces a list of proof obligations. Obligations without a compatible SMT encoding go directly to Lean. For the remaining obligations, the router selects either direct SMT or direct Lean. Obligations left unresolved by SMT are escalated to the Lean Proof-Repair Agent. Counterexamples and unresolve
Results
LLM2Cert verifies 81 of 105 instances (77.1%), 17.1 percentage points more than one-shot proposal without feedback. On the 81 fixed certificates, routing verifies 22 that All-SMT leaves unresolved. Structured repair fixes 21 of 26 failing Lean obligations.
