formal verification teams

Abstract: We look at a two-variable logic over finite graphs that allows Presburger quantifiers: linear arithmetic inequalities between the number of elements that satisfy subformulas. The prior literature shows that closing two-variable logic under Presburger quantification leads to undecidability, while closing under \emph{local quantification} -- the counts are always over neighbors of a given node -- preserves decidability. Here we show decidability of satisfiability for an intermediate logic that allows both local counts and global counts, but where the linear constraints do not mix the two. The proof requires a significant extension of the prior machinery developed for two-variable logic with counting. As a corollary we obtain decidability of satisfiability for an important family of Graph Neural Networks (GNNs). GNNs are a popular graph learning formalism. For example, in a variation of GNNs considered in the past literature, local aggregation is used in each layer to create modified values at each vertex of a graph, and then global aggregation is used in a final layer to obtain a single numerical value for the graph as a whole. Our logic is motivated by the fact that mixing of local counting and global aggregation in GNNs has been shown to lead to undecidability. Our results here show that if global and local aggregation are separated, one regains decidability. Decidability of other static analysis problems, like equivalence of GNNs, follows from the decidability of satisfiability.

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.

Abstract: A semilinear set is stratifiable if it is a finite union of linear sets whose periods have at most two nonzero coordinates, with no two periods in one component connecting alternating pairs of coordinates. We give a computable many-one reduction from the existence of a rational zero of an integer polynomial to deciding stratifiability. After the classical reduction to quadratic systems, we reduce rational solvability of these systems to a problem we call finite separation by Cartesian products of rational linear forms. Its input consists of rational subspaces $D_1,\ldots,D_k\le\mathbb Q^r\times\mathbb Q^r$. A separator is a map $(\boldsymbol x,\boldsymbol y)\mapsto(u(\boldsymbol x),v(\boldsymbol y))$, where $u,v\colon\mathbb Q^r\to\mathbb Q$ are nonzero rational linear forms. The problem asks whether finitely many separators suffice so that every pair outside $\bigcup_iD_i$ receives, from some separator, a value attained at no pair in that union. We then reduce this problem to stratifiability. Ginsburg and Spanier's characterization of letter-bounded context-free languages} also induces a reduction from rational polynomial solvability to context-freeness of letter-bounded languages specified by semilinear exponent sets. An OpenAI preprint claims undecidability of rational polynomial solvability; if correct, our result settles the decidability of general stratifiability, a problem open since 1966.

Abstract: Temporal hyperlogics combine explicit quantification over traces with temporal requirements evaluated over the quantified traces. HyperRecHML is a temporal hyperlogic which allows for arbitrary mixing of trace quantification and the use of fixed points for expressing temporal requirements, which makes it very expressive in comparison to other first-order hyperlogics. HyperRecHML has already been successfully applied in runtime verification, but the decidability of its model checking problem remains open. We answer this question positively by providing two main contributions. Firstly, a normalization procedure that allows to reduce arbitrary HyperRecHML formulas to a normal form with restricted nesting of trace quantification and fixed points. Secondly, we provide an automata-based model checking algorithm for formulas of this normal form. The complexity of our algorithm is comparable to similar ones for other hyperlogics, despite the extra expressive power.

Abstract: Let $V_i(n)$ denote the minimum worst-case number of comparisons needed to find the $i$-th smallest of $n$ distinct elements. We construct algorithms showing $V_7(16)\le28$ and $V_8(16)\le29$, improving the previously reported upper bounds of 30 and 31. Together with known lower bounds, these results establish $V_7(16)=28$ and leave $V_8(16)\in\{28,29\}$. For 17 elements, we establish $V_5(17)=27$ and improve the upper bounds for ranks 6 through 9 to 29, 30, 31, and 31, respectively. Every new upper bound has an explicit decision-graph certificate verified by a static checker developed independently of the search. We also derive a lower bound for selection from a partially ordered state by combining the Fussenegger-Gabow weight with its order-reversed counterpart. All new upper bounds and this lower bound are formally verified in Lean 4. For $V_8(16)$, we show that a lower bound based solely on the total number of decision-tree leaves cannot establish $V_8(16)\ge29$. The algorithms were found using fixed-budget search, information-guided comparison ordering, and proof-number search. Proof-number search was decisive in finding the 28-comparison algorithm; in our experiments, refuting a comparison budget remained substantially more expensive than finding an algorithm within it.

Abstract: Fine-tuned Large Language Models (LLMs) significantly advance Automated Theorem Proving (ATP), but are often deployed as guiding policies within tree search rather than for single-attempt generation. Recent work shows cross entropy is suboptimal for an LLM used in flat search strategies such as aggregation or filtering and that work has developed new loss functions to correct this misalignment. Extending this alignment to tree search is more challenging: proof discovery depends on exploration and recovery through off-trace states that supervised demonstrations do not reveal. We extend Compute-Aligned Training (CAT) to this setting through an abstraction of policy-guided search, deriving tractable, trace-supported losses. Alongside these search-aware losses, we introduce a search-agnostic uniform-allocation (UA) loss that accounts for the budget without specifying the specific search. Both induce scalar weights on per-tactic cross-entropy gradients. We characterize how off-trace behavior affects the search-aware weights, including conditions for vanishing approximation error at large budgets. On a Lean benchmark, both approaches achieve higher observed proof-success rates than cross-entropy across six search strategies, with strong results from a single shared UA adapter. Budget sweeps show larger gains over cross-entropy at 16 than at 256 expansions, implying CAT scales with test time compute.

Abstract: Recurrent GNNs iterate message passing to convergence, and their logical characterizations to date rely on multi-set aggregation, graded (counting) logics, and halting or acceptance conditions that cannot be verified from the network's parameters. We study recurrent GNNs with set-based aggregation and identify sufficient conditions checkable from the weights for networks to compile into formulas and formulas into networks. The main result is an effective, two-directional equivalence between a class of networks and the Boolean closure of reachability and safety properties, the fragment B$Σ^{\circ}_1$ of the modal $μ$-calculus. The fragment is not an artifact: it is the exact expressive level of stabilization over finite vocabulary, which supports fixed points of a single polarity and Boolean combinations thereof, but not the composition of fixed points of opposite polarities. The correspondence needs no counting logic, no external halting signal, and no non-effective acceptance condition, yielding a verifiable path from weights to symbolic explanations for networks meeting the conditions.