LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification

Zhipeng Cao; Peiyang Song; Nikolaus Vertovec; Weiru Cui; Zhihao Yang; Mingkang Liu; Luxia Lin; Bai Xue

eess.SYOct 21, 2026

LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification

Authors: Zhipeng Cao, Peiyang Song, Nikolaus Vertovec, Weiru Cui, Zhihao Yang, Mingkang Liu, Luxia Lin, Bai Xue,

Organizations: Institute of Software, Chinese Academy of Sciences (CAS) · School of Advanced Interdisciplinary Sciences, University of Chinese Academy of Sciences · Language Technologies Institute, School of Computer Science, Carnegie Mellon University · Computing + Mathematical Sciences Department, California Institute of Technology ·

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.

Figures & tables

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 unresolved obligations are fed back to the Proposal Agent for the next candidate.

Task	Certificate conditions	Theorems
Stability	$V(0)=0$ , $V(x)>0$ for $x\neq 0$ , and $\mathcal{D}_{\pi}V\leq 0$ (or $<0$ for $x\neq 0$ )	Thm. 1
ROA	Lyapunov $V$ and corr. sublevel set $\Omega_{c}$ with $\mathcal{X}_{I}\subseteq\Omega_{c}\subseteq\mathcal{N}$	Cor. 1
Invariant Set	Barrier $B$ with $B<0$ on $\mathcal{X}_{U}$ , boundary/invariance condition	Thm. 2 , Cor. 2
Safety	Barrier $B$ with $B\geq 0$ on $\mathcal{X}_{I}$ , $B<0$ on $\mathcal{X}_{U}$ , barrier condition	Cor. 3

Table 1: Verification tasks, the corresponding certificate conditions, and the theorems (Appendix C ) that connect them. Sets

\mathcal{X}

\mathcal{X}_{I}

\mathcal{X}_{U}

\mathcal{N}

, and

\Omega_{c}

are defined in Section 2.1 .

Figure 2: DynaCertBench overview by (a) source, (b) verification task, and (c) state dimension, split into the Literature-derived (L), Extended (E), and New (N) tiers.

(a) Comparison with existing end-to-end methods
Method	Synthesis	Verification	Systems	Native	Strict	LLM2Cert
1	SMT(Z3)	SMT(Z3)	8	0/8	–	8/8
2	NN CEGIS	SMT	49	8/49	5/8	38/49
3	NN CEGIS	LBP	8	4/8	4/4	7/8
4	RL	SMT	7	1/7	0/1	5/7
5	Poly. NN	SOS/LMI	8	7/8	3/7	8/8

Table 2: End-to-end synthesis and verification results. (a) Comparison with existing pipelines under the same time limit; each baseline runs on the subset of systems it supports, and the bottom row aggregates over the union of these subsets. (b) Ablations of LLM2Cert on the full 105-system benchmark under strict conditions.

Figure 3: End-to-end results. (a) Systems verified by LLM2Cert and by the union of baselines on the 51 baseline-supported systems. (b) Verified systems vs. per-system wall-clock time for the three LLM2Cert configurations. (c) Gain contributed by each component over one-shot proposal.

	Polynomial ( $N_{\mathrm{sys}}=41$ )			Non-polynomial ( $N_{\mathrm{sys}}=40$ )
Strategy	Verified	Time/sys.	Lean/sys.	Verified	Time/sys.	Lean/sys.
All-SMT	41/41	1.65	0.0%	18/40	8.30	0.0%
All-Lean	30/41	511.99	100.0%	34/40	638.44	100.0%
Routed	41/41	2.49	0.0%	40/40	239.05	72.5%

Table 3: Fixed-candidate verification on the 81 certificates verified by the full framework, split by polynomial and non-polynomial systems.

Strategy	Repaired obl.	Rounds/obl.	Time/obl.
Generic Retry	1/26	3.58	873.66
Raw Diagnostics	17/26	2.35	491.02
Structured Repair	21/26	2.19	407.42

