LLM2Cert: LLM Synthesis of Certificates with SMT/Lean Verification

1 INTRODUCTION

• Existing SOS, interval, and SMT methods face numerical or δ-SAT caveats, ad-hoc relaxations, and poor scaling on high-dimensional, strongly nonlinear systems.Lean offers an exact theorem checked by a small trusted kernel.Source: §1 · p. 2
• Standard benchmarks remain mostly low-dimensional, parameter-free systems on tightly bounded domains, leaving high-dimensional engineering-relevant cases scarce.Existing datasets are described as implicitly designed around solver limits.Source: §1 · p. 2
• DynaCertBench covers stability, region-of-attraction, forward-invariance, and safety tasks, including high-dimensional, control-constrained, strongly nonlinear, and parameterized systems.Each instance uses exact, unrelaxed certificate conditions.Source: §1 · p. 2
• LLM2Cert integrates SMT and Lean for continuous- and discrete-time certificate verification, delegating obligations SMT cannot discharge to Lean.This design avoids conservative SMT assumptions including Taylor approximations, δ-satisfiability, and excluding a neighborhood around the origin.Source: §1 · p. 2
• SMT and Lean are complementary: SMT can discharge obligations efficiently, while Lean resolves others left unresolved by SMT.The framework uses SMT for faster verification and counterexample generation, with Lean finalizing formal proofs.Source: §1 · p. 2

2.1 DYNAMICAL SYSTEMS AND VERIFICATION TASKS

• Four tasks are considered: equilibrium stability, region-of-attraction verification, forward-invariant set synthesis avoiding unsafe states, and safety from initial states.A scalar certificate instantiates a Lyapunov or barrier function; its change is expressed by a Lie derivative in continuous time or a one-step difference in discrete time.Source: §2.1 · p. 3
• The formulation verifies a proposed candidate set rather than optimizing its size, and tests a specific feedback policy rather than existence of an admissible control at each state.The system definitions specify control inputs, closed-loop dynamics, state domains, initial and unsafe sets, and Lyapunov sublevel sets.Source: §2.1 · pp. 2–3

2.2 SOUNDNESS OF CERTIFICATE CONDITIONS

• Soundness has two layers: Lean proves that each task’s certificate conditions imply the corresponding property, and LLM2Cert verifies that every candidate condition is discharged.Acceptance requires an SMT unsat verdict or a kernel-checked Lean proof.Source: §2.2 · p. 3

3 LLM2CERT: LLM-BASED CERTIFICATE SYNTHESIS WITH SMT AND LEAN VERIFICATION

• LLM2Cert combines LLM candidate synthesis with SMT and Lean verification while keeping the candidate and obligations fixed and never relaxing target statements.The section’s shaded boxes follow System 88 as a running example.Source: §3 · p. 4

3.1 CANDIDATE SEARCH, OBLIGATION LIST, AND FAST SCREENING

• The Proposal Agent parses a symbolic certificate and policy into a typed expression tree, then instantiates the task theorem to produce obligations retaining the original constraints.Finite-state screening can reject a candidate and return violating samples, but passing screening does not guarantee validity and leaves every obligation for formal verification.Source: §3.1 · p. 4

3.2 VERIFICATION ROUTER

• The router sends obligations without compatible SMT encodings directly to Lean and escalates SMT δ-sat or timeout outcomes to Lean for proof of the unchanged statement.An SMT unsat verifies an obligation, while sat returns a counterexample to the Proposal Agent.Source: §3.2 · pp. 4–5

3.3 LEAN PROOF-REPAIR AGENT

• The Lean Proof-Repair Agent may revise only the proof body, using structured feedback on failures, source location, and remaining goals.Accepted proofs must type-check against the fixed theorem and pass an audit rejecting sorry and nonstandard axioms; repair is bounded by time and rounds.Source: §3.3 · p. 5

3.4 SOUNDNESS AND TERMINATION

• A candidate is verified only when every obligation has proof evidence; violations reject it, while obligations still open after the Lean budget leave it unresolved.Counterexamples or failure diagnostics return to the Proposal Agent for another candidate; exhausting the candidate budget is reported as search exhaustion.Source: §3.4 · p. 5
• In the running safety example, three obligations are discharged by SMT and the remaining obligation is proved in Lean, establishing the candidate’s exact safety conditions.The Lean proof is accepted after compiler feedback guides a third attempt.Source: §3.3 · p. 5, §3.4 · p. 6

4.1 MOTIVATION AND DESIGN GOALS

• DynaCertBench keeps exact verification targets and adds high-dimensional, control-constrained systems to benchmarks dominated by low-dimensional polynomial systems.Prior benchmarks often exclude a neighborhood of the origin, approximate transcendental terms with Taylor expansions, or accept δ-sat verdicts.Source: §4.1 · p. 6

4.2 DATA COLLECTION AND CURATION

• The benchmark collects 233 candidates from 15 papers and BarrierBench, then applies five curation rules to retain 80 distinct core systems.Only 7 of 29 nominally high-dimensional entries survive curation; Extended instances scale or modify retained systems, while New instances are constructed high-dimensional systems.Source: §4.2 · p. 6

4.3 DATASET STATISTICS AND ANALYSIS

• The Extended and New tiers raise the number of instances with n ≥5 from 7 to 25, with results reported by tier to distinguish them from the literature-derived core.Figure 2 summarizes the benchmark by source, task, and state dimension.Source: §4.3 · p. 6

5.1 EXPERIMENTAL SETUP

• The evaluation covers stability, region-of-attraction, forward-invariance, and safety tasks, with candidates counted only when every obligation is definitively discharged.It compares end-to-end configurations and also fixes candidates and obligations for backend comparisons.Source: §5.1 · p. 7

5.2 MAIN EXPERIMENT: END-TO-END SYNTHESIS AND VERIFICATION

• LLM2CERT verifies 40/51 instances, while baselines verify 19/51 natively and only 11 remain valid under strict conditions.Among the 51 systems, LLM2CERT verifies 23 that no baseline verifies natively; baselines verify two that LLM2CERT leaves unresolved.Source: §5.2 · p. 8, Table 2 · p. 8

5.3 END-TO-END ABLATIONS

• 81/105 instances are verified by full LLM2CERT, versus 63/105 by One-shot Proposal without feedback.The full framework also improves results by 15.0, 27.3, and 21.4 percentage points on the Literature-derived, Extended, and New tiers, respectively.Source: §5.3 · p. 8, Table 2 · p. 8

5.4 VERIFICATION FRAMEWORK ANALYSIS

• 21 certificates that All-SMT leaves unresolved are verified by All-Lean, all on non-polynomial systems; SMT resolves additional certificates that Lean does not finish within budget.On polynomial systems SMT covers all certificates verified by Lean, while on non-polynomial systems Lean verifies 34/40 versus SMT’s 18/40.Source: §5.4 · p. 9, Table 3 · p. 9
• 58 of 81 fixed certificates are verified by All-SMT within 30 seconds per obligation, rising to 59 at 900 seconds; All-Lean verifies 64/81.On systems it verifies, mean time is 1.65 seconds for polynomial systems and 8.30 seconds for non-polynomial systems with All-SMT, versus 511.99 and 638.44 seconds with All-Lean.Source: §5.4 · p. 9, Table 3 · p. 9
• ROUTED verifies all 81 certificates: SMT discharges 253/296 obligations, while 43/296 reach Lean through escalation, direct routing, or lack of an SMT encoding.The reported routes include 21 after δ-sat or timeout, 19 direct router decisions, and 3 obligations without an SMT encoding.Source: §5.4 · p. 9, Table 3 · p. 9
• Structured Repair repairs 21/26 failed obligations across 15/19 systems, with a mean repair time of 407.42 seconds per obligation.Generic Retry repairs 1/26 obligations and no complete system; Raw Diagnostics repairs 17/26.Source: §5.4 · pp. 9–10, Table 4 · p. 9

6 CONCLUSION

• LLM2CERT verifies 77.1% of DynaCertBench instances end to end, using SMT or kernel-checked Lean proofs for exact certificate conditions.The framework routes per obligation and falls back to Lean when solvers time out or return δ-sat.Source: §6 · p. 10
• DynaCertBench restores high-dimensional, constrained, and nonlinearly coupled systems that solver-oriented datasets have excluded.The conclusion characterizes the benchmark as curated to address those omissions.Source: §6 · p. 10
• The authors describe kernel-checked proof as a foundational first step toward practical verification of synthesized dynamical-system certificates.Source: §6 · p. 10

A LIMITATIONS AND FUTURE WORK

• DynaCertBench remains a curated set of 105 instances, the framework focuses primarily on deterministic systems and prescribed verification domains, and broader dynamics and region-size objectives remain future work.The authors identify high-dimensional, hybrid, and uncertain dynamics, stochastic systems, and explicit optimization of certified sets as directions for extension.Source: A LIMITATIONS AND FUTURE WORK · p. 15

B RELATED WORK

• Certificate synthesis spans parameterized SOS or semidefinite templates, bilinear formulations, and learner–verifier loops, with verifier choice depending on candidate representation.For a fixed certificate, verification approaches include SMT, algebraic decompositions, deductive provers, and proof assistants; their assurance artifacts are not interchangeable.Source: B RELATED WORK · p. 15
• Certificate synthesis requires selecting a witness whose exact stability or safety obligations are true and provable, so the framework separates synthesis, route selection, and Lean proof construction.The loop returns structured failures without changing the frozen theorem.Source: B RELATED WORK · pp. 15–16

C DYNAMICAL MODELS AND NOTATION

• The models cover continuous- and discrete-time dynamics with control inputs, and define closed-loop dynamics and trajectories under a state-feedback policy.The notation includes domains, initial and unsafe sets, and Lyapunov sublevel sets.Source: C DYNAMICAL MODELS AND NOTATION · p. 16, §C.1 · p. 16

C.1 SYSTEM PROPERTIES

• The stated system properties cover stability, region-of-attraction verification, forward-invariant set synthesis, and safety verification for closed-loop trajectories.The safety formulations include an explicit unsafe set or the complement of a prescribed safe domain.Source: §C.1 · p. 16

C.2 CERTIFICATE CONDITIONS

• Lyapunov conditions use positivity and decrease of V to certify stability, asymptotic or exponential stability, and region-of-attraction membership.The region-of-attraction condition uses a compact sublevel set containing the initial set within the specified neighborhood.Source: §C.2 · p. 17
• Barrier conditions on B distinguish unsafe states and constrain boundary behavior or discrete-time updates to support invariant-set and safety guarantees.The corollaries apply when the candidate set is nonempty for invariance, or when B is nonnegative on the initial set for safety verification.Source: §C.2 · p. 17

C.3 VERIFICATION PRINCIPLES

• SMT solvers search for counterexamples to universal conditions, while Lean constructs proof terms checked by its kernel.For dReal, δ-sat concerns a δ-weakened problem and is inconclusive about the original formula; verified certificate conditions imply the corresponding stability or safety theorem.Source: §C.3 · p. 18

D PROMPTS DETAILS IN LLM2CERT

• Prompt interfaces use harness-injected runtime values, with tables summarizing message roles, evidence flow, and output processing.The complete serialized prompts, JSON schemas, and case traces are supplied in supplementary material.Source: D PROMPTS DETAILS IN LLM2CERT · p. 18, Table 5 · p. 18, Table 6 · p. 18

D.1 PROPOSAL AGENT

• The Proposal Agent validates each candidate’s format and semantics, compiles accepted candidates into a representation that induces verification obligations, and uses a task profile to interpret the certificate.The initial prompt requires task-specific theorem conditions, correct continuous- or discrete-time semantics, and—when parameters are fixed—a state-only certificate valid uniformly over the parameter interval.Source: §D.1 · p. 19, §D.1.1 · p. 19

D.1.1 INITIAL PROPOSAL PROMPT

• The initial proposal prompt requires bounded, observation-compatible controllers when applicable and concise JSON expressions with a construction note identifying auxiliary quantities, factorized changes, and explicit verification bounds.It directs the agent to satisfy supplied theorem conditions rather than relaxed numerical surrogates.Source: §D.1.1 · p. 19

D.1.2 PROPOSAL REPAIR PROMPT

• Proposal repair uses confirmed, independently replayed counterexamples to authorize a new candidate; timeouts and proof diagnostics remain evidence, and the verification target cannot be changed.The Lean theorem and obligation list stay locked; task-specific constraints preserve the claimed domain or safety semantics while allowing the region-of-attraction level c to change.Source: §D.1.2 · p. 20

D.2 LEAN PROOF-REPAIR AGENT

• The Lean Proof-Repair Agent handles one obligation at a time, returning a proof body for a fixed theorem that the harness compiles in a pinned Lean/Mathlib environment.The theorem header and generated definitions remain fixed.Source: §D.2 · p. 20, §D.2.1 · p. 20

D.2.1 INITIAL LEAN PROOF PROMPT

• The initial prompt requires proving the exact stated Lyapunov, barrier, or safety condition from locked inputs, including the theorem statement, definitions, system, controller, certificate, and candidate hash.It specifies conditions including positivity, Lie derivatives, decrease, boundary, initial-set, and unsafe-set obligations.Source: §D.2.1 · pp. 20–21
• Proofs must compile, preserve the locked theorem hash, and pass an axiom audit; prompts forbid shortcuts such as sorry, admit, user-defined axioms, unsafe, or external assumptions.The accepted dependency set is propext, Classical.choice, and Quot.sound.Source: §D.2.1 · p. 21

D.2.2 COMPILER-GROUNDED LEAN REPAIR

• Lean proof repair classifies failures and returns relevant compiler or proof evidence within the same locked context, rejecting forbidden proof content and failed axiom audits.The implementation bounds repairs to three format-only repairs, six ordinary proof rounds, and three qualified-name repair rounds.Source: §D.2.2 · pp. 21–22

D.2.3 LEAN PROOF FOLLOW-UP PROMPT

• Follow-up prompts provide compiler diagnostics and repair mode, require fixing reported errors without changing the verification target, and preserve accepted helpers while editing only failing proof components.The response must be either a concrete proof body or a precise blocker.Source: §D.2.3 · p. 22

D.2.4 LOCAL LEANREPAIR PROMPT

• Optional local Lean repair freezes the proof and requests a patch to one compiler-selected source span, preserving unrelated text and disallowing new top-level lemmas.A patch must use verified declarations and can return cannot_patch if the selected line cannot be repaired alone.Source: §D.2.4 · p. 22

D.3 VERIFICATION ROUTER PROMPT

• After deterministic fast checks, the router selects direct Lean or SMT and orders eligible solvers; SMT results are independently checked and may be rescued by Lean4.For bounded fixed parameters, the query keeps the parameter quantified so UNSAT establishes the uniform condition.Source: §D.3 · p. 23

D.4 EXAMPLE INPUT–OUTPUT TRACE

• The recorded System 88 trace shows a parser-rejected certificate assignment corrected after feedback, followed by an SMT timeout and successful Lean proof repair.The first Lean responses had a namespace error and then incorrect theorem application syntax; the next repair compiled, with axioms listed as propext, Classical.choice, and Quot.sound.Source: §D.4 · p. 24
• In the example trace, Z3 and CVC5 discharged unsafe separation, initial containment, and control admissibility; Lean accepted the strict Lie proof, and audited lemmas and a generic theorem closed the remaining obligations.The candidate was finally marked verified.Source: §D.4 · pp. 24–25

E.1 IMPLEMENTATION DETAILS

• Full and fixed-certificate runs use Lean 4.32.2, Mathlib revision 905b95818eb3, Z3 4.15.4, CVC5 1.3.3, Yices 2.7.0, and dReal 4.21.06.1; runs allow up to five candidate rounds and 2,400 seconds.SMT solvers have 30-second timeouts; each Lean obligation allows up to six proof rounds within 900 seconds, and fixed-certificate obligations receive a fresh 900-second budget.Source: §E.1 · p. 25
• Fast screening samples initial, unsafe, and analysis or boundary sets, but passing it does not prove an obligation; candidate, hypothesis, and theorem statements stay frozen during verification.The screen uses 1,500 initial-set samples, 1,500 unsafe-set samples, and 2,000 analysis-region or boundary samples.Source: §E.1 · p. 25
• For each frozen obligation, the harness checks hashes, routes to compatible SMT or direct Lean, and lets the non-ALL-SMT strategy request an audited Lean proof when SMT does not resolve it.ALL-SMT returns unresolved when no compatible encoding or definitive UNSAT verdict is available; an audited task-level closing theorem completes verification.Source: §E.1 · p. 26

E.2 ADDITIONAL RESULTS FOR THE MAIN EXPERIMENT

• ROA has the largest mean recorded token usage, while forward-invariance has the largest mean end-to-end time.Both cost columns average successful systems within each task.Source: §E.2 · p. 26, Table 7 · p. 26
• 81/105 systems are verified across all four task categories in the full end-to-end results.Table 7 reports mean costs over successful systems within each task.Source: Table 7 · p. 26, §E.2 · p. 26
• 488 of 707 recorded calls have returned usage receipts, and the Lean proof agent has the largest mean per-call usage.Visible output excludes reasoning tokens.Source: Table 8 · p. 26, §E.2 · p. 26

Coverage and backend allocation

• 81/81 certificates are covered by Full, while SMT-first + Lean covers 80/81 using 26 Lean obligations; its remaining open obligation is radial unboundedness.Table 9 reports task-wise coverage and Lean allocation on the frozen certificates.Source: Table 9 · p. 27, §E.3 · p. 27

Verification time

• 94.28 s is the mean verification time for SMT-first + Lean, compared with 579.17 s for All-Lean and 3.68 s for All-SMT.Full records a mean of 119.31 s; means are over certificates verified by each strategy.Source: §E.3 · p. 27, Table 10 · p. 27

Recorded model usage

• 9.15k tokens per system for SMT-first + Lean is 63.2% below All-Lean’s 24.87k, while Full uses 8.34k tokens per system.The token comparison uses the common 81-certificate cohort; mean times over verified certificates are 83.7% lower for SMT-first + Lean than All-Lean.Source: §E.3 · p. 27, Table 11 · p. 27

SMT-first verification paths

• SMT discharges 270/296 obligations (91.2%) by unsat within 30 s; 26 Lean paths include δ-sat, timed-out SMT checks, and obligations without SMT encodings.Continuous decrease or exponential decay and discrete inductiveness account for 20/26 Lean obligations (76.9%) and 74.8% of summed condition time; SMT verifies equilibrium, positivity, and control-admissibility checks.Source: §E.3 · pp. 27–28, Table 12 · p. 28

Repair outcomes

• 21/26 obligations are completed by Structured Repair, compared with 17/26 for Raw Diagnostics and 1/26 for Generic Retry, using 66 calls versus 71 and 95.The repair cohort overlaps the separately defined SMT-first Lean set on 11 obligations.Source: §E.4 · p. 28

Usage and repair time

• Structured Repair’s recorded token total is 4.9% below Generic Retry and 20.2% above Raw Diagnostics, while its mean timeout-charged repair time is the lowest.Usage receipts are available for 45/66 Structured Repair calls, 43/71 Raw Diagnostics calls, and 53/95 Generic Retry calls; token columns sum those receipts.Source: §E.4 · p. 28, Table 13 · p. 28

Repair cohort

• The 26-obligation cohort includes 15 dynamical decrease or inductiveness obligations, six positivity or quadratic bounds, and two radial-unboundedness obligations.It also includes one each for equilibrium, unsafe separation, and set containment.Source: §E.4 · p. 28

E.5 ANALYSIS OF UNRESOLVED SYSTEMS

• 24 systems remain unresolved in the Full experiment: six produce no parsed candidate and 18 enter Lean verification.Table 14 groups their last recorded events to identify stages where additional candidate or proof work can extend coverage.Source: §E.5 · p. 29, Table 14 · p. 29
• Three runs also contain a replay-confirmed violation on another obligation, so last recorded events do not define mutually exclusive mathematical causes.The table identifies the final recorded execution stage.Source: §E.5 · p. 29

Curation rules

• Candidate records are curated by merging duplicates and configurations, retaining family representatives, removing structural redundancy, and excluding out-of-scope models.Instances are identified by intrinsic plant dynamics and control specifications; solver settings, neural architectures, and scaled domains are consolidated under corresponding systems.Source: §F.1 · p. 29

Curation results

• 233 candidate records are reduced to 80 Literature-derived instances after 153 exclusions: 24 duplicates, 23 alternative configurations, 44 family variants, 54 structurally simplified systems, and eight out-of-scope entries.The retained 80 comprise 47 from source papers, one from a textbook, and 32 from BarrierBench.Source: §F.1 · p. 29, Table 15 · p. 30, Table 16 · p. 30

High-dimensional scarcity

• Only 7 of 29 nominally high-dimensional candidate records (n ≥5) survive curation, highlighting the scarcity of genuinely high-dimensional systems in the literature.The nine high-dimensional records from Liu et al. (2024) collapse to one canonical system, while nine BarrierBench instances are excluded for structural simplification.Source: §F.1 · p. 29

Motivation for dataset extension

• The benchmark adds 11 Extended instances and 14 New systems with coupled, non-polynomial dynamics in five to ten dimensions to the 80-system core.Extended cases change state dimension, verification domains, or control constraints.Source: §F.1 · p. 30

High-dimensional benchmark growth

• 25 benchmark instances have n ≥5, up from 7; their share rises from 8.75% of the Literature-derived tier to 23.81% of the full benchmark.The Extended and New tiers contribute four and fourteen high-dimensional instances, respectively, for a 15.06 percentage-point increase in share.Source: §F.1 · p. 30

F.2 EXPERIMENTS DETAILS FOR MAIN TEXT

• Baseline methods use distinct numerical semantics, and inconclusive solver outcomes are not counted as verification.FOSSIL uses dReal at δF = 10^-5; the RL method checks its obligations only outside BϵR(0); and SynNLF uses a floating-point SOS/LMI check through MOSEK. Method-specific precision, domain exclusions, and tolerances are not transferred to SMT+Lean verification.Source: §F.2 · pp. 30–31

F.3 PROBLEM 1 : STABILITY CERTIFICATION

• Stability cases span two- to nine-dimensional systems, with targets ranging from local asymptotic stability to global asymptotic stability.For the listed local cases, the evaluation often removes the original puncture around the equilibrium from N; examples include nonpolynomial and polynomial systems and higher-dimensional systems from prior work.Source: §F.3 · pp. 31, 32, 35, 36

F.4 PROBLEM 2 : REGION-OF-ATTRACTION VERIFICATION

• ROA cases include circular and box-shaped target sets, with evaluation covering both ROA verification and an analytically constructed ROA.Examples retain the listed target set while changing an original ϵ-ROA target to ROA verification, and include a system whose original paper used an analytical Zubov construction.Source: §F.4 · pp. 37–38
• The region-of-attraction instances include a 10-dimensional system and a scalar system whose target is broadened from an original ϵ-ROA to the full region |x|≤1.The 10-dimensional instance retains the original domain [−1, 1]10; both instances are identified as ROA verification tasks.Source: §F.4 · p. 38

F.5 PROBLEM 3 :FORWARD-INVARIANT SET SYNTHESIS

• The forward-invariance instances include a sampled, controlled six-state PVTOL model and nonlinear systems in two and four dimensions with specified safe sets and unsafe regions.The listed examples also include discrete-time transitions and a four-dimensional closed-loop system.Source: §F.5 · p. 39

F.6 PROBLEM 4 :SAFETY VERIFICATION

• The safety instances span two- to eight-dimensional systems, including bounded domains and unbounded-domain barrier-verification tasks.Examples include a bounded two-dimensional case, an eight-dimensional case, and unbounded-domain cases.Source: §F.6 · pp. 41–42
• Systems 71–80 are designated barrier/safety verification tasks, with listed state spaces including R2, R3, and R4.Source: §F.6 · pp. 48–49
• Initial and unsafe sets are specified as boxes or norm-ball regions, including separated regions in state spaces from R2 to R4.Source: §F.6 · pp. 48–50
• The listed dynamics include continuous vector fields and discrete update maps with nonlinear terms such as sine, cosine, tanh, and exponential expressions.Source: §F.6 · pp. 49–50

F.7 EXTENDED TIER: SCALED AND PERTURBED VARIANTS OF RETAINED SYSTEMS

• The extended tier strengthens stability objectives, adds control constraints, scales systems to higher dimensions, and introduces parameter variations.Examples include changing local asymptotic stability to global asymptotic or exponential stability and imposing bounded control inputs.Source: §F.7 · pp. 50–52
• Safety is verified uniformly for every time-invariant ω in [0.5, 2] using a single barrier function that depends only on x.The barrier conditions must hold across the full admissible parameter range.Source: §F.7 · p. 54

F.8 NEWLY DESIGNED CHALLENGE INSTANCES

• New challenge instances address limited literature coverage of non-polynomial and high-dimensional systems, including 7D trigonometric-rational systems and a 10D cyclic rational system.The listed tasks include global exponential stability, ROA, and ROA verification.Source: §F.8 · pp. 54–55
• The new suite also includes controlled forward-invariance synthesis and discrete-time network invariance challenges.Examples include cascade systems, six-node opinion dynamics, and a 10D controlled Hopfield network.Source: §F.8 · pp. 56–58

• System 103 is labeled a 6D arctan-chain safety system with a discrete-time state update.Source: §F.8 · pp. 58–59
• System 104 is an 8D parametric nonlinear robust-safety task with a state-only barrier certificate required to hold uniformly for each fixed ω in [0.5, 2].The passage describes ω as a fixed uncertain parameter.Source: §F.8 · p. 59
• System 105 is labeled a 5D arctangent perturbation safety system.Source: §F.8 · p. 59