Let a Neural Network be Your Invariant
Authors: Mirco Giacobbe
Daniel Kroening
Abhinandan Pal
Michael Tautschnig
Venue: NeurIPS 2025 poster ()
Keywords: Neural Model Checking
Inductive Invariants
Safety Verification
Primary area: machine_learning_for_sciences

Abstract: Safety verification ensures that a system avoids undesired behaviour. 
Liveness complements safety, ensuring that the system also achieves its
desired objectives.  A complete specification of functional correctness must
combine both safety and liveness.  Proving with mathematical
certainty that a system satisfies a safety property demands presenting an
appropriate inductive invariant of the system, whereas proving liveness
requires showing a measure of progress witnessed by a ranking function. 
Neural model checking has recently introduced a data-driven approach to the
formal verification of reactive systems, albeit focusing on ranking
functions and thus addressing liveness properties only.  In this paper, we
extend and generalise neural model checking to additionally encompass
inductive invariants and thus safety properties as well.  Given a system and
a linear temporal logic specification of safety and liveness, our approach
alternates a learning and a checking component towards the construction of a
provably sound neural certificate.  Our new method introduces a neural
certificate architecture that jointly represents inductive invariants as
proofs of safety, and ranking functions as proofs of liveness.  Moreover,
our new architecture is amenable to training using constraint solvers,
accelerating prior neural model checking work otherwise based on gradient
descent. We experimentally demonstrate that our method is orders of
magnitude faster than the state-of-the-art model checkers on pure liveness
and combined safety and liveness verification tasks written in
SystemVerilog, while enabling the verification of richer properties than was
previously possible for neural model checking.

Let a Neural Network Be Your Invariant
Mirco Giacobbe" University of Birmingham, UK Zeroth Research, UK
Daniel Kroening" Amazon Web Services, USA
Abhinandan Pal"
Michael Tautschnig"
University of Birmingham, UK National Institute of Informatics Tokyo, Japan
Amazon Web Services, USA Queen Mary University of London, UK
Abstract
Safety verification ensures that a system avoids undesired behaviour. Liveness complements safety, ensuring that the system also achieves its desired objectives. A complete specification of functional correctness must combine both safety and liveness. Proving with mathematical certainty that system satisfies a safety property demands presenting an appropriate inductive invariant of the system, whereas proving liveness requires showing measure of progress witnessed by a ranking function. Neural model checking has recently introduced data-driven approach to the formal verification of reactive systems, albeit focusing ranking functions and thus addressing liveness properties only. In this paper, we extend and generalise neural model checking to additionally encompass inductive invariants and thus safety properties as well. Given a system and a linear temporal logic specification of safety and liveness, our approach alternates learning and a checking component towards the construction of a provably sound neural certificate. Our method introduces neural certificate architecture that jointly represents inductive invariants as proofss of safety, and ranking functions as proofs of liveness. Moreover,
architecture amenable training using constraint solvers, accelerating prior neural model checking work otherwise based on gradient descent. We experimentally demonstrate that method is orders of magnitude faster than the state-of-the-art model checkers on pure liveness and combined safety and liveness verification tasks written in System Verilog, while enabling the verification of richer properties than was previously possible for neural model checking.
1 Introduction
Model checking addresses the question of whether reactive system M meets specification of intended behaviour & [42]. Reactive systems are systems that continually respond to inputs and operate over infinite executions. Exemplars include hardware designs implementing processing units, communication and arbitration protocols, as well as digital controllers for automotive, aerospace, medical applications, where safety is paramount. Safety properties require that nothing bad ever happens. A safety violation is finite execution the last state of which falsifies and the damage is irredeemable [77]. Safety properties are dual to liveness properties, which require that something good eventually happens. liveness violation is evidenced by an infinite execution that falsifies 4 any finite violating prefix could in principle still be extended to compliant execution (77). Every linear-time specification is the composition of safety and a liveness property [ and linear temporal logic (LTL) provides an expressive language for specifying linear-time properties of reactive systems.
'The authors are listed alphabetically.
39th Conference on Neural Information Processing Systems (NcurIPS 2025).

---

System Verilog Assertions (SVA) bring linear- time logic into commercial hardware design flows [56] and electronic design automation vendors have spent decades optimising symbolic model checkers for them. Testing and simulation alone cannot fully guarantee that system meets its specifications, and explicitly enumerating every possible behaviour is impractical, except for the most trivial hardware designs. Symbolic model checking has made it feasible to handle large state spaces. Two symbolic paradigms dominate. Algorithms based on binary decision diagrams (BDDs) provide sound and complete procedures for LTL model checking, yet BDDs often explode in size when faced with arithmetic data paths ubiquitous in modern hardware design 226 [2]. Bounded model checking (BMC) algorithms enjoy the much more scalable combinatorial and arithmetic reasoning of SAT solvers, but only explore the state space up to a finite depth, sacrificing completeness over unbounded execution [77. Incremental algorithms for the construction of exploration frontiers (IC3) bridge that gap in unbounded safety verification (20), but fall short on liveness.
Neural model checking is an automated approach that leverages neural certificates to verify reactive systems against LTT. specifications, but prior work has exclusively focused on liveness properties (3] This prior cognate work learns ranking functions represented neural networks-whie serve as proof of liveness-from random executions and then checks their validity using symbolic reasoning. thereby providing formal guarantees. However, specifications that characterise pure safety or combi- nations of safety and liveness additionally demand the construction of inductive invariants -wichh serve proofs of safety. Prior work does not construct such invariants, leaving safety out of reach.
In this paper, we demonstrate that neural networks are an effective representation for inductive invariants as well. Our novel method leverages neural certificates to simultaneously represent ranking functions and inductive invariants. Given a hardware design MM and non-deterministic Büchi automaton A + that recognises the violations to an LTL formula o we train a neural certificate on sample transitions of the synchronous composition M || A-s. This network (i) classifies each state as inside or outside the invariant and (ii) ranks the states, within the invariant, to strictly decrease whenever an accepting state is encountered. We then pose a one-step BMC query to check the neural certificate is true over the entire state space. On affirmation, this proves every accepting state is either (i) unreachable or (ii) visited at most finitely many times. This implies that no reachable behaviour of M satisfies - thereby proving that every reachable behaviour of M satisfies 4
We implemented our method using a new neural ranking function architecture that enables training using constraint solvers, in contrast to prior work that exclusively relies on gradient descent for training 633 Our new architecture yields more compact representations and it is much more efficient and numerically stable than prior work. We extended the prior benchmark with standard safety and combined liveness and safety verification problems, and have compared our method with the state-of-the-arr hardware model checkers. Measuring against the per-task fastest pure-liveness, our method is faster on 66 % of tasks, 10x faster on 46 %, 10 x on 11 %, and 10 x on 4 %. On pure safety tasks, while not outperforming, for all approaches in under 1s. The picture changes dramatically for properties that demand both an inductive invariant and ranking function: method is faster than the leading model checkers on 61 % of tasks, running 102x x on 43 %, 10 x on 27 %, and 10 x on 6 %.
match the best symbolic tools: 80 % of instances complete
Our contribution is threefold. First, by simultaneously representing inductive invariants and ranking functions using neural networks, we extend and generalise neural model checking to verify arbitrary LTL properties encompassing both safety and liveness. Second, by introducing a neural architecture amenable to training using constraint solvers, we achieve both superior runtime efficiency and numer- ical stability. Third, by evaluating our method across a 634-task benchmark suite, we demonstrate that our method outperforms the state of the art in automated formal verification.
2 Model Checking Safety and Liveness
We consider specifications tb in LTL over a set of atomic propositions II. LTL extends propositional logic with temporal operators: X t meaning & holds at the next step, 4 meaning & eventually holds,
G ④ meaning & always holds, Φ2 U Φ. meaning Φ holds at all times until Φb necessarily holds at some future step, and +, W $ meaning o holds at all time before 2 possibly occurs [102.. LTL naturally expresses safety, liveness, and their combinations for reactive systems. For II = (a. the formula G a is a safety property: a single finite prefix whose last state violates a refutes it. By contrast. F b is liveness property: no finite execution suffices to disprove it, since b may still
2

---

occur later. The formula a b combines both: its safety component forbids any prefix containing -a/- before the first b, while its liveness component requires that b eventually occurs. Equivalently a Uu = a Wb A F b, where a Wb is pure safety and F b is pure liveness.
We model reactive system M over finite variable set XM initial condition M and a sequential update relation Update The variables are split into inputs inp XM and state-holding registers reg X.. Init is first-order predicate over reg X.M and Update. .MM is a first-order predicate over XM rrgg X/M. where the set of primed variables denotes the next-cycle values. reactive system M induces transition system with state space S of valuations of XM, initial states So S S with E Su - Init, (reg 8), and transition relation reg -MMS S X S with s -M s' - Update (s. s'). The executions of M are the infinite sequences (so. $1, ... where E So and 8; - 8,+1 for all i E N.
state transition system by an
We cast our model checking question a language inclusion question. Given a system M, define as obs XM S XM its set of observables, and in turn define the language LM of M as the set of sequences (obs so; obs 81... s1...) --...ch we call the traces of M-induced by the executions (80, 81 ...) of .M. Given an LTL formula & over atomic propositions 11 and the alphabet Σ = 2l1 of valuations of II, we define the language La S Σ" of & as the set of all possible traces (ou, o1...) E E" satisfying Q. Provided that II = obs X XM (which we require to be Boolean), the model checking question asks whether LM S Lg. i.e., all traces of M satisfy 4. This is equivalent to the language emptiness question LM n -- = 0, i.e., no trace of .M violates & [[] 42
As is standard in nutomata-theoretio verification, we reduce the language emptiness question an equivalent fair emptiness question. A non-deterministic Büchi automaton A consists of a finite set of states Q, an initial state Qo Q, imput alphabet Σ, transition relation 5 C Q E x Q, and set of fair states F C QQU 88 39 [25]. This can be viewed as reactive system with single variable XA {q} 8. We define the fair language L', of A as the set of traces of A whose respective executions visit F infinitely often. We rely on the fact that every LTL formula &b admits a non-eeteriinistic Büchi automaton Ag for which A, T.p. Our reduction to fair emptiness thus constructs an automaton A and forms the synchronous product M || A . between M and A - with the fair states defined S F. We refer the reader to the literature for full formal definition of the synchronous product ( 11 42];
over Q, where (q) - q = qo and Update ( 9,44) > (g,
; the key property to note is that M'MIIA_ LM n L' Hence, our language emptiness question and, in turn, our model checking question amount to deciding the fair emptiness question L'MIA = 0.
We answer the fair emptiness question by presenting a certificate consisting of two components: (i) an inductive invariant defined as a set 7 reg S x Q that captures (or over-approximates) the reachable states of M || A .. and (ii) a ranking function V I - W over a well-founded relation (W. <) that assigns ranks all states within the invariant that prove that all reachable executions visit fair states at most finitely many times. Concretely, for all s, s E S and q, g' EQ.
8 LE So
(reg 8, .9) E 1,
(I)
g) + MMIAA (8', (') A (reg 8, g) E
(reg 8',9¹) I,
(2)
(8. MI (s', d') A (reg 8, q) E
V (ree 8,4) 2 V (reg s', ,',"),,
(3)
(8,9) + MIIA... (s', d') A (reg q) E 1 A FEF = V V(reg 8, q) > V Vireg s .'.g").
(4)
Clauses 1 and 2 state that initial states lie in I and that / is closed under transitions, so / forms an over-approo averrapproximation of the set of reachable states. Clauses ( and 4 require that, along every transition whose source is in I, the rank V/ never increases, and it decreases strictly whenever the source state fair (q E F). Because (W. <) well founded, only finitely many strict decreases are possible; hence, fair states must be visited at most finitely many times. This implies that all executions are unfair, i.e., I A = 0. which is equivalent to saying all traces of M satisfy [15).
Figure Sooureeiiinn Iillstrrate our workflow on an example. Figure T gives SystemVerilog module M that satisfies the LTL property T- = U b. Figure Dp gives a Büchi automaton A. recognising - Figure D depicts the state space of the synchronous product M || A-4b product states are arranged on two-dimensional grid, each state corresponding to the pair of a state s; of M (where i is the value of the register c) and a state qn. qt. or 92 of A-a. The sole initial state is (80, qn), and the dotted region indicates the inductive invariant T. Each state in / indicates in its upper-right corner the respective rank, taken from N. Along each transition in J, the rank strictly decreases when leaving a fair state and never increases otherwise, ensuring that the sole fair cycle within I terminates. Notably,
3

---

Σ
nodule NODEL (input elx, output reg b);
reg [s:0] c D;
A-o
assign (c 60);
assign (c 60);
alvays @(posedge elx) begin
(ae ab]
q1
<= 1;
end
(a6)
Phi: assert property
(ab)
qo
Q2
(S(paedgge clk) a_until b);
enduodule
Phi = (aUb)
(a)
(b)
42
aB
a6
a5
25
S6
60
0
80
82
861
862
863
(c)
Figure I: Model checking safety and liveness on an illustrative example
the system has a non-terminating fair cycle (e.g.. the cycle on q2), but this is unreachable and excluded by I. In general, invariants may include unreachable states, provided none can lead to fair cycle.
3 Neural Partially-Ranking Functions
We reduce the fair emptiness problem to a machine learning task by (i) modelling the invariant I classifier over-approximating the reachable states, and (ii) modelling the ranking function V as a regressor. In this section, we present our learn-check workflow which, upon termination of our procedure, formally ensures that these two components jointly satisfy conditions Crucially, we introduce the neural partially-raking function, which combines the definition of inductive invariant and ranking function into single neural network.
4 -
We define a neural partially-rankinng function over discrete parameter space O the function
V reg S x -
(5)
Our objective is to learn upper bound Z and of parameters (0g +) such that for all 8, s E S and q. of E Q, the following two conditions hold:
E Su
(regss; Ogo):
(6)
(s.9) MMIAAS
ARA Vreg s; s;
V(ro s; f2y) (roggs';8p) + 1r()). (7)
where 1 r if E F else O. The trainable network parameters are in O and are distinct for each automaton state q E Q, while a is global. The initiation condition of Eq. (6) ensures that all initial states receive rank bounded above by K. The ranking condition of Eq. ( ensures that states bounded above by x are inductively assigned a rank. Ultimately, a solution is and {0,) induces an invariant / and ranking function V satisfying the clauses (4), respectively defined as follows:
I (reg s. 9) 2 (rogss; 0,))
V s, q) V (reg s; 0,)) if (rog s. E I.
(8)
Since the hardware state space S and Q are finite, the image V = (V s; 0,): : s E S.4 E Q) of V for a constant parameter [0,) finite well, having least element under the strict inequality over the integers. This makes (W, <) well founded, having infinite descending chain.
We train V in counterexample-guides inductive synthesis loop as illustrated in Figure Our procedure incrementally constructs two datasets Dinit and D train V to respectively satisfy

---

Dinit 1
(ri, :
Dirans f- 1
F
Candidate V. 10.1
Linear Sign
Learn
Linear + Sign
Lincau
Linear
Linear
Linear Step
Dinit t Dini U Cinit
Check
Derans f- Dorns U Crrans
o1. 02:
(A1.
1m))
Valid!
(rr
(a)
(b)
Figure 2: Our learn-check workflow (a) and architecture for neural partially-ranking functions (b)
conditions (6) and 77) The dataset Dinit contains sample initial register values reg 8 of M where E So. and the dataset Draans contains sample transitions M A- in the form of quadruples (reg reg s', q') where (s, q) MiIAA (s', q'). Initially, we assume that Dinit and Dtrans are empty. Our learning component computes a set of parameters (0, hee to hold over the set of samples Dinit and Derans- Our checking component formally verifies whether conditions (6) and ( hold over the entire state space. If the checker confirms the conditions, then the procedure halts successfully. In the converse case, it provides sets of counterexamples Cinit and Cirans which are respectively added to Dinit and Dtrans, and learning and checking are repeated in loop.
Learning Our learning phase computes set of parameters for which our initiation and ranking conditions are valid across all samples in the dataset. More precisely, enforcing our initiation condition amounts satisfying the following constraint:
LearnInit(O,.o x) A (r;
rEDia
Similarly, satisfying ranking condition amounts to satisfying the following constraint:
LearnRank((, x.) A ((::g) = (rr: 0g) ((r:044) 1r(g))
(10)
(r.q.r'.q')El Duars
Overall, our learning phase is tasked to solve the following question which, we show in Section we cast to a constraint satisfaction problem:
30, k: Learnlnit(O, A LearnRank(O, k)
(11)
If valid set of parameters exists, then this is passed to the checking phase. If valid set of parameters does not exist, this indicates a larger network is needed or no solution exists at all. this case, our strategy is to progressively add hidden layer widen it and retry until preset limit.
Checking Our checking phase determines the presence or the absence of counterexamples to initiation and ranking conditions for the candidate parameters (04. More preciscly, counterexample for the initiation condition must satisfy the following constraint:
Checklnit(s) = Init (s, 4o) A K < V (reg s; 0g
(12)
Similarly, counterexample for the ranking condition must satisfy the following constraint:
CheckRank(s, q, o Update qs,
k 2 Vrrg s; 6,)) A Vreg s; 0.)) < V(rr' + +r(())
(13)
Overall, our checking phase asks whether the following statement holds:
3s: CheckInit(s)
3s,gr' r'. Check q.7
(14)
We check the initialisation and ranking conditions independently. If both queries are unsatisfiable. then conclude that V is valid neural partiall function. If either or both satisfiable.
5

---

then the respective assignments constitute counterexamples. To produce multiple counterexamples Cinit or Cerans in each iteration, we check (T3) over explicitly enumerated automaton pairs (q. q') independently. This accelerates convergence, and gives equal emphasis to each transition of .....
Our counterexample-guide inductive synthesis procedure captures task-specific edge cases that yield succinct datasets. This is in contrast to prior work that benefits from random initialisation of the datasets before the first iteration [63]. Moreover, as we show in Section 4 we further optimise our procedure by proposing a specialised architecture that is amenable not only to checking but also to learning using efficient and numerically stable constraint satisfaction solvers.
4 Learning Neural Partially-Ranking Functions Using MILP Solvers
We present a specialised architecture for neural partially-ranking functions amenable to training using constraint satisfaction solvers. Our architecture is illustrated in Figure Given a vector of word-level register values r = (ri,...,Tw) Tw) with n = reg XM). our architecture feeds r into two branches. The left component a (m4)) consists of T. fully connected layers (W((), .14)) ..... wL" o(9) with .. N neurons, respectively, sign activation functions on the hidden layers, and step function on the output layer featuring = Nr neurons. The right component consists of m linear functions with n inputs each: g(r-)) = A r + c(a), The left component a acts as mask that selects or excludes the linear functions of the right component f3; in other words, V(r, 02)) = (14)) 3(ra))
I1 requires encoding. We build upon the result for which feed-forward neural networks with sign activation functions are amenable to training with mixed-integer linear programming (MILP) solvers [67[2]] [21]. Henceforth, we use i.j to index individual elements of linear components, specifically i for the inputs elements and for output elements, and we use to index layers of the network. single hyperparameter P E Noo bounds the magnitude of all decision variables in the encoding. Decision variables shared across multiple (q) b(9)) (g) (9)
Every application of arguments (r, 0g) to V in Eqs. (
occurrences of and associated to a common q are denoted as w
Oij C [-P, to
respectively refer to the elements of W/(9), (/9)) AA()) and c(9); the threshold x E [-P, P] is also a common decision variable in the learning phase. Decision variables associated to specific occurrences of r and q are d (r.4) E {0, 1} to indicate the activation status of the corresponding neurons, = to
represent neuron-weight products where (r.4) E [M PM,] with M, = max(/ri],... (xx)) (r-q)
-ilj and Zitj E [-P,, P] with 2 2, and finally vj (r-g) E [M, P.M,] to represent the overall output of the network. First, we encode the relationship between z, r and w at layer 1 as
(r.g) = r
(15)
$11
Then, for 1,..., L, we encode the relationship between u, z and b layer / (where e 0) as (r-g) =
= =1 For I 2....,, L. we encode the relationship between u at layer I 1 and 2 and w layer I as
(us)
brj + EieN, 30j
(r
2) (ufp
= brj + EieN. (r,9)
Fitj S <( (16)
(=i)) it
(r.q) (4)
+ 2P
u (t-1); S 2P) A (z + w (g) 2P (1-1)) 50) A (r:g)
(r.q)
(r.q)
(17)
(Z16)
(r-9) - w()
(q) - 2P (r
(t- 2 -2P) A (Z48) + wij
(g)
+ 2P (r.g) (f-1)) 2 0)
which represents Zitj
(r = waj if u ((-1)) = 1, and Fifj
(r.4)
(r.4) Wity otherwise. Finally, we encode
the relationship between v. a, and u at layer L
(u(t))) (r.4) 1 1j
(r.4)
c
(4)
Eien rea (g)) (u
(r.g) - of ((9))) = 0)
(18)
As result, each occurrence of V(r, 0g) in Eqs.
corresponds the linear term Eiem U.
(r.9)
Notably, a naive encoding that represents (r:4) as a product between a neuron variable and w would induce bilinear constraints; our encoding avoids this and produces an equivalent encoding with linear constraints only. This enables using efficient MILP (and SMT) solvers in the learning phase.
Essentially, our architecture represents a piecewise function with 2 configurations, given by a e {0. 1) 1)m). each of which induces a specific summation of linear functions, given by 3 E 2m in the spirit of piecewise- decision variables to the integer type, which results in neural networks that naturally quantised.
ranking functions (76] 123 124 In our implementation, we restrict all

---

Table 1: Tasks completed per tool, per design; in bold the max per design, per spec-type
LS
LCD
Tmop
12cS
7-Seg
PWM
VGA
UARTI
Delay
Gray
Blink
Total
Pure Safety
Tasks
16
28
17
20
13
12
20
10
32
11
25
206
Dur
16
28
17
4
15
12
20
10
32
11
25
190
ABC
16
28
17
15
12
10
11
25
206
nuXmv
16
28
17
20
15
12
20
10
32
11
25
206
rIC3
16
28
17
20
15
2
20
10
32
11
25
196
Pure Liveness
Tasks
16
14
17
20
30
12
10
10
32
33
25
219
Our
14
17
20
30
12
10
33
14
192
ABC
3
5
9
4
10
3
5
10
8
16
78
nuXmv
12
13
17
16
28
4
10
32
33
180
rIC3
13
7
17
6
10
19
110
NNC 24
15
3
10
20
30
10
9
10
32
33
172
Safety + Liveness
Tasks
32
14
17
20
15
12
10
10
32
22
25
209
Dur
32
14
17
3
12
10
10
32
22
11
172
ABC
12
11
20
6
11
nuXmv
11
12
14
16
15
6
10
10
26
14
20
154
rIC3
12
14
14
20
8
4
10
9
18
14
6
129
Experimental Evaluation
Implementation We implemented prototype using modular Python 3.12 pipeline Given an LTL formula 4, we obtained A- with Spot 2.11.6 [51], converted SystemVeriloog to bit- vector SMT using EBMC 5.6 [91]. performed validity queries and computed counterexamples us- ing Bitwuzla 0.7.0 [96). and trained a neural partially-ranking function using the MILP solver Gurobi 12.0.1 [65 Our method relies on single global hyperparameter configuration, be- sides the integer bound P (see Section 4). We chose P from a finite set of configurations (1,5, 10, [M/10], [M/2], , M, M+ 2M where M is the largest value any register can take in the hardware design; this renders the bounds for 21, and Vj quadratic in M except when P = 1, or 10. We configured the architecture to start with linear model (per g E A-a)) and add one hidden layer with a single neuron (left branch of Figure 2h) upon the first failure of the learning phase, subsequently increasing its width by one neuron upon subsequent failures, up to 5 attempts.
Experimental Setup Building on the ten parameterised System Verilog designs and 194 pure- liveness tasks of prior work (63]. we add eleventh design and, for all eleven, contribute additional pure-safety and combined safety-liveness specifications on each task, yielding a 634-task suite that retains the original diversity (Appendix (A). We compared against (i) the gradient-based neural model checking approach, labelled 2MC² 24 (liveness only) [63] and (ii) the winners of recent HWMCC editions [ nuXmv 2.1.0 (28). rIC3 1.5.1 [119], and ABC/Super-Pree
24 For nuXmv we translated each design with its assertions to SMV using EBMC; then, we converted SMV to AIG for ABC and rIC3 with AIGER 18 yielding fully automated flow. All experiments ran on an AWS m6a.4xlarge instance (16 vCPUs, 64 GB RAM, Ubuntu 24.04). Each task had a 5 h timeout per tool; aggregate, the experiments consumed 9083 (=:378 d) of compute time.
Overall Efficacy Table I presents all solved instances by property class. For pure-safety
historically emphasised in HWMCC [6 107 symbolic tools clear 2 95 % of tasks, and we remain close to decades-matun tools at 92 %. For pure-liveness, performance spreads: nuXmv 82 %. ABC 36 %, rIC3 %, 24 %, while we complete 88 %. On sufety-plus-livene properties, the gap widens, nuXmv solves 74 %, ABC 46 %, rIC3 61 %, and our approach reaches 82 %.
Comparison on Pure Safety We generally perform on par with leading symbolic checkers with decades of optimisation, as Figure indicates, while being faster than NuXmv on 17 %, rIC3 on

---

nuXmv
rIC3
ABC
NMC
24
Dur
Time
02
Tusks complesed
Tasks complesed
Tisks completed
(a) Pure-Safety
(b) Livenesss
(c) Safety-Livenes
Cutaal Time
30m
10x
Suie space $i2e
1m
10ax
out Fimme
10aa
10*
100
.03
Abs
830 15 30 15 35 15s 3m Sin 20m 3h
Sn
Ii Sm 20m
is Ximih
Best of other tools time
Best of other tooks time
Best of other tools time
(d) Pure-Safety
(e) Liveness
(l) Safety- LiveneLs
Figure 3: Runtime comparison with the state of the art (all times are in log scale)
25 %, and ABC on 32 % of safety tasks. Figure Jd plots each individual task by time, with the per-task fastest symbolic solver on the z-axis and our method on the y-axis; point size and brightness reflect state-space size. While symbolic tools often lead on individual instances, in 80 % of tasks both finish within 1s, indicating that a our method can meaningfully match portfolio of symbolic safety checkers, besides being the first neural model checking framework to support general safety.
Comparison on Pure Liveness Figure 3p indicates that our method is consistently faster than the others. Within 1 s we solve 24 % more tasks than nuXmv, 59 % more tasks than rIC3, 59 % more than ABC, and 64 % more than 24; at min the margins widen to 31 %, 68 %. 76 %, 71 %. and they still measure 12 %. 45 %, 59 %, 13 % after 1 h. The percentage of tasks completed in 5 per task by nuXmv, NMC 24, rIC3, and ABC are completed in under 7s, s, 0.6 0.3 s by our method. Figure 31 shows the per-task runtime gains against the fastest competing method per task: our method is faster on 66 % of tasks, at least 10x faster on 46 %, 102 x faster on 29 %. 10 x faster on 11 %. 10 faster on 4 %. and 108 x faster on 1 % with respect to the whole state of the art. On a specific comparison with NMC 24 we obtain speedups of at least 10x on 88 %, 102x x on 79 %, 102x x on 45 %, 10 x on 18 %, and 10y x 5 %. Finally overall, 5 % of tasks timeout for all tools except ours.
Comparison on Combined Safety and Liveness Figure indicates that the performance gap between our method and the alternatives further widens safety-livenes, tasks. Within 1 approach completes 31 % more tasks than nuXmv, 34 % more than rIC3 and 36 % more than ABC; after 1 min the gaps grow 38 %, 43 %, 54 %, and persist 20 %. 31 %, 41 % after 1 h. Benchmarks that exhaust nuXmv, ABC or r rIC3 in h finish in 56 6s, 0.8 s per task with our approach. Figure 3 shows that we are faster on 61 %. 10x faster on 52 %, 10 faster on 43 %. 10 x faster on 36 % 10 x faster on 27 %, and 10 x faster on 6 % of the tasks; all tools, besides ours, hit the h timeout on 18 % of the task suite, bringing arbitrary LTL verification to runtime parity with pure-safety.
Neural Certificates Expressivity In Figure 4r, Auto is our default configuration that starts with linear for each state q of A and escalates to neural models only if linear is infeasible; Only Linear is the ablation that exity immediately when the linear model fails. The linear model completes 48 % of tasks within 9s per task and makes no progress thereafter; by contrast, our default finishes 87 % overall. Since the default always tries the linear model first, it never trails the ablation; when linear
8

---

Api2 MCt. Sdfazil
Qurchi 10c vMl
Line
MeriGIT
Time
A01
25%
43%
65%
10
Tasks complesed
Tasks complesed
Tasks complesed
(a) Linear Architecture Ablation
(b) Uniformly Random Samples (c) Other Learning Engines
Figure 4: Runtime analysis of our approach (all times are in log scale)
fails, automatic widening provides the expressivity needed to solve a lot more instances, showing that purely affine certificates are insufficient while our neural-certificate architecture succeeds.
Comparison with Random Dataset Generation Our iterative procedure presented in Figure 2 starts with empty datasets Dinit and Drans and populates them purely via counterexample-guieee procedure, which identifies edge-cases one by one towards the synthesis of neural partially-ranking functions. This contrast with the cognate neural model checking approach based on gradient descent, which benefits from random test generation to initially populate the datasets and rarely relies on the generation of data by means of counterexamples 63 Section 5]. Figure D evaluates our MILP-based approach under multiple random initialisation sizes with 0 (our default), 10, 25, and 50 randomly generated samples, respectively. As our experiment indicates, our default approach nearly indistinguishable from the Best curve (which indicates the fastest configuration per instance). This indicates that our MILP-based approach does not benefit from unguided random data generation.
Comparison with SMT Learning Engines Our new architecture makes learning amenable to MILP solving and, more generally, to decision procedures for linear theories implemented in SMT solvers. Figure 4 compares alternative engines for our learn phase, where replace the MILP solver Gurobi with the SMT solvers CVC5 1.1.2 [4], MathSAT 5.6.10 [36], and Z3 4. 4.10. [49] via PySMT [59]. Within the 5 h timeout, MathSAT completed 81 % of tasks, Gurobi completed 87 %, CVC5 completed 88 %, and Z3 completed 96 % of tasks. Gurobi and Z3 offer the best compromise between speed and efficacy, with Z3 demonstrating superior coverage and Gurobi shorter runtimes: Gurobi was on average 7x faster than 23 on successfully solved instances. However, Gurobi failed return result in 13 % of cases because of memory segmentation faults, model infeasibility for our hyper-parameters, numerical mismatches after evaluation the result with NumPy; only 2 tasks were timeouts. The Best curve selects the fastest engine per onstance-obviouslyy outperforming every other solver, providing a baseline for a potential portfolio implementation. We remark that all experiments besides this comparison (Figure 44) use only Gurobi its learning engine.
Strengths and Limitations Our approach is much more straightforward in terms of parameter tuning then the prior neural model checking approach [63]. owing to the theoretical completeness and the superior numerical stability of MILP and SMT algorithms over stochastic gradient descent. However, this strongly relies on sign-activated feed-forward neural networks; the generalisation to further architectures is an open problem for future investigation. Our method is amenable to training functions.
over parameters of integer type, which naturally results in quantised neural partially- On the other hand, our approach is limited to hardware and reactive systems without arrays or strings of parametric length, procedure calls or dynamic data structures, which are topics for future work.
Threats to Validity Our empirical evaluation has demonstrated the superior performance of our approach over the state of the art on verification tasks derived from standard textbook level hardware designs. Our benchmark suite encompasses word-level designs with safety and liveness properties, unlike the standard HWMCC'24 benchmarks which focus on pure safety properties [19]. Our benchmark is arguably the hardest (as of today) for word-level liveness and combined sifety-liveness hardware verification. Yet, our evaluation may not be representative verifications tasks other than suite and further research is required to assess the generalisability and the scalability of our approach to other workloads. Future work includes the integration of neural and compositional model checking towards the scalable formal verification of industrial-se scale designs 40 88 [34].

---

Related Work
Model Checking Linear Temporal Logic Formal hardware verification relies on model checking
LTL specifications coniffiiinncooiieddd
codified, c.g., as VerlemVerillog Assertions- guarantee safety and live-
ness properties 8 56
77
102 Symbolic engines based on BDD fixed-points [ 75 or
SAT/IC3 reasoning I7
87 [14] among other methods have evolved over fifty years, with key contributions to formal verification honoured by the ACM Turing Awards of 1996, 2007,
20
73
and 2013. The automata -ooomat-theoretic approaches to model checking often reduce model checking to fair-emptiness. This has been tackled via k-liveness bounded model checking [38 69], IC3
with strongly connected components [23]. or BDDs with Emerson-Leei fixed-point computation
[52]. Ranking functions were originally devised for program termination (55] and later gen- eralised to liveness certificates [5]
6
44 50
64 81 [25]. may be linear 22 [04], piecewise-
defined 776 [23 [24], word-level 32
471, lexicographic [22 82). or represented as disjunctive
well-founded relations 37
43 45
74 [03.. Traditional algorithms for the automated construction of
ranking functions and inductive invariants usually rely on constraint solving (using Farkas' lemma or
Positivstellensatz results) abstract interpretation [3 43 45
103 [05].
Machine Learning for Automated Reasoning Neural methods have permeated every layer of
formal reasoning. In theorem proving, they guide clause selection [53] [4], premise sclection [13
68 89
127], tactic prediction [100, [32), and even end-to-end proof search [54] [06]. In constraint
solving, neural approaches have been integrated into SMT
12
85
and SAT solving 66 79
113 [28], and have been further extended to combinatorial optimisation
83 and MILP
[60
93
Similar ideas have been applied to program synthesis [5
33
72
122 algorithm selection 88 86
termination analysis 77. circuit synthesis and repair from temporal logic specifications [46
and generation of satisfying traces for given LTL properties (66. A large body of work focussed on learning inductive invariants via teacher-learner loops [57] decision trees (58 76), random search
115), data-driven templates [98], neural networks [109
133 reinforcement learning 1166 131 and,
most recently, large language models (29 [71
[01 130]. These techniques target safety alone; I.TL.
specifications that encompass both safety and liveness are out of scope. Handling properties that combine safety and liveness using machine learning fills significant gap in the field.
Neural Certificates As opposed using neural networks to generate formal proof certificates, our approach uses neural networks to represent them (along with mathematical guarantees). falling within
the spectrum of neural certificates. This extends recent work control 2 30 48
78
92
95
108 135
137), formal verification of software and probabilistic programs 3
62 and model checking
reactive systems under pure liveness LTL properties [63]. Our work has enabled neural certificates to effectively prove arbitrary LTL properties, orders of magnitude faster than the state of the art.
7 Conclusion
We have presented novel and improved neural model checking approach for arbitrary compositions of safety and liveness specifications. By introducing specialised neural partially-rankin function architecture that (i) simultaneously represents inductive invariants and ranking functions and (ii) is amenable to training with numerically stable MILP solvers in counterexample-guiiee our method yields compact and naturally quantised certificates. We implemented lightweight Python prototype that combines off-the-shelf MILP (Gurobi), SMT (Bitwuzla), and BMC (EBMC) to train and certify the network in an iterative approach that provides formal guarantees (65 91 96
procedure,
Our improved technique attains speedups up to 10 x and 10 % higher completion (within 5 time limit) over the state-of-the-ar symbolic model checkers and prior work on neural model checking [24]] 28 63 [19], benchmark suite of 634 hardware model checking tasks encompassing safety, liveness and combined safety-liveness verification tasks written in System Verilog.
A complete specification for the functional correctness of reactive systems must capture both safety and liveness: the former guarantees the absence of undesired behaviour; the latter guarantees the presence of desired behaviour. Our approach has extended neural model checking to capture both safety and liveness, simultaneously. This paves a path towards the provably safe application of artificial intelligence and machine learning to the design of high-assurance industrial hardware, with impact to avionics [90] 118), automotive 197 120), medical devices 770 126), nuclear control
[7 99). rail signalling 34, 35), robotics [110 129 utility grids [25] 94 and more.
10

---

Acknowledgments
We thank Matthew Leeke, Sonia Marin, and Mark Ryan for their feedback and the anonymous reviewers for their comments and suggestions this manuscript. This work was supported in part by the Amazon Research Award Neural Software Verification (Fall 2024), and by the Advanced Research and Invention Agency (ARIA) under the Safeguarded Al programme.
References
[1] A. Abate, C. David, P. Kesseli, D. Kroening, and E. Polgreen. Counterexample guided inductive synthesis modulo theories. In CAV (1), volume 10981 of LNCS, pages 270-288. Springer, 2018.
[2] A. Abate, D. Ahmed, M. Giacobbe, and A. Peruffo. Formal synthesis of Lyapunov neural networks. IEEE Control. Syst. Letr., 5(3):773-778, 2021.
[3] A. Abate, M. Giacobbe, D. Roy. Learning probabilistic termination proofs. In CAV (2), volume 12760 of LNCS, pages 26. Springer, 2021.
[4] A. Abate, A. Edwards, M. Giacobbe, H. Punchihewa, and D. Roy. Quantitative verification with neural networks. In CONCUR, volume 279 of L/Ples, pages 22:1-22:188 Schloss Dagstuhl Leibniz--Zntrrum für Informatik, 2023.
[5] A. Abate, M. Giacobbe, and D. Roy. Stochastic omega-regular verification and control with supernartingals.. In CAV (3), volume 14683 of LNCS, pages 395-419. Springer, 2024.
[6] A. Abate, M. Giacobbe, and D. Roy. Quantitative supermartingale certificates. In (2), volume 15932 of LNCS, pages 3-28. Springer, 2025.
[7] Y. Alon and C. David. Using graph neural networks for program termination. In ESEC/SIG- SOFT FSE, pages 910-921. ACM, 2022.
[8] B. Alper and B. Schneider. Recognizing safety and liveness. Distributed Comput., 2(3):
1 117-126, 1987.
[9] R. Alur and T. A. Henzinger. Reactive modules. LICS, pages 207-218. IEEE, 1996.
[10] Z. S. Andraus, M. H. Liffiton, and K. A. Sakallah. Reveal: A formal verification tool for Verilog designs. In LPAR, volume 5330 of LNCS, pages 343-352. Springer, 2008
[11] C. Baier and J. Katoen. Principles of Model Checking. MIT Press, 2008
[12] M. Balunovic, P. Bielik, and M. Vechev. Learning solve SMT formulas. In NeurIPS, pages 10338-10349, 2018.
[13] K. Bansal, S. M. Loos, M. N. Rabe, C. Szegedy, and S. Wilcox. HOList: An environment for machine learning of higher order logic theorem proving. ICML, volume 97 Proceedings of Machine Learning Research, pages 454-463. PMLR, 2019.
[14] H. Barbosa, C. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mo- hamed, A. Niemetz, A. Nötzli, et al. eve5: versatile and industrial-strength SMT solver. In TACAS, LNCS, pages 415 4-42. Springer, 2022.
[15] S. Barke, E. A. Gonzalez, S. R. Kasibatla, T. Berg- Kirkpatrick, and N. Polikarpova. HYSYNTH: context-free L.M approximation for guiding program synthesis. In NeurlPS, 2024.
[16] A. Biere, N. Froleyks, and M. Preiner. Hardware model checking competition (HWMCC) 2020. htLps:ts///wwcccc.e githhb....u..... peattuub.o/// 10/2020/
[17] Biere, A. Cimatti, F. M. Clarke, and Zhu. Symbolic model checking without BDDs, In TACAS, volume 1579 of LNCS, pages 193-207. Springer, 1999.

---

[18] A. Biere, K. Heljanko, and S. Wieringa. AIGER 1.9 and beyond. Technical Report 1 11/2. Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040) Linz, Austria, 2011.
[19] A. Biere, N. Froleyks, and M. Preiner. Hardware model checking competition 2024, In FMCAD, pages 7-7. IEEE, 2024.
[20] A. R. Bradley, SAT-based model checking without unrolling. In VMCAI, volume 6538 of LNCS, pages 70-87. Springer, 2011.
[21] A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability, In CAV, volume 3576 of LNCS, pages 491-504, Springer, 2005.
[22] A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In ICALP, volume Springer, 2005.
3580 of LNCS. pages
[23] A. R. Bradley, F. Somenzi, Z. Hassan, and Y. Zhang. An incremental approach to model checking progress properties. In FMCAD, pages 144-153. FMCAD Inc., 2011.
[24] R. K. Brayton and A. Mishchenko. ABC: an academic industrial-strength verification tool. In CAV, volume 6174 of LNCS, pages 24 40. Springer, 2010.
[25] T. Brihaye, M. Jungers, S. Lasaulce, N. Markey, and G. Oreiby. Using model checking for analyzing distributed power control problems. EURASIP Journal on Wireless Commumications and Networking, 2010:1-13, 2010.
[26] J. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. Hwang. Symbolic model checking: 1020 states and beyond. In L/CS, pages 428 439. IEEE Computer Society, 1990.
[27] I. Buzhinsky and A. Pakonen. Model-checking detailed fault-tolerant nuclear power plant safety functions. IEEE Access, 7:162139 (166219--6226665 2019.
[28] Cavada, A. Cimatti, M. Dorigatti, A. Griggio, Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuXmv symbolic model checker. In CAV, volume 8559 of LNCS, pages 334-342. Springer, 2014.
[29] S. Chakraborty, K. Lahiri, S. Fakhoury, A. Lal, M. Musuvathi, A. Rastogi, A. Senthilnathan, R. Sharma, and N. Swamy. Ranking LLM-generated loop invariants for program verification. In EMNLP (Findings), pages 9164-9175. Association for Computational Linguistics, 2023.
[30] Y. Chang, N. Roohi, and Gao. Neural Lyapumov control. In NeurlPS, pages 3240-3244 2019.
[31] K. Chatterjee, H. Fu, and A. K. Goharshady. Termination analysis of probabilistic programs through Positivstellensatz'.. ss. In CAV (I), volume 9779 of LNCS, pages 3-22. Springer, 2016.
[32] H. Chen, C. David, D. Kroening, P. Schrammel, and B. Wachter. Bit-precise procedure-modular termination analysis. ACM Trans. Program. Lang. Syst., 40(1):1:1-1:388 2018.
[33] X. Chen, D. Song, and Y. Tian. Latent execution for neural program synthesis beyond domain-specific languages. In NewrlPS, pages 22196-22208, 2021.
[34] A. Cimatti, F. Giunchiglia, G. Mongardi, D. Romano, F. Torielli, and P. Traverso. Formal verification of railway interlocking system using model checking. Formal Aspects Comput. 10(4):361-380, 1998.
[35] A. Cimatti, R. Corvino, A. Lazzaro, I. Narasamdya, T. Rizzo, M. Roveri, A. Sanseviero, and A. Tchaltsev. Formal verification and validation of ERTMS industrial railway train spacing system. In CAV, volume 7358 of LNCS, pages 393. Springer, 2012.
[36] A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani. The MathSAT5 SMT solver. In TACAS, LNCS, pages 93-107. Springer, 2013.
[37] Cimatti, A. Griggio, C. Johannsen, K. Y. Rozier, and S. Tonetta. Infinite-state liveness checking with rlive. In CAV (I), volume 15931 of LNCS, pages 215-236. Springer, 2025.
12

---

[38] K. Claessen and N. Sörensson. A liveness checking algorithm that counts. In FMCAD, pages 52-59. IEEE, 2012.
[39] E. M. Clarke, E. A. Emerson, and A. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8()):244-263, 1986.
[40] E. M. Clarke, D. Long, and K. L. McMillan. Compositional model checking. In LICS, pages 353-362. IEEE Computer Society, 1989.
[41] E. M. Clarke, R. P. Kurshan, and H. Veith. The localization reduction and counterexample- guided abstraction refinement. In Essays in Memory of Amir Pnueli, volume 6200 of LNCS, pages 61-71. Springer, 2010.
[42] E. M. Clarke, O. Grumberg, D. Kroening, D. A. Peled, and H. Veith. Model Checking, 2nd Edition. MIT Press, 2018.
[43] Cook, A. Podelski, and Rybalchenko. Termination proofs for systems code. PLDI, pages 415-426. ACM, 2006.
[44] B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M. Y. Vardi. Proving that programs eventually do something good. In POPL., pages 265-276. ACM, 2007.
[45] Cook, A. See, and Zuleger. Ramsey vs. lexicographic termination proving. TACAS, volume 7795 of LNCS, pages 47-61. Springer, 2013.
[46] M. Cosler, F. Schmitt, C. Hahn, and B. Finkbeiner. Iterative circuit repair against formal specifications. In ICLR. OpenReview.net, 2023.
[47] C. David, D. Kroening, and M. Lewis. Unrestricted termination and non-termination arguments for bit-vector programs. In ESOP, volume 9032 of LNCS, pages 183-204. Springer, 2015.
[48] C. Dawson, Z. Qin, S. Gao, and C. Fan. Safe nonlinear control using robust neural Lyapunov- barrier functions. CoRL, volume 164 of Proceedings of Machine Learning Research, pages 1724-1735, PMLR, 2021.
[49] L. De Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, LNCS, pages 337-340. Springer, 2008
[50] Dimitrova, M. F. Fioriti, H. Hermanns, and R. Majumdar. Probabilistic CTL* * The deductive way. In TACAS, volume 9636 of LNCS, pages 280-296. Springer, 2016.
[51] A. Lutet-Lutz, E. Renault, M. Colange, F. Renkin, A. G. Aisse, P. Schlehuber-Caissier, T. Medioni, A. Martin, Dubois, Gillard, and H. Lauko. From Spot 2.0 to Spot 2.10: What's 's new? In CAV (2), volume 13372 of LNCS, pages 174-187. Springer, 2022.
[52] E. A. Emerson and C. Lei. Modalities for model checking: Branching time strikes back. In POPL, pages 84 9.. ACM Press, 1985.
[53] V. Firoiu, F. Aygün, A. Anand, 7.. Ahmed, Glorot, L. Orseau, L. M. Zhang, D. Precup, and
S. Mourad. Training a first-order theorem prover from synthetic data. CoRR, abs/2103.033798, 2021.
[54] E. First, M. N. Rabe, T. Ringer, and Y. Brun. Baldur: Whole-proof generation and repair with large language models. In ESEC/SIGSOFT FSE, pages 1229-1241. ACM, 2023.
[55] R. W. Floyd. Assigning meanings to programs. In Proceedings of Symposium in Applied Mathematics, volume 19, pages 19-32, 1967.
[56] H. Foster. The 2022 Wilson research group functional verification study, 2022. URL https: https://blogs... sw www.siimens.comm
http:///wwww..ee..oooooooo////// prologue- theeettheeeee 2022-0222220 wwwson wtw.:oowoo...eedddoooooooooooone
[57] P. Garg, C. Löding, P. Madhusudan, and D. Neider. ICE: robust framework for learning invariants. In CAV, volume 8559 of LNCS, pages 69-87. Springer, 2014.
13

---

[58] P. Garg, D. Neider, P. Madhusudan, and D. Roth. Learning invariants using decision trees and implication counterexamples. POPL, pages 512-512. ACM, 2016.
[59] M. Gario and A. Micheli. PySMT: A solver-agnostic library for fast prototyping of SMT-based algorithms. In SMT Workshop 2015, 2015.
[60] Z. Geng, X. L. Wang, X. Li, Y. Zhang, and F. Wu. A deep instance generative framework for MILP solvers under limited data availability. In NeurIPS, 2023.
[61] M. Ghanem, F. Schmitt, J. Siber, and B. Finkbeiner. Learning better representations from less data for propositional satisfiability. In NeurlPS, 2024.
[62] M. Giacobbe, D. Kroening, and J. Parsert. Neural termination analysis. In ESEC/SIGSOFT FSE, pages 633-645 ACM, 2022.
[63] M. Giacobbe, D. Kroening, A. Pal, and M. Tautschnig. Neural model checking. In NeurIPS, 2024.
[64] O. Grumberg, Francez, J. A. Makowsky, and W. de Roever. A proof rule for fair termination of guarded commands. Inf. Control., 66(1/)):83 1985.
[65] Gurobi Optimization, LLC. Gurobi Optimizer Reference Manual, 2024. URL https://www gurobi. com
[66] C. Hahn, F. Schmitt, U. Kreber, M. N. Rabe, and Finkbeiner. Teaching temporal logics to neural networks. In ICLR. OpenReview.net, 2021.
[67] R. T. Iearte, L. Illanes, M. P. Castro, A. A. Ciré, S. A. Mellraith, and J. C. Beck. Training binarized neural networks using MIP and CP. In CP, volume 11802 of LNCS, pages 401-417. Springer, 2019.
[68] G. Irving, C. Szegedy, A. A. Alemi, N. Eén, F. Chollet, and J. Urban. Deepmath deep sequence models for premise selection. In NIPS, pages 2235-2243, 2016.
[69] A. Ivrii, Z. Nevo, and J. Baumgartner. k-FAIR = K-LIVENESS + MAIR-revisiting SAT-based liveness algorithms. In FMCAD, pages 1-5. IEEE, 2018
[70] Z. Jiang, M. Pajie, S. Moarref, R. Alur, and R. Mangharam. Modeling and verification of a dual chamber implantable pacemaker. In TACAS, volume 7214 of LNCS, pages 188-20% Springer, 2012.
[71] A. Kamath, A. Senthilnathan, S. Chakraborty, P. Deligiannis, S. K. Lahiri, A. Lal, A. Rastogi, S. Roy, and R. Sharma. Finding inductive loop invariants using large language models. CoRR, abs/2311. 1. 1.09988, 2023.
[72] N. Kobayashi, Sekiyama, I. Sato, and H. Unno. Towards synthesis and verification. Formal Methods in System Design, pages 1-33, 2025.
guided program
[73] D. Kroening and O. Strichman. Efficient computation of recurrence diameters. In VMCAI, volume 2575 of LNCS, pages 298-309, Springer, 2003.
[74] D. Kroening, N. Sharygina, A. Tsitovich, and C. M. Wintersteiger. Termination analysis with compositional transition invariants. In CAV, volume 6174 of LNCS, pages 89-103. Springer, 2010.
[75] O. Kupferman and M. Y. Vardi. Model checking of safety properties. In CAV, volume 1633 of LNCS, pages 172-183. Springer, 1999.
[76] S. Kura, H. Unno, and I. Hasuo. Decision tree learning in CEGIS-bascl termination analysis. In CAV (2), volume 12760 of LNCS, pages 75-98. Springer, 2021.
[77] L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Eng., 12):125-143, 1977.
14

---

[78] M. Lechner, D. Zikelić, K. Chatterjee, and T. A. Henzinger. Stability verification in stochastic control systems via neural network supermartingales. AAAL, pages 7326-7336. AAAI Press, 2022.
[79] G. Lederman, M. N. Rabe, S. Seshia, and E. A. Lee. Learning heuristics for quantified boolean formulas through reinforcement learning. In ICLR. OpenReview.net, 2020.
[80] W. Leeson and M. B. Dwyer. Algorithm selection for software verification using graph neural networks, ACM Trans. Softw. Eng. Methodol, 33(3).6::177:336, 2024.
[81] D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP, volume 115 of LNCS, pages 264-277. Springer, 1981.
[82] J. Leike and M. Heizmann. Ranking templates for linear loops. Log. Methods Comput. Sci., 11(1), 2015.
[83] Y. Li, J. Guo, R. Wang, and J. Yan. From distribution learning in training to gradient search in testing for combinatorial optimization. In NeurlPS, 2023.
[84] S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk. Deep network guided proof search. In LPAR, volume 46 of EPiC Series in Computing, pages 85-105. EasyChair, 2017.
[85] Z. Lu, S. Siemer, P. Jha, F. Manea, J. Day, and V. Ganesh. Z3-alpha: reinforcement learning guided SMT solver. System Description: SMT-COMP, 2023.
[86] Z. Lu, P. Chien, N. Lee, and V. Ganesh. Algorithm selection for word-level hardware model checking (student abstract). In AAAI, pages
AAAI Press, 2025.
[87] McMillan. Applying SAT methods in unbounded symbolic model checking. In CAV, volume 2404 of LNCS, pages 250-264. Springer, 2002.
[88] K. I.. McMillan. Toward liveness proofs at scale. In CAV (1), volume 14681 of LNCS, pages 255-276. Springer, 2024.
[89] M. Mikula, S. Tworkowski, S. Antoniak, B. Piotrowski, A. Q. Jiang, J. P. Zhou, C. Szegedy, L. Kucinski, P. Milos, and Y. Wu. Magnushammer: A transformer-based approach to premise selection. In ICLR. OpenReview.ne,, 2024.
[90] Y. Moy, E. Ledinot, H. Delseny, Wiels, and B. Monate. Testing or formal verification: DO-178C alternatives and industrial experience. IEEE Softw, 30(3):50-57, 2013.
[91] R. Mukherjee, D. Kroening, and T. Melham. Hardware verification using software analyzers. In ISVLSI, pages 7-12. IEEE Computer Society, 2015.
[92]
A. Nadali, Murali, A. Trivedi, and M. Zamani. Neural closure certificates. In AAAI, pages 21 21446-21451 AAAT Press, 2024.
[93] V. Nair, S. Bartunov, F. Gimeno, I. von Glehn, P. Lichocki, Lobov, O'Donoghue, N. Son- nerat, C. Tjandraatmadja, P. Wang, R. Addanki, T. Hapuarachchi, T. Keck, J. Keeling, P. Kohli, I. Ktena, Y. Li, O. Vinyals, and Y. Zwols. Solving mixed integer programs using neural networks. CORR, abs/2012. 133499 2020.
[94] Y. Nemouchi, S. Etigowni, A. J. Zolan, and R. Macwan. Formally verified ZTA requirements for OT/ICS environments with Isabelle/HOL. VSTTE, volume 14095 of LNCS, pages 64 84. Springer, 2023.
[95] G. Neustroev, M. Giacobbe, and A. Lukina. Neural continuous-time supermartingale certifi- cates. In AAAL, pages 77538-27546.. AAAI Press, 2025.
[96] Niemetz and M. Preiner. Bitwuzla. In CAV (2), volume 13965 of LNCS, pages 3-17. Springer, 2023.
[97] M. Nyberg, D. Gurov, C. Lidström, A. Rasmusson, and J. Westman. Formal verification in automotive industry: Enablers and obstacles. In ISoLA (4), volume 11247 of LNCS, pages 139-158. Springer, 2018.
15

---

[98] S. Padhi, R. Sharma, and T. D. Millstein. Data-driven precondition inference with learned features. PLDI, pages 12-56. ACM, 2016.
[99] A. Pakonen, T. Tahvonen, M. Hartikainen, and M. Pihlanko. Practical applications of model checking in the Finnish nuclear industry. In 10th International Topical Meeting on Nuclear Plant Instrumentation, Control and Human Machine Interface Technologies (NPIC HMIT 2017). American Nuclear Society, pages 1342-13522 2017.
[100] A. Paliwal, S. M. Loos, M. N. Rabe, K. Bansal, and C. Szegedy. Graph representations for higher-order logic and theorem proving. In AAAI, pages 2967-2974. AAAI Press, 2020.
[101] K. Pei, D. Bieber, K. Shi, C. Sutton, and P. Yin. Can large language models reason about program invariants? In ICML, volume 202 of Proceedings of Machine Learning Research, pages 27496-27520. PMLR, 2023.
[102] A. Pnueli. The temporal logic of programs. In FOCS, pages 46-57. IEEE, 1977.
[103] A. Podelski and A. Rybalchenko. Transition invariants. In LICS, pages 32-41. IEEE, 2004.
[104] A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, volume 2937 of LNCS, pages 239-251. Springer, 2004.
[105] A. Podelski and A. Rybalchenko. Transition predicate abstraction and fair termination. ACM Trans. Program. Lang. Syst., 29(3):15, 2007.
[106] S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03399 2020.
[107] M. Preiner, N. Froleyks, and A. Biere. Hardware model checking competition (HWMCC) 2024. URL https: http:///cmcc..ghuubbbo.. 10/2024/
[108] Z. Qin, K. Zhang, Y. Chen, J. Chen, and C. Fan. Learning safe multi-agent control with decentralized neural barrier certificates. In ICLR. OpenReview.net, 2021.
[109] G. Ryan, J. Wong, J. Yao, R. Gu, and S. Jana. CLN2INV: learning loop invariants with continuous logic networks. In ICLR. OpenReview.net, 2020.
[110] S. Scherer, F. Lerda, and E. M. Clarke. Model checking of robotic control systems. In ISAIRAS, 2005.
[111] F. Schmitt, C. Hahn, M. N. Rabe, and B. Finkbeiner. Neural circuit synthesis from specification patterns. In NeurIPS, pages 15408-15420, 2021.
[112] J. Scott, A. Niemetz, M. Preiner, S. Nejati, and V. Ganesh. MachSMT: A machine learning- based algorithm selector for SMT solvers. In TACAS (2), volume 12652 of LNCS, pages 303-325. Springer, 2021.
[113] D. Selsam, M. Lamm, B. Bünz, P. Liang, I. de Moura, and D. L.. Dill. Learning a SAT solver from single-bit supervision. In ICLR (Poster). OpenReview.nen 2019.
[114] T. Scufert, F. Winterer, C. Scholl, K. Scheibler, T. Paxian, and B. Becker. Everything you always wanted to know about generalization of proof obligations in PDR. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 13541:135 2023.
[115] R. Sharma and A. Aiken. From invariant checking to invariant inference using randomized search. Formal Methods Syst. Des., 48(3):235-256, 2016.
[116] X. Si. H. Dai, M. Raghothaman, M. Naik, and L. Song. Learning loop invariants for program verification. In NeurlPS, pages 7762-7773, 2018
[117] A. Solar-Lezama, L. Tancau, R. Bodík, S. A. Seshia, and V. A. Saraswat. Combinatorial sketching for finite programs. ASPLOS, pages 404 415. ACM, 2006.
[118] J. Souyris, V. Wiels, Delmas, and H. Delseny. Formal verification of avionics software products. In FM, volume 5850 of LNCS, pages 532-546. Springer, 2009,
16

---

[119] Y. Su, Q. Yang. Ci, T. Bu, and Z. Huang. The rIC3 hardware model checker. In CAV volume 15931 of LNCS, pages 185-199. Springer, 2025.
[120] X. Sun, H. Khedr, and Y. Shoukry. Formal verification of neural network controlled au- tonomous systems. In HSCC, pages 147-156. ACM, 2019.
[121] T. Thorbjarnarson and N. Yorke-Smith. On training neural networks with mixed integer programming. CoRR, abs/2009. 00325,, 2020.
[122] D. Trivedi, J. Zhang, S. Sun, and J. Lim. Learning to synthesize programs as interpretable and generalizable policies. In NeurlPS, pages 25146-25663, 2021.
[123] C. Urban. The abstract domain of segmented ranking functions. In SAS, volume 7935 of LNCS, pages 43-62. Springer, 2013.
[124] C. Urban. FuncTiio: An abstract domain functor for termination (competition contribution). In TACAS, volume 9035 of LNCS, pages 464-466. Springer, 2015.
[125] M. Y. Vardi. Verification of concurrent programs: The theoreta- framework. Ann. Pure Appl. Log., 51(1-)):79-99 1991.
[126] D. A. Vogel. Medical Device Software Verification,, Validation and Compliance. Artech House, 2011.
[127] M. Wang, Tang, Wang, and J. Deng. Premise selection for theorem proving by deep graph embedding. In NIPS, pages 2796, 2017.
[128] W. Wang, Y. Hu, M. Tiwari, S. Khurshid, K. L. McMillan, and R. Mikkkulainen. NeuroBack: Improving CDCL SAT solving using graph neural networks. ICLR. OpenReview.ned 2024.
[129] M. Weißmann, Bedenk, C. Buckl, and C. Knoll. Model checking industrial robot systems. In SPIN, volume 6823 of LNCS, pages 161-176. Springer, 2011.
[130] G. Wu, W. Cao, Y. Yao, H. Wei, T. Chen, and X. Ma. LLM meets bounded model checking: Neuro-symbolic loop invariant inference. ASE, pages 406-417. ACM, 2024.
[131] M. Wu, T. Tsukada, H. Unno, T. Sekiyama, and K. Suenaga. Learning heuristics for template- based CEGIS of loop invariants with reinforcement learning. arXiv:2107.09766, 2021.
[132] K. Yang and J. Deng. Learning to prove theorems via interacting with proof assistants. In ICML, volume 97 of Proceedings of Machine Learning Research, pages 6984-6994. PMLR, 2019.
[133] J. Yao, G. Ryan, J. Wong, Jana, and R. Gu. Learning nonlinear loop invariants with gated continuous logic networks. In PLDI, pages 106-120. ACM, 2020.
[134] J. Yao, R. Tao, R. Gu, and J. Nieh. Mostly automated verification of liveness properties for distributed protocols with ranking functions. Proc. ACM Program. Lang.. 8(POPL):1028-100 2024.
[135] H. Zhao, X. Zeng. Т. Chen, and Z. Liu. Synthesizing barrier certificates using neural networks. In HSCC, pages 25:1-25:11. ACM, 2020.
[136] Zikelic, M. Lechner, Henzinger, and K. Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In AAAI, pages 11926-11935. AAAI Press, 2023.
[137] Zikelic, Lechner, A. Verma, K. Chatterjee, and A. Henzinger. Compositional policy learning in stochastic control systems with formal guarantees. In NewrIPS, 2023.
17

---

Model
LTL Specification (Pure-Liveness)
FG !rst
GF sig
DELAY
FG !rst GF
sig A X !sig
LCD Controller
FG lcd_enable GF ready
Blink
FG !rst GF ledON
Thermocouple
FG !rst GF get_data
FG !rst + GF disp
7-Segment
FG !rst ->
GF disp ^ GF disp
12c Stretch
FG |xrst A ena
GF stre
Pulse Width Modulation
GF !pulse
VGA Controller
FG !rst -> GF disp_
UART Transmitter
FG !rst GF wait
Load-Store
FG !rst GF sig
FG ! + GF sig
Gray Counter
FG !rst + GF sig ^ X !sig
FG !rst
GF sig A GF !sig
Table 2: Model Name and LTL Specification in our Benchmark (Pure-Liveness)
Model
LTL Specification (Pure-Safety)
G !err
DELAY
G G(sig sig
- X 1sig
G (Ilcd_enable) ready) X ready
LCD Controller
G X wait - busy
Blink
G (mode1 A X model) - (cnt!=0)
G ((( !spi_ A get_data A !rst ) + X get__data
Thermocouple
7-Segment
G (!sig A X !sig A !rst) + (dso A ds0) V (ds1 A X ds1
12c Stretch
G (!strc A X strr)
+ X switch
Pulse Width Modulation
(pulseLB + pulse)
!pulseUB + !pulse
G (en !rst) + (hs + X !hs) (!hs + X hs)
VGA Controller
G (en !rst) + (vs X !vs) (!vs + X vs)
UART Transmitter
G (wait bussy
transmit busy
Load-Store
G sig X X !sig
Gray Counter
G (sig !rst) + X !sig
Table 3: Model Name and LTL Specification in our Benchmark (Pure-Safety)
18

---

Model
LTL. Specificatiin (Safety-I Liveness)
G !rst + XG ent N U sig)
Delay
FG !rst - FG cnn N U sig
LCD Controller
receive + receevve U ready
Blink
G !rst + G [ledON + [ledON modee)
Thermocouple
G !rst + G pause + ( (aass U get_
7-Segment
G !rst + G (( ds0 A X ds0) ds1 X Xds1)
U sig
i2c Stretch
G !rst G !strc + |strc U switch
Pulse Width Modulation
GF !pulseUB XG !pulseUB !pulse
VGA Controller
G (Vent G(Vente == 0) (( (Vent == 0) U Hent == 0))
UART Transmitter
G !rrt G busy
busy wait
G !rst + G modeUP + modeUP U sig)
Load-Store
G !rst - G
modeUP + !sig modeDDWN
G !rst
XG cnt V sig
Gray Counter
FG !rst
FG cnt
U sig
Table Model Name and LTL. Specification in our Benchmark (Safety + Liveness)
A Details of the Case Studies
We benchmark our tool on eleven RTL designs. Ten are adopted from the neural model-checking study of [63], which provided only pure-liveness, properties. We extend every design with semantically natural pure safety and safety plus liveness specifications. Table 2 lists all pure-liveness formulas, Table 3 the pure-safety formulas, and Table the safety-liveness formulas, all Linear Temporal Logic (LTL.). Below we discuss each design together with its full specification suite.
Delay (DELAY). counter cnt raises a pulse sig after fixed delay and reset by rst. Liveness requires FG rsst -> GF sig and, prevent sig from sticking, FG Irst - GF (sig A X sig). Safety bounds the counter, G ent <= N, and clears sig in the next cycle, G (sig - X !sig). Safety-Livenes formulas constrain ent until sig occurs, !rst - XG (ent N U sig) and its eventually variant FG !rst + FG (cnt < N sig).
LCD Controller (LCD) After initialisation the controller waits for lcd_ seable, switches from ready to send, and returns to ready. Liveness demands FG lcd_enable - GF ready. Safety preserves ready when lcd_enable low, G((!Icd_ena)) enable A ready) + X readyy. and asserts busy in wait. G(X wait > busy); for safety- livene-l a receive phase persists until ready, G(receive + (receive U ready)).
Blink (BLINK). counter toggles led on every wrap and raises one-cycle flag flg. Liveness asserts FG !rst - GF GeddNN, while safety enforces staying in mode1 if cnt has wrapped: G( G(mode11 A Xmode1) + X(cnt + 0)). The safety-liveness specification ensures that led remains on until modeO is reached: G Isst + G(ledON > (ledON U mode0))..
Thermocouple (Tmcp.). The FSM cycles through start, get_data data, pause. Liveness requires FG !ra + GF get_data. Safety keeps get_data active idle bus and safety-liveness keeps pause active until get_data becomes reachable: G(!spi_busy A get_data A !rst + X get_data) and G ! - G G(pause (pause U get_data)).
19

---

7-Segment (7-Seg) Two displays alternate unless reset. Liveness enforces FG !rst - (GF disp A GF disp 1) and the single-display variant FG !sst + GF disp 1. Safety freezes the display in the absence of sig: G(!sigAXI sigg/ sigA!rst !rst ((600->ass)\ddaaAAaae)) while safety-livente holds the display until sig, G !rat + G(((ds) A Xda0) V (ds1 A Xds1)) U sig).
Pe Stretch (i2cS) Timing signals scl_clk and data_clk clk are generated according bus fre- quency; stretch handles clock stretching. Liveness states FG (!rst A ena) + GF stre. Safety links rising stretch to switch: G(!stre A Xstre Xswitch) meanwhile safety- liveness, under permanent reset-low, keeps stretch low until switch, G ! G(!strc (!stre U switch)).
Pulse Width Modulation (PWM). . An N-bit counter drives pulse; the design must regularly unset the pulse. Accordingly, liveness requires GF !pulse. Two guard signals bound the duty-cycle window: pulseLB (minimum width) and pulseUB (maximum width). Safety enforces these bounds every cycle, G((pulseLB pulsse) A (!pulseUB !pulse)) and safety-liveness strengthens them with a fairness clause that forces the upper bound to be violated-and thus pulse to be low-infinitely often: GF !pulseUB XG (G!luuleUUB !pulse).
VGA Controller (VGA). Horizontal and vertical counters drive disp_ena. Liveness: FG !rst -> GF disp_ ena. Safety flips hs and under disp_ena: G((en A !rst) > ((hs <> X!hs) V (ths ++ Xhs))). G((en A !rst) - ((vs + X!vs) V (!vs Xvs))), and safety-liveness asserts vertical-horizontal counter relationship G (Vent==0 + (Vent==0 U Hcnt==0)).
UART Transmitter (UARTt). The FSM toggles between wait and transmit. Liveness: FG !rst GF wait. Safety couples busy with required modes: G((wiit + !busy) A (transmit + busy)), and safety-liveness under permanent reset-low holds busy until wait, !rst - Gbbusy > (busy wait))..
Load-Store (LS) A counter counts up in load, down in store; sig triggers the switch. Liveness: FG !rrt + GF sig. Safety clears sig after cycles: G(sig + XX!sig). The safety- liveness formulas hold modeUP until sig and, symmetrically, !sig until modeDOWN: G !rst + GmooeeU + (modeUP U sig)) and G !rst XG(oodeUP > (!sig U modeDOwN)).
Gray Counter (Gray). Counts in Gray code to minimise bit flips. Liveness: FG ! - GF sig, FGIrst - GF(sig Xtsig), and FGIrst (GFsig GF!sig). Safety clears sig one step later: G (sig/ A !rst + X!sig) Safety-liveness bind the counter until sig: G ! - XG(ent 0 U sig) and its eventually counterpart FG !rst + FG(ent > U sig).
Collectively, these benchmarks exercise handshake logic, clock stretching, display timing, PWM generation, UART serialisation, counter bounds, and Gray-code sequencing. Each property appears in lire-liveness, pure-safety, and safety-liveness form, enabling comprehensive assessment across the complete verification spectrum.
20

---

NeurIPS Paper Checklist
1. Claims
Question: Do the main claims made in the abstract and introduction accurately reflect the
paper's contributions and scope?
Answer: [Yes]
Justification: The main claims of this paper are stated in the abstract and elaborated in Section 1
There, we briefly outline the theoretical underpinnings of these claims and summarise experimental results that quantify the scalability of our approach.
Guidelines:
The answer NA means that the abstract and introduction do not include the claims made in the paper.
The abstract and/or introduction should clearly state the claims made, including the contributions made the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers.
The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalise to other settings.
is fine to include aspirational goals as motivation as long as is clear that these goals not attained by the paper.
2. Limitations
Question:
Does the paper discuss the limitations the work performed by the authors?
Answer: [Yes]
Justification: SeetionnSinnludess a dedicated Strengths and Limitations subsection, where we explicitly state our drawbacks and justify their reasonableness, along with discussion of theoretical and practical constraints. Section 5 contains a class of problems (pure- safety) where we underperform. The accompanying Threats Validity subsection critically evaluates the scope of our claims by motivating the benchmark selection used for comparison against alternative verification methods.
Guidelines:
The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper.
The authors encouraged to create separate "I "Limitations" section in their paper.
The paper should point any strong assumptions and how robust the results to violations of these assumptions (e.g.. independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be.
The authors should reflect the scope of the claims made, e.g., if the approach only tested on a few datasets or with few runs. In general, empirical results often depend on implicit assumptions, which should be articulated.
The authors should reflect the factors that influence the performance of the approach. For example, facial recognition algorithm may perform poorly when image resolution low or images are taken in low lighting. Or speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon.
The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size.
If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness.
While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, worse outcome might be that reviewers discover limitations that aren't acknowledged the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an impor- tant role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations.
21

---

3. Theory assumptions and proofs
Question: For each theoretical result, does the paper provide the full set of assumptions and complete (and correct) proof?
Answer: [Yes]
Justification: We provide references for all theoretical foundations underpinning work, including automata-theoreti LTL model checking, fair termination, inductive invariant and the use of ranking functions and inductive invariants in see 2
Guidelines:
The answer NA means that the paper does not include theoretical results. All the theorems, formulas, and proofs in the paper should be numbered and cross- referenced.
All assumptions should be clearly stated or referenced in the statement of any theorems.
The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged provide short proof sketch to provide intuition.
Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material.
Theorems and Lemmas that the proof relies upon should be properly referenced.
4. Experimental result reproducibility
Question: Does the paper fully disclose all the information needed to reproduce the main ex- perimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?
Answer: [Yes]
The Implementation subsection of Section describes the full pipeline used in our prototype and specifies the versions of all external dependencies. It outlines the neural network architecture under both linear and automatic configurations, as well as the learning engines used. This section also states the configurations employed in our main experiments and ablation studies. In contrast, Section 3 addresses the theoretical underpinnings of the learning procedure, including dataset generation, the design of the neural architecture, and the SMT-based check step, part of our iterative approach. Together, these sections provide sufficient detail to replicate our method for neural model checking of safety and liveness properties. Additionally, the Experimental Setup subsection discusses the versions of competing tools, the hardware environment used for evaluation, and the translation procedure from System Verilog to the appropriate input formats for each tool. For reproducibility and further implementation details, our code and benchmarks will be made publicly available.
Justification:
Guidelines:
The answer NA means that the paper does not include experiments. If the paper includes experiments, a No answer this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not.
If the contribution is dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable.
Depending on the contribution, reproducibility can be accomplished in various ways. For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is specific model and empirical evaluation, it may be necessary to either make possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed.
While NeurIPS does not require releasing code, the conference does require all submis- sions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. For example
22

---

(a) If the contribution is primarily a new algorithm, the paper should make it clear how reproduce that algorithm.
(b) If the contribution is primarily
model architecture, the paper should descrihe the architecture clearly and fully.
(c) the contribution is a new model (e.g., a large language model), then there should either be way to access this model for reproducing the results or way to reproduce the model (e.g., with an open open-source dataset or instructions for how to construct the dataset).
(d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome describe the partieular way they provide for reproducibility. In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should possible for other researchers to have some path to reproducing verifying the results.
5. Open access to data and code
Question: Does the paper provide open access the data and code, with sufficient instruc- tions to faithfully reproduce the main experimental results, as described in supplemental material?
Answer: [Yes]
Justification: Alongside the paper, we provide a zip archive as per NeurlPS guidelines. It includes all benchmarks, experiment scripts, and README, md with detailed instructions for reproducing our results.
Guidelines:
The answer NA means that paper does not include experiments requiring code.
Please see the NeurIPS code and data submission guidelines (kttps://nips.ce ec/
public/guides//0 Sawaas//ooSSuusssiooooooooo
for more details.
While we encourage the release of code and data, we understand that this might not be possible, so "No" an acceptable answer. Papers cannot be rejected simply for not including code, unless this is central to the contribution (e.g., for new open-source benchmark).
The instructions should contain the exact command and environment needed to run to reproduce the results. See the NeurIPS code and data submission guidelines (https wwwp:///wwdeeeeeee wttp://oooeeeeeeeeeeeeeeeee
//nips
ssioiooiccccycicoiicccoooaoiiici for more details.
The authors should provide instructions on data access and preparation, including how access the raw data, preprocessed data, intermediate data, and generated data, etc.
The authors should provide scripts to reproduce all experimental results for the new proposed method and baselines. If only subset of experiments are reproducible, they should state which ones are omitted from the script and why.
At submission time, to preserve anonymity, the authors should release anonymized versions (if applicable).
Providing as much information as possible in supplemental material (appended to the paper) recommended, but including URLs to data and code permitted.
6. Experimental setting/details
Question: Does the paper specify all the training and test details (e.g., data splits, hyper- parameters, how they were chosen, type of optimizer, etc.) necessary to understand the results?
Answer: [Yes]
Justification: Section 5 particularly the Implementation subsection, discusses our use of single hyperparameter and outlines how it is selected. We also detail the tools used for the learn and check phases. Our approach to dataset generation is described in Section 3 and full description of the benchmark suite is provided in Appendix A
Guidelines:
The answer NA means that the paper does not include experiments.
The experimental setting should be presented the core the paper to level of detail
that is necessary to appreciate the results and make sense of them.
23

---

The full details can be provided either with the code, in appendix, or as supplemental
material.
7. Experiment statistical significance
Does the paper report error bars suitably and correctly defined or other appropriate information about the statistical significance of the experiments?
Question:
Answer: [Yes]
Justification: Because formal-verificttion tools are deterministic and must return provably correct answers, traditional variance measures-error bars and confidence intervals-are not meaningful. Instead for statistical significance, we run each tool once on a substantial benchmark suite of 634 instances and provide cactus plots, an experimental setup consistent with community practice in formal verification competitions such as HWMCC. Statistical evidence is conveyed by cactus plots (Figure 3 a-ce;; Figure 4 (bbc)), which report, for every time cap up to 15 min, the cumulative number of tasks each competitor completes. Seatter plots (Figure d-- complement this view by plotting one point per benchmark task, exposing the full runtime distribution rather than aggregate summaries. We additionally annotate salient figures our text-e.g., the percentage tasks finished within given cap and the count lying to the right of the 10x diagonal-to underscore the consistent performance gaps observed across tools and throughout our ablation study.
Guidelines:
The answer NA means that the paper does not include experiments.
The authors should answer "Yes" if the results are accompanied by error bars, confi- dence intervals, statistical significance tests, least for the experiments that support the main claims of the paper.
The factors of variability that the error bars are capturing should be clearly stated (for example, train/test split, initialization, random drawing of some parameter, or overall run with given experimental conditions).
The method for calculating the error bars should be explained (closed form formula, call to a library function, bootstrap, etc.)
The assumptions made should be given (e.g., Normally distributed errors).
It should be clear whether the error bar is the standard deviation the standard error of the mean.
It is OK to report 1-sigma error bars, but one should state it. The authors should preferably report a 2-sigma error bar than state that they have 96% CI, if the hypothesis of Normality of errors is not verified.
For asymmetric distributions, the authors should be careful figures symmetric error bars that would yield results that are out of range (e.g. negative error rates).
show in tables or
If error bars are reported in tables or plots, The authors should explain in the text how they were calculated and reference the corresponding figures tables in the text.
8. Experiments compute resources
For each experiment, does the paper provide sufficient information on the com- puter resources (type of compute workers, memory, time execution) needed to reproduce the experiments?
Question:
Answer: [Yes]
The compute environment is described in the Experimental Setup subsection of Section 5) where we specify our Amazon EC2 instance (type and configuration) and report the total wall-clock time across all experiments. To avoid cluttering the paper with over 7 000 individual measurements (634 tasks multiple settings), we provide the complete runtime data in the supplementary ZIP archive and through cactus plots. In the main paper, one can visualise the per-task runtime through the cactus (Figure aac))Figure b-c)) and scatter plots 3 d-f)).
Justification:
Guidelines:
The answer NA means that the paper does not include experiments.
24

---

The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage.
The paper should provide the amount of compute required for each of the individual experimental rums as well as estimate the total compute.
The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't 't make it into the paper).
9. Code of ethics
Question: Does the research conducted in the paper conform, in every respect, with the NeurlPS Code of Ethics
Answer: [Yes]
Justification: We affirm that all content presented in this work is disclosed with full academic integrity. All original contributions are properly eited, and methodology is described in detail throughout the paper to ensure reproducibility. In addition, we provide our full implementation and experimental setup as part of the supplementary materials. Our experi- ments exclusively use synthetic data, with no human subjects involved, and are therefore fully aligned with ethical research standards. The goal of our method is enhance the reliability and safery of computer systems. The benchmark hardware designs are drawn from prior work, which is cited accordingly, with one additional design introduced by us. While the sure-liveness specifications are taken from the same work, we developed additional pure-safety and liveness specifications based on the semantics of each design. We have reviewed the NeurIPS Code of Ethics and confirm our strict adherence to its principles. Guidelines:
The answer NA means that the authors have not reviewed the NeurlPS Code of Ethics.
If the authors answer No. they should explain the special circumstances that require deviation from the Code of Ethics.
The authors should make sure to preserve anonymity (e.g.. if there a special consid- eration due to laws or regulations in their jurisdiction).
10. Broader impacts
Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?
Answer: [Yes]
Justification: As discussed in the introduction and conclusion, improving the correctness of hardware designs prior fabrication contributes to the development of safer and more reliable systems. Avoiding the manufacture of flawed silicon also reduces material waste. We are not aware of any direct path by which our method could be applied harmful ends.
Guidelines:
The answer NA means that there no societal impact of the work performed.
If the authors answer NA or No, they should explain why their work has no societal impact why the paper does not address societal impact.
Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.
The conference expects that many papers will be foundational research and tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster.
The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional unintentional) misuse of the technology.
25

---

If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition attacks, mechanisms for monitoring misuse, mechanisms to monitor how system learns from feedback over time, improving the efficiency and accessibility of MI.).
11. Safeguards
Does the paper describe safeguards that have been put in place for responsible release of data models that have high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?
Question:
Answer: [NA]
Our work contributes to improving the correctness hardware systems. The benchmark designs used in evaluation extensions of prior benchmark suite and consist of standard hardware modules drawn from well-known literature. These designs are in the public domain and do not pose any risk of misuse.
Justification:
Guidelines:
The answer NA means that the paper poses such risks.
Released models that have high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters.
Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images.
We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make best faith effort.
12. Licenses for existing assets
Are the creators original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?
Question:
Answer: [Yes]
Justification: We include the licenses for all tools stated in section 5 and provide appropriate citations for each.
Guidelines:
The answer NA means that the paper does not use existing assets.
The authors should cite the original paper that produced the code package dataset.
The authors should state which version of the asset used and, possible, include URL.
The name of the license (e.g., CC-BY 4.0) should be included for each asset.
For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.
If assets are released, the license, copyright information, and terms of in the package should be provided. For popular datasets, wwwppsawitthteee thwode..teccee....o. com datasets has curated licenses for some datasets. Their licensing guide can help determine the license of dataset.
For existing datasets that re- re-packaged, both the original license and the license of the derived asset (if has changed) should be provided.
If this information is not available online, the authors are encouraged to reach out to the asset's s creators.
13. New assets
Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?
Answer: [Yes]
26

---

Justification: We include the source code of our prototype and the extended benchmark suite as supplementary material to this paper, released under the MIT License.
Guidelines:
The answer NA means that the paper does release new assets.
Researchers should communicate the details the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc.
The paper should discuss whether and how consent was obtained from people whose asset used.
At submission time, remember to amonymize your assets (if applicable). You can either create anonymized URL or include an anonymized zip file.
14. Crowdsourcing and research with human subjects
Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well details about compensation (if any)?
Answer: [NA]
Justification: This paper does not involve crowdsourcing or research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Including this information in the supplemental material is fine, but if the main contribu- tion of the paper involves human subjects, then much detail as possible should be included the main paper.
According to the NeurlPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector.
15. Institutional review board (IRB) approvals or equivalent for research with human subjects
Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?
Answer: [NA]
Justification: This paper does not involve crowdsourcing or research with human subjects.
Guidelines:
The answer NA means that the paper does not involve crowdsourcing nor research with human subjects.
Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper.
We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere the NeurIPS Code of Ethics and the guidelines for their institution.
For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review.
Declaration LLM usage
Question: Does the paper describe the usage of LLMs if is an important, original, or non-standard component of the core methods in this research? Note that if the LLM is used only for writing, editing, or formatting purposes and does not impact the core methodology, scientific rigorousness, originality of the research, declaration is not required.
Answer: [NA]
27

---

The core method development in this research does not involve large language models (LLMs) as any important, original, or non-standard components.
Justification:
Guidelines:
The answer NA means that the core method development in this research does not involve LLMs as any important, original, or non non-standard components.
Please refer to our LLM policy for what should or should be described.
28


Reviews:
[{"review_id": "n8nL6MKIGg", "reviewer": "Reviewer_jK1G", "summary": "This paper addresses the problem of verifying verilog circuits by conjecturing\nproof certificates using a neural network. Prior work has shown acceleration of\nliveness properties by having a neural network conjecture a measure of progress\n(a ranking function.) The key contribution of this work is to also predict\na safety invariants. These are then fed into a formal verification pipeline\nto assert correctness. The method of learning the neural network departs\nfrom other systems in that it uses a constraint solver, e.g. SMT, to\nset the neural network weights or prove that there exists no neural network\nthat satisfies a set of constraints. This enables smaller networks by using\nlinearly searching the space of neural networks. Finally, they show that\nthis method accelerates or is competitive with existing non-neural solvers.", "questions": "1. How was the architecture family selected?\n\n2. What are the limitations on the neural networks that can be used.\n\n3. Do you see a path towards learning to generalize to multi-task settings? i.e., taking the verliog as input and learning to interpolate over verliog programs?", "limitations": "yes", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "## Strength\n\n1. The domain of verilog verification is very important -- both historically\n   and particularly given the explosion in bespoke hardware designs for AI \n   acceleration.\n\n2. The provided speed gains seem non-trivial, particularly in a portfolio suite.\n\n3. The method produces much smaller networks, and actually provably the smallest\n   in the class explored, than a naive overparameterized model.\n\n## Weakness\n\n\n1. The largest weakest from my reading, and one that I'd appreciate more exploration\n   in a future draft, is the class of Neural Networks supported by both the synthesis\n   and verification queries. I particular, my understanding is the class of\n   non-linearitie is limited by the theories (efficiently) covered by the SMT\n   solvers.\n\n2. Relatedly, while interesting the counter example loop -- in the formal methods\n   literature an instance of CEGIS? -- implicitly relies on refuting smaller neural\n   architectures having sufficient capacity. This seems to work well in these benchmarks,\n   but may catastrophically fail for larger problems.\n\n3. As a minor criticism, I disagree with the discussion around quantization --\n   namely that the quantization need not be learned. In an information\n   theoretic sense, the optimal quantization is necessarily dependent on the\n   input distribution and downstream arithmetic circuit. Fixing the quantization\n   a-priori necessarily loses expressivity. That said, I think the advantages\n   for fitting into SMT theories might outweigh the downsides.", "was_revised": true, "final_justification": "I've maintained my score. The main criticisms raised through the review process seem to be (i) the lack of expressiveness of the target class of NN (ii) the learning procedure (iii) the subtle restriction of verilog programs\n\nI think (i) and (ii) while restrictions, point more to future directions and opportunities than failings of the paper. (iii) is indeed a failing and I would encourage the authors to better address, e.g., in an appendix, but it is not severe enough for me to lower my score.", "rebuttal": "The reviewer correctly notes that our work is restricted to neural networks with rectified activation functions—a choice that is common in both machine learning and verification literature. In our context, this design is specifically motivated by the need to encode networks into efficient (linear) theories of SMT solvers. We will expand on this important point and provide the details of our symbolic encoding in the revised version.\n\nWe confirm that our approach is indeed an instance of a CEGIS loop. As with most CEGIS-based best-effort methods, there remains scope for tackling more challenging problems—an open direction for future research.\n\nThe question of whether the appropriate quantisation should be learned is an important one, relevant to all approaches that employ quantised neural networks. In our case, the learning procedure produces networks with integer coefficients, reducing the quantisation to simply estimate the maximum range (and not the minimum precision), which is a significantly simpler quantisation task than in the general setting—and notably simpler than in cognate work such as neural model checking (NeurIPS’24).\n\nQ1. Our architecture family was specifically designed to balance trainability and verifiability, leveraging efficient SMT theories—namely, Linear Integer Arithmetic (LIA/MILP) for training and Bit-Vector (BV) theory for verification. As noted above, we will provide further elaboration on this point in the revised version.\n\nQ2. As such, while the general approach of training neural certificates as invariants  applies in principle to every feed-forward architecture, the algorithm based on SMT that we presented in this paper benefits from network families that have rectified activation functions (sign and ReLU) and discrete values domains. \n\nQ3. Our approach, which learns from system executions, is designed for single-task, unsupervised settings. Whether it can be generalised to support transfer learning across tasks remains an open question for future work—one that would require more than a straightforward extension of the work presented in this paper."}, {"review_id": "RKEEMG13x7", "reviewer": "Reviewer_Z4tK", "summary": "The paper presents a new approach for proving safety and liveness of reactive systems, where the proofs are represented using neural networks. The results build on recent results, including [56,57], which address temporal model checking and liveness verification, respectively. In this paper, reactive systems can be construed as state-transition systems, which admit variables and that transition relations, set of initial states, etc. are described symbolically (for instance, by means of SMT formulas). The proof techniques adopted in the paper are in fact standard in the verification literature. To prove safety, one establishes a program invariant. To prove liveness, one provides a ranking function. The authors prove the two properties at the same time using the notion of \"partially\" ranking function: the proof rules (5) - (7). In this paper, the authors propose to represent such a partially ranking function as a neural network (i.e. a \"neural certificate\"). Neural certificates are not new, as the authors also describe in Section 5, but the paper is the first time when they are employed for partially ranking functions. The authors then propose a new learning algorithm for inferring neural certificates, which are curiously not based on standard ML machinery, but based on SMT solvers. In fact, the SMT-based learning algorithm is reminiscent of CEGAR-based formula synthesis that exploits constraint solvers. The connection between neural certificates and SMT solvers lies in the well-known fact that neural networks (with ReLU activation functions) can be translated into MILP (Mixed Integer Linear Programming), which can in turn be solved by most SMT-solvers. \n\nIn the implementation and experiments, the work assumes a SystemVerilog input, which consists of a program and a property to verify. The implementation combines many existing tools including SPOT to convert an LTL formula into an automaton, EBMC to convert SystemVerilog program into SMT over bitvectors, bitwuzla to solve SMT over bitvectors, and Gurobi to solve MILP constraints. Experiments are conducted on an extension of prior benchmarks from [57], which includes both safety and liveness properties. In total, this is a 634 task suite. The authors report highly encouraging experimental results, in particular outperforming existing symbolic approaches on safety-liveness properties.", "questions": "Please respond to what I mentioned above seem to be weaknesses of the paper.", "limitations": "Yes", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 2, "significance": 2, "originality": 3, "strengths_and_weaknesses": "Strengths:\n- the paper attacks an important problem in verification\n- the use of neural certificates for the first time for safety-liveness properties\n- CEGAR learning algorithm to infer neural certificates that exploits SMT solvers\n- positive experimental results showing competitiveness of the technique\n\nWeaknesses:\n- Benefits of neural networks are unclear, upon further reflection. \n- Restrictions in the allowed programs by the proposed approach are unclear. \n\nLet me elaborate more on what I perceive as weaknesses of the paper; the authors should address these during the rebuttal. Firstly, the main benefit of neural networks is the existence of backpropagation algorithms that use gradient descent. This is not used in the paper, which opted to \"train\" the neural networks using constraint solvers instead of gradient descent. The authors position the contribution of the paper as \"using neural networks as proofs\". Since we know that neural networks can be seen as MILP formulas, it seems that the entire approach can simply be seen as CEGAR-based formula synthesis (by using SMT-solvers as oracles) and one can dispense of neural networks from their approach. This raises the questions of relevance of the paper to an ML conference.\n\nSecondly, the authors were not very clear in the definition in the preliminaries (Section 2) of what kind of variables are allowed in the programs, and what kind of data types and operations are allowed. There are hints on these in Section 3 and Section 4, based on results and tools that are used to translate from SystemVerilog to neural networks. That is, the programs use bitvectors, but for example no arrays, strings, etc. It would be good if the authors provide more details on the limitation of their approach. What type of programs can your approach handle in theory?\n\nFinally, the paper did a reasonable job in explaining basic concepts in formal verification for an ML conference. That said, there are a few definitions that the authors forgot to define (e.g. MILP).", "was_revised": true, "final_justification": "During the rebuttal, raised limitations were acknowledged by the authors. Since such neural certificate could still be represented efficiently by SMT formulas, it's still unclear to me the advantage of the neural representation. For these reasons, I've decided to keep my original score.", "rebuttal": "The reviewer highlights two central aspects of our work, which we will emphasise in the revised version.\n\nFirst, it is indeed correct that one of the main advantages of neural networks is their compatibility with gradient descent—an aspect we do not exploit in this work. However, this is not the only benefit neural networks offer. They are powerful representations of non-linear functions, independent of the training algorithm used. Our work hands down leverages this representational power. We have shown that our architecture is an appropriate representation for invariant and ranking functions on a standard benchmark. And most importantly, our ablation study has shown that linear functions are insufficient.  It is the use of neural networks to effectively represent non-linear invariant and ranking functions that allows our method to dominate the state of the art.\n\nSecond, the reviewer is correct in noting that our method is limited to systems where the number and size of variables are known a priori. Our method does not directly extend to arrays and strings of parametric length, or to dynamic data structures, being specifically tailored to hardware and embedded software that does not rely on stack or heap memory. Extending it to general-purpose software presents significant challenges and represents an important direction for future research.\n\nFinally, we appreciate pointing out the lack of certain definitions, which we will expand upon in the revised version."}, {"review_id": "BngnbLjn5k", "reviewer": "Reviewer_MKHH", "summary": "This paper presents a novel approach to model checking of reactive systems against full linear temporal logic (LTL) specifications. Unlike prior neural methods, which were limited to proving liveness properties via learned ranking functions, this work introduces a unified neural certificate that simultaneously encodes inductive invariants (for safety) and ranking functions (for liveness).\n\nThe key innovation lies in training these neural certificates using constraint solving, rather than gradient descent, and verifying their correctness via a single symbolic check. The authors demonstrate that their method is sound, scalable for many practical tasks, and significantly outperforms both prior neural model checkers and established symbolic model checking tools on an extended benchmark suite.", "questions": "- How does the method handle specifications where the Büchi automaton for ¬Φ is very large or nondeterministic? Can the approach scale symbolically in that case?\n- Would your method benefit from hybrid approaches (e.g., warm-starting with gradient descent and refining with constraint solving)?\n- How do you plan to scale your method to train large networks specifically how you use the solver efficiently?", "limitations": "yes", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 3, "significance": 3, "originality": 3, "strengths_and_weaknesses": "Strengths\n-----------\n - Clear Technical Innovation: The central idea—joint learning of safety and liveness proofs using a unified neural network—is novel and well-motivated. Prior work addressed liveness only; this paper closes that critical gap.\n - Soundness Preserved: Despite using machine learning components, the approach guarantees formal soundness through symbolic verification. The combination of logic-based training and model checking is elegant and rigorous.\n - Strong Empirical Performance: On a comprehensive 634-task benchmark, the method outperforms five decades of symbolic model checking techniques in many categories, especially for properties combining safety and liveness. Reported speedups (up to 10⁴×) are significant.\n\nWeaknesses\n---------------\n - Scalability Limits of Constraint Solvers: Although the paper reports excellent performance on the benchmark suite, it does not address how the constraint-solver-based training will scale to systems with large state spaces or complex invariants. Solvers tend to struggle with large, nonlinear constraint encodings—this bottleneck should be discussed more explicitly.\n- Baseline selection: The evaluation is strong, but lacks a direct comparison with the most recent symbolic checkers such as rIC3 (https://arxiv.org/html/2502.13605v1). It's unclear whether the proposed method would retain its performance advantage in those cases.\n - Assumes Büchi Automata Are Given: The approach assumes that the violation automaton for ¬Φ (a nondeterministic Büchi automaton) is already constructed. This step can be a significant practical hurdle, especially for real-world LTL specifications.", "was_revised": true, "final_justification": "Thanks for the rebuttal. I will keep my score as is.", "rebuttal": "Q1. Our method handles specifications whose corresponding automaton is non-deterministic by allowing counterexample transitions to be generated along all possible branches of the automaton. Regarding the question of whether we experimented with large specifications, we note that in most practical cases, industrial specifications are composed of lists of relatively small temporal logic obligations; see, for example, \"Toward Liveness Proofs at Scale\" (CAV 2024). Our work aligns with and captures this standard scenario.\n\nQ2. Our method would not benefit from warm-starting the constraint solver using gradient descent, for the simple reason that the solvers we employ neither require nor expect an initial value. Assessing whether our approach could benefit from warm-starting would require integrating alternative solvers—a direction that falls outside the scope of this manuscript but is indeed a very good suggestion for future work.\n\nQ3. Our method indeed benefits from using compact neural networks, and our experiments show that such models are sufficient in practice on a standard benchmark. In fact, our approach explicitly searches for the smallest network possible for a given benchmark, since (as the reviewer points out) constraint solvers tend to struggle with very large problem instances. In this paper, we argue that the key to scalable verification with neural certificates lies in using small networks, rather than scaling verification algorithms to handle large networks. That said, we acknowledge that for other verification tasks, scaling to larger networks might prove more effective. Exploring this trade-off is an important direction for future research on neural certificates.\n\nFinally, we thank the reviewer for suggesting rIC3. We have evaluated the publicly available “16‑threads Portfolio rIC3” implementation (github.com/gipsyh/rIC3). On tasks that are easy for most tools, rIC3 outperforms other symbolic approaches, consistent with the authors’ own evaluation. However, on harder instances, the performance gap narrows, and rIC3 aligns with other symbolic tools; in fact, for 40% of tasks, nuXmv outperforms rIC3. Nevertheless, overall—and especially when viewed on log-scale cactus plots—our method remains the clear winner outside of pure safety verification. All statistics comparing our tool against the best-performing tools run in parallel change by at most 3 percentage points, leaving our conclusions unchanged. As NeurIPS'25 rebuttal policy precludes the inclusion of new figures, we will provide the updated experiments only in the revised version of the manuscript."}, {"review_id": "EZniZQIrW8", "reviewer": "Reviewer_3nK8", "summary": "This paper introduces a novel extension to neural model checking by enabling neural networks to serve simultaneously as inductive invariants (for safety verification) and ranking functions (for liveness verification). The authors propose a unified neural certificate architecture—called a partially-ranking function—that classifies reachable states (safety) and ranks their progress toward satisfying liveness properties. Unlike prior work that uses gradient descent, this approach leverages constraint solvers (e.g., SMT, MILP) for training, improving both correctness guarantees and computational efficiency.\nThe authors demonstrate the practicality and effectiveness of the method through extensive experiments on 634 benchmarks from SystemVerilog designs, showing up to big speedups over both traditional symbolic model checkers and previous neural approaches, especially for combined safety-liveness verification tasks.", "questions": "Can the authors elaborate on the frequency and nature of solver errors encountered during experiments? Would fallback strategies be practical or recommended?\n\nDo the authors foresee limitations in applying this to software model checking, such as pointer-based memory or concurrency?\n\nThe architecture is piecewise-linear and intentionally simple for SMT compatibility. How expressive is it for more complex invariants/rankings?\n\nIn cases where the neural certificate fails to converge, how does one determine whether the issue is with architecture capacity, undersampling, or unsatisfiability of the spec?", "limitations": "Future work could strengthen solver diagnostics and scalability to more diverse systems.", "rating": 5, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": 3, "clarity": 4, "significance": 4, "originality": 3, "strengths_and_weaknesses": "Strengths \n\n- The paper presents a robust and formally grounded method that advances the frontier of neural formal verification. The constraint-based training of partially-ranking functions is innovative and mathematically sound.\n- The paper is well-structured and includes motivating examples, mathematical formulation, and diagrams that effectively communicate the ideas.\n- The approach addresses a critical gap in existing neural model checking, namely the inability to reason about safety properties, and brings it to parity with classical model checking tools.\n- The unification of safety and liveness certificates into a single neural network and the replacement of gradient descent with SMT/MILP solvers are novel contributions.\n\nWeaknesses\n\n- Although the authors scale to realistic hardware designs, it remains unclear how well the method generalizes to larger or more complex systems\n- The method depends heavily on solver behavior and issues like solver unsoundness or numerical instability are not deeply analyzed", "was_revised": true, "final_justification": "I am fine with the authors' answer and will maintain my score.", "rebuttal": "Q1. We thank the reviewer for suggesting a failure analysis. After re‑running the pure‑liveness suite, we found the failure causes to be as follows: 18 % were numerical mismatches between Gurobi’s solution and our NumPy sanity check; 39 % gave “model infeasible’’ reports for every architecture explored by our‑auto (we consider between zero to five hidden neurons); 21 % were segmentation faults; 7 % exited complaining that the MILP exceeds our size‑limited licence; and 14 % were time‑outs. We will report the failure analysis for the entire task suite in subsequent versions.\n\n\nIn total, across all benchmarks, Gurobi fails 98 times out of 634 tasks. We note that our method already includes a fallback strategy. A simple two‑solver portfolio—launching a sound solver in parallel (e.g., Z3) and considering the first solver to finish the entire task—rescues 59 of these 98 cases within the time cap with Z3. Fig. 4(c) shows the improvement possible from a four-solver portfolio through the Best curve. We will incorporate these numbers and emphasise the portfolio fallback strategy in the revision.\n\nQ2. Our method learns ranking functions and inductive invariants from data, relying on knowledge of the number and types of allocated variables. This assumption is specific to hardware and, in many cases, to embedded software. Generalising our approach to software with dynamic memory allocation as well as concurrency would require the use of compositional proof rules. This challenge applies to all certificate synthesis methods—not just neural approaches—and represents a compelling direction for future work.\n\nQ3. As correctly noted, our architecture is piecewise-linear—a design choice that ensures compatibility with linear theories within SMT solvers. In theory, our architecture could represent any invariant or ranking function over a finite state space by effectively encoding a large look-up table. However, this is clearly impractical except for trivial cases. The more relevant and open question is what can be expressed succinctly—that is, with a small number of neurons. This remains an intriguing direction for future research on neural certificates.\n\nQ4.Our method distinguishes undersampling from the other two failure cases. Specifically, when the learner succeeds but the checker returns a counter-example, we add it to the training set for the next learn-check iteration, mitigating undersampling. Otherwise, if the learner fails—and assuming the learner is complete—we can infer that either the network architecture lacks sufficient capacity or the specification is unsatisfiable. In this case, our algorithm increases the network size, and this scenario arises in our experiments. In principle, we could eventually distinguish between capacity limitations and unsatisfiability. In the worst case, we would enumerate all possible states (which are finite) and construct a network large enough to function as a look-up table, represented as a large piecewise-linear function. However, distinguishing capacity limitations and unsatisfiability with this approach is only practically feasible for trivial verification tasks before hitting the timeout."}]

Author rebuttal:

Meta-review: This work proposes a neural network certificate for proving the safety and liveness of reactive systems, where the neural network aims to learn a partial ranking function. The proof techniques (e.g., invariants and ranking functions) themselves are classical, but the work is the first to demonstrate that the partial ranking functions can be represented and learned via a neural network for an LTL specification. The evaluation is based on practical SystemVerilog verification problems, and a test suites with a large number of instances were demonstrated with promising results. Overall, the contribution of this work is novel and above the bar for NeurIPS publication.

One limitation of this work is the use of SMT/MILP solver to deal with neural network certificates, which inherently limits the neural network size and complexity. I suggest that the authors look into the tools developed by the neural network verification community, such as the tools proposed in VNN-COMP (https://arxiv.org/abs/2412.19985), which should provide significantly better scalability to further enhance the practicality and scalability of this work.

The use of a constraint programming solver in the learning approach is potentially another limitation, although it can work better on smaller-scale problems. Recent works in neural certificates, such as https://arxiv.org/pdf/2404.07956 and https://arxiv.org/pdf/2506.01356 have moved away from constraint programming and SMT for trading off scalability. I hope the authors can consider these factors in their future work.
Decision: Accept (poster)