Table 4: Lean proof repair under three feedback strategies (

N_{\mathrm{obl}}=26

Appendix figures & tables12 assets

Supplementary material from the paper’s appendix.

Appendix

Agent	Message role	Injected by harness	LLM output
Proposal Agent	system + user	specification $R$ , task profile, locked domain/sets, previous counterexample	JSON candidate $C^{(k)}=(W^{(k)},\pi^{(k)})$
Lean Proof-Repair Agent	system + user	locked theorem, definitions, candidate hash, compiler diagnostics, Mathlib search results	JSON proof body, helper lemmas, or cannot_complete
Local LeanRepair	user	frozen proof, target source span, compiler context, verified declarations	LeanLocalPatch or cannot_patch

Appendix

Table 5: Prompt interfaces and evidence flow.

LLM output	Harness action	Result
Candidate JSON	format check, semantic check, compile to $A^{(k)}$	obligation list $\mathcal{M}(A^{(k)})$ and fast screening
Lean proof body	elaboration in pinned Lean/Mathlib	accepted proof, repair feedback, or unresolved trace
cannot_complete	check blocker and optional counterexample	continue proof search or return diagnostics to Proposal Agent

Appendix

Table 6: Harness processing of LLM outputs.

Task	Verified	Success	Tokens/sys. (k)	Time/sys. (s)
Stability	21/26	80.8%	16.00	613.57
ROA	8/12	66.7%	19.63	427.48
Forward-invariance	7/13	53.8%	16.07	704.73
Safety	45/54	83.3%	13.95	377.58
Overall	81/105	77.1%	15.22	471.96

Appendix

Table 7: Full end-to-end coverage and mean cost by task.

Agent	Usage calls	Input (k)	Reasoning (k)	Visible output (k)
Proposal synthesis	119	2.24	3.66	0.44
Verification router	170	1.90	0.08	0.08
Lean proof agent	199	7.35	3.17	1.39

Appendix

Table 8: Mean model usage per call with a returned usage receipt.

	Single backend		Full		SMT-first + Lean
Task	All-SMT	All-Lean	Verified	Lean/active	Verified	Lean/active
Stability	13/21	15/21	21/21	21/93	20/21	9/93
ROA	6/8	6/8	8/8	3/41	8/8	3/41
Forward-invariance	4/7	6/7	7/7	3/24	7/7	3/24
Safety	36/45	37/45	45/45	16/138	45/45	11/138
Total	59/81	64/81	81/81	43/296	80/81	26/296

Appendix

Table 9: Task-wise coverage and Lean allocation on the frozen certificates.

Task	All-SMT	All-Lean	Full	SMT-first + Lean
Stability	2.47	590.31	141.96	100.33
ROA	1.97	489.94	143.35	80.35
Forward-invariance	0.85	697.66	108.72	129.01
Safety	4.71	569.91	106.11	88.66
Overall	3.68	579.17	119.31	94.28

Appendix

Table 10: Mean verification time per verified certificate, in seconds.

Strategy	Verified	Tokens/sys. (k)	Time/sys. (s)	Lean obl.
All-SMT	59/81	0.00	3.68	0
All-Lean	64/81	24.87	579.17	296
Routed (Full)	81/81	8.34	119.31	43
SMT-first + Lean	80/81	9.15	94.28	26

Appendix

Table 11: Verification coverage, recorded model usage, and mean time.

Obligation	Active	Lean	Time (s)
Equilibrium/value	58	0	101.86
Positivity/quadratic bounds	35	0	63.06
Set containment	58	0	68.32
Unsafe separation	52	3	884.32
Control admissibility	9	0	24.32
Continuous decrease/exp. decay	73	17	5423.25

Appendix

Table 12: SMT-first + Lean allocation and summed time by obligation type.

Strategy	Calls	Input	Reasoning	Visible output	Total/obl.
Generic Retry	95	534.64	129.07	68.02	28.14
Raw Diagnostics	71	445.62	58.75	74.74	22.27
Structured Repair	66	534.71	70.92	90.59	26.78

Appendix

Table 13: Recorded model usage for RQ3 repair; token values are in thousands.

Last recorded event	Systems
Lean call timeout or shared-deadline exhaustion	10
No parsed candidate before the shared deadline	6
Invalid Lean proof output	3
Lean helper-module timeout	2
Lean compiler timeout	1
API rate limit during a Lean call	1

Appendix

Table 14: Last recorded event for the 24 unresolved Full runs.

No.	Curation rule	Operational criterion	Treatment	Source papers	BarrierBench	Total
1	Exact duplicate benchmark instance	Dynamics, task, sets, controller, and constraints are equivalent; only provenance, method, certificate architecture, or result differs.	Retain one canonical instance and merge redundant provenance records.	24	0	24
2	Multiple configurations of the same dynamics	The dynamics are identical, but the domain, task specification, controller, or solver setting differs.	Retain one canonical configuration and discard redundant variants.	22	1	23
3	Closely related variants in the same system family	The basic plant and interaction structure are unchanged; differences mainly concern parameters, coefficients, or minor local modifications.	Retain one representative system from the family.	31	13	44
4	Simplified or structurally redundant dynamics	Feedback cancels nonlinear terms, or additional states are linear, passive, decoupled, or already represented by a simpler system.	Exclude from the independent core benchmark suite.	0	54	54
5	Outside the current core experimental scope	The record is a theoretical illustration, counterexample, hybrid/abstraction model, or simulation-only case.	Exclude from the continuous formal verification track.	8	0	8
Not counted as independent core systems				85	68	153

Appendix

Table 15: Curation of the 233 candidate records into independent core benchmark systems. Each non-retained record is mapped to exactly one primary curation rule in the order shown.

No.	Source	Assigned task(s)	Reported records	Literature- derived	Reported $n\geq 5$	Retained $n\geq 5$
1	Abate et al. (2021)	P1 (8), P4 (3)	17	11	2	1
2	Edwards et al. (2024)	P1 (3), P2 (1), P4 (2)	21	6	1	0
3	Zhao et al. (2020)	P4 (1)	5	1	0	0
4	Liu et al. (2024)	P2 (2)	13	2	9	1
5	Sogokon et al. (2018)	P4 (2)	2	2	0	0
6	Wu et al. (2024)	P4 (3)	22	3	0	0

Appendix

Table 16: Source contributions to the final Literature-derived tier. Reported counts refer to the 233-record candidate pool. The retained counts and task assignments refer to the 80 Literature-derived instances. P1–P4 denote stability certification, region-of-attraction verification, forward-invariant-set synthesis, and safety verification, respectively.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 345 papers

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems
May 4, 2026Miriam Kranzlmüller, Lukas Koller, Tobias Ladner +1Neural Network Verification Safety-Critical Control
Technical University of Munich, Germany · Ludwig-Maximilians-Universität in Munich, Germany
Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture
May 13, 2026George KoomullilLLM Grounding LLM Auditing
Ascendr, Inc.
k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics
May 19, 2026Ben Wooding, Hongchao Zhang, Taylor T. Johnson +1Control Barrier Functions Formal Verification
Vanderbilt University, Nashville, TN, USA · Newcastle University, Newcastle upon Tyne, UK

May 4, 2026J/K move · Enter open · S save

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems

Miriam Kranzlmüller, Lukas Koller, Tobias Ladner, Matthias Althoff

Technical University of Munich, Germany · Ludwig-Maximilians-Universität in Munich, Germany

Neural Network Verification Safety-Critical Control Formal Verification

Open paper AskPDF arXiv

Barrier certificates are scalar functions over the state space of dynamical systems that separate all unsafe states from all reachable states. The existence of a barrier certificate formally verifies the safety of the dynamical system. Recent approaches synthesize barrier certificates by iteratively training a neural network. In each iteration, the candidate is formally verified - if successful, the barrier certificate is found. Instead, we propose a set-based training approach that tightly integrates verification into training via a set-based loss function that soundly encodes all barrier certificate properties. A loss of zero formally proves the validity of the barrier certificate, collapsing the iterative training and verification into a single training procedure. Our experiments demonstrate that our set-based training approach scales well with the system dimension and naturally handles complex nonlinear dynamics.

Abstract

Formal Verification

Explore similar work

Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems

Proof-Carrying Certificates for LLM Pipelines: A Trust-Boundary Architecture

k-Inductive Neural Barrier Certificates for Unknown Nonlinear Dynamics