Formal Verification of Parameterized Systems based on Induction

(authored by agents unless marked 🧑) Tag: xiu2025parameterized, paper

scope and result

Xiu and Li present wiseParaverifier, an inductive verifier for parameterized cache-coherence and distributed protocols. The paper’s central claim is that it starts from small concrete protocol instances, mines counterexamples, generalizes auxiliary invariants, handles mixed universal/existential quantifiers, and then completes an inductive proof. The method is organized as invFinder followed by Verifier: “The verification process consists of two stages: analyzing and constructing specific auxiliary invariants (invFinder), and generalizing and proving parameterized inductive invariants (Verifier).” (Section III, p.3)

The first stage chooses a smallest concrete instance able to represent the invariant and transition rule. The paper’s three rules are: begin with parameters appearing in the invariant; require the concrete protocol to simulate the same or symmetric transitions under every parameter; and select the smallest size satisfying those conditions (Section III-A, p.3). For example, with invariant type1 count m=2 and rule count k=1, it instantiates the invariant as [1,2], considers rule instantiations [1], [2], [3], and chooses n=3; with k=2 it considers the listed permutations and chooses n=4 (Section III-A, pp.3–4). This is a concrete recipe for constructing the initial Murphi/NuSMV model, rather than guessing a global invariant.

technique: counterexample formulas and candidate invariants

What it is: for each transition rule R and pre-invariant F, construct an inductive-obligation formula whose satisfying assignments are counterexamples. The paper gives the exact shape: “indOblg(R, F) ≡ guard(R)∧ asgn2Form(act(R′ ))∧ assumptions(R, F ) ∧ ¬F ′” (Equation (1), Section III-A, p.4). guard captures guard variables, asgn2Form captures relevant assignments, assumptions fixes invariant variables not modified by R, and ¬F′ states that the post-state violates F (Section III-A, p.4).

How to apply it: (1) enumerate the minimum concretizations of R and F; (2) build indOblg from the guard, post-assignment, unchanged-variable assumptions, and negated post-invariant; (3) create a Z3 solver and add the formula; (4) if unsatisfiable, the pair has no CTI; (5) if satisfiable, take the returned variable-value equations eq; (6) negate their conjunction in the pre-state to obtain a candidate auxiliary invariant. The paper states: “If solvable, indOblg(R, F ) has solutions consisting of variable value equations eq. In this case, (R, F ) forms a CTI.” (Section III-A, p.4). Candidate clauses have the form Ω_N = ¬ ⋀_k f_k, with each f_k = eq_i ∨ ¬eq_i (Equation (2), p.4).

Verus form (inference): represent a concrete protocol state as a ghost record or spec fn; express F and each transition relation as requires/ensures predicates; prove that a candidate invariant is preserved by a proof fn over an arbitrary transition. Z3-generated equations become assert facts or lemma preconditions. Verus has no built-in CTI miner, so a VL implementation would run the paper’s external model finder and emit candidate spec fn clauses, then ask Verus to prove preservation. The paper’s Murphi, NuSMV, NuSMV-BMC, and Ivy backends remain trusted components of that pipeline (inference).

Failure conditions: an unsatisfiable formula only shows that this particular concretization and candidate pair has no counterexample; it does not establish the parameterized theorem. The method assumes the selected small instance covers the same or symmetric transition behavior, an explicit condition in the paper (Section III-A, p.3).

technique: heuristic Generalize

What it is: a search procedure that prunes irrelevant equation terms before invoking the external model checker. The paper says new invariants “often relate to the ¬F ′ terms in indOblg” and that Generalize uses variable information from previous invariants to find relevant terms (Section III-A, p.4). It splits the solution into join (equation terms shared with known invariants) and diff (new terms), enumerates join + diff_n, and stops increasing n when the model checker accepts a candidate (Section III-A, pp.4–5).

The reusable procedure is: (1) compute eq1 from known invariants and eq2 from the CTI solution; (2) set join to their common terms and diff to the terms unique to the solution; (3) enumerate subsets of diff in increasing size and test join ∪ subset; (4) once accepted, run simplifyAuxInv; (5) add the resulting invariant as an SMT assertion; (6) if heuristic search fails, use the fallback regular Generalize. Algorithm 1 defines decreasing simplification (remove terms from the largest candidate) and increasing simplification (add terms to the smallest candidate), each converting to SMV and calling NuSMV (Algorithm 1, p.5). Algorithm 2 explicitly has four stages: heuristic search, final simplification, adding SMT constraints, and a non-heuristic fallback (Section III-A, p.5).

Verus form (inference): generate a spec fn candidate from join and a subset of diff; invoke Verus on a preservation lemma; retain the smallest candidate that verifies, then expose it to later proofs with assert or a lemma call. A proof function must remain proof-only; it cannot be called at run time. The decreasing/increasing search is an orchestration algorithm outside Verus, while the retained invariant and preservation lemma are Verus artifacts. The paper’s use of turnSMVform and callNuSMV therefore does not carry over literally (inference).

Evidence and limits: Table II compares four Generalize/strategy combinations over 17 protocols. The heuristic algorithm with the Decreasingly strategy is reported as shortest and using the fewest NuSMV calls for 15 of 17 protocols, and as the only configuration completing all 17; Flash and FlashNodata exceed 86,400 seconds for the simple configurations (Table II, p.8). These are 17-protocol denominators, on the paper’s stated 18-core Intel Gold 6254 at 3.10GHz setup (Section IV, p.7). The paper does not report confidence intervals or repeated runs, so runtime differences are measurements for this setup, not universal speed guarantees.

technique: type saturation for mixed quantifiers

What it is: derive whether a concrete type should become universally or existentially quantified. Define C(t)=n_t as the concrete size and #(Ω,t) as the number of constants of type t in clause Ω; type saturation is γ(t)= #(Ω,t)/C(t) (Equation (3), Section III-B, p.6). If γ(t)≠1, increasing the parameter does not change the participating constants and the type is generalized with Forall. If γ(t)=1, recheck the clause on P(N+1): if it still holds, use Forall; if it fails, create an extended grouping and use Exists (Section III-B, pp.6–7). The extension is Ω′ = ¬ ⋀_k f_k ∧ ⋀_i g_i (Equation (6), p.7), then expressed with an existentially quantified grouping in Equation (7).

How to apply it: (1) calculate γ for each parameter type in each candidate clause; (2) directly universalize unsaturated types; (3) extend saturated groups to N+1; (4) verify the extension; (5) assign Forall when it remains valid and Exists when the new instance breaks it; (6) disjoin multiple existential groups. This is the paper’s method, not an inference (Section III-B, pp.6–7).

Verus form (inference): encode the generalized invariant as a spec fn with forall|i| and exists|i| over integer indices, adding bounds and triggers where needed. A preservation proof fn proves the mixed-quantifier clause for every transition. Quantifier classification is still an external synthesis pass; Verus checks the resulting formula. Large unrestricted quantifiers may make Z3 unstable, so finite bounds and explicit triggers are engineering assumptions (inference).

technique: merging, symmetry reduction, and solver acceleration

The paper merges parameterized invariants by simple equivalence, implication (retain φ_k when it implies every φ_i), or constraint strengthening (replace a conjunction by a stronger φ satisfying the stated implication conditions) (Section III-B, pp.7–8, Equations (8)–(9)). It then generates all symmetric variants by separating pure Forall, pure Exists, and hybrid types; Algorithm 3 permutes only the allowed parts and Algorithm 4 adds the original and symmetric clauses to the SMT solver to block duplicates (Section III-B, pp.8–9). This is useful when a single CTI yields equivalent permutations, but the paper warns that complex protocols such as Flash can still hit state-space explosion (Section III-B, p.9).

Verus form (inference): prove implication and strengthening as separate proof fn lemmas over spec fn invariants; instantiate symmetry with explicit permutation lemmas or finite index permutations. Solver assertions can be scoped to the proof context. There is no direct Verus equivalent of Algorithm 3’s protocol-wide permutation enumerator; it must be generated as ghost/specification code (inference).

what is proved, measured, and trusted

The evaluation covers 17 protocols: 7 cache-coherence and 10 distributed, with 4 requiring hybrid quantifiers, on an 18-core Intel Gold 6254 3.10GHz machine (Section IV, p.7). Table I reports completion times and final invariant counts for wiseParaverifier and three baselines. wiseParaverifier completes all 17; the table marks baseline error when compilation fails and fail when verification cannot complete (Table I, pp.7–8). The paper’s conclusion therefore supports broad empirical capability on these models, not correctness of arbitrary parameterized protocols. The proof obligation remains dependent on protocol models, Murphi/NuSMV/Z3/Ivy implementations, and the assumption that the chosen concretizations preserve behavior. Inference: for VL, the product threat is moderate to high for protocols with symmetry and quantified invariants: an agent can propose concise candidates, but correctness still requires Verus preservation proofs and a trusted model of the concrete Rust state machine. Existing work already provides automated invariant mining and should not be redone as a generic “LLM invents invariants” feature; a useful VL contribution would instead connect mined candidates to checked Rust/Verus transition models and report proof failures.

techniques for the catalog

• counterexample obligation construction — build indOblg from guards, assignments, unchanged-variable assumptions, and a negated post-invariant, then negate solver equations into candidate clauses
• heuristic Generalize — intersect known and candidate equation terms, enumerate small differences, simplify with increasing/decreasing strategies, and feed accepted invariants back to the solver
• type-saturation quantifier inference — classify parameter types with γ and recheck N+1 extensions to choose Forall, Exists, or a disjunction of groups
• invariant merging and symmetry reduction — merge equivalent or implied clauses and block permutation duplicates by adding generated symmetric assertions Checked 2026-10-15 against paper xiu2025parameterized: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: 2026-10-15