Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators

SMT solvers like Z3 and cvc5 answer "is this logical formula satisfiable?" and sit under symbolic execution and program verification, so a bug in one silently corrupts everything built on it — but the solvers keep gaining new features faster than test generators can follow, and asking an LLM to write test formulas directly makes about half of them syntactically invalid while costing a fortune in LLM calls; this paper (Nanjing University — Maolin Sun, Yibiao Yang, Yuming Zhou) presents Once4All, which pays the LLM once to read the docs and write reusable formula generators, then fuzzes cheaply by dropping their output into skeletons taken from real formulas — finding 45 bugs in Z3 and cvc5, 40 already fixed.

The argument in one glance

Problem

SMT solvers keep gaining features faster than their testers can follow

A Satisfiability Modulo Theory (SMT) solver answers a deceptively simple question: given a logical formula over background theories like arithmetic, bit-vectors, strings, or sequences, is there an assignment of values that makes it true? Tools like Z3 and cvc5 are the workhorses behind symbolic execution engines (such as KLEE), automated program verification, and network and language analysis — they sit on the critical path, so a bug in a solver silently corrupts every tool built on top of it, sometimes into security vulnerabilities. That makes testing them essential, and testing means feeding them high-quality formulas that exercise their logic and expose disagreements or crashes. The hard part is that solvers are moving targets: the SMT-LIB input language keeps evolving (version 2.7 added polymorphic sorts and higher-order functions; version 3 is planned), and individual solvers add their own extended theories (cvc5 has Bag, Set, and Sequence theories, often only informally documented). Older test generators, tuned to earlier solver versions, cannot keep pace with these new features — which are exactly where fresh, untested bugs hide. So the challenge is generating test formulas that are always valid, deeply varied, and current with whatever the solver just added.
What people did

Enumerate from a grammar, mutate old formulas, or ask an LLM to write them

Three families of SMT fuzzers exist. Generation-based tools (like ET) enumerate formulas from a predefined grammar or rules. Mutation-based tools (like OpFuzz, which mutates operators, or HistFuzz, which reuses historical bug-triggering formulas) take existing formulas and change them to make new ones. And, most recently, LLM-based tools (like LaST, a retrained model, or Fuzz4All) prompt a large language model to write complete SMT formulas directly. Each tries to produce inputs that reach deep, buggy solver states, differing in whether they build from scratch, mutate seeds, or ask an LLM.
Why it fell short

Fixed rules miss new features; direct LLM generation is invalid and costly

Each family breaks on the moving-target problem. Generation- and mutation-based tools rely on hand-written grammars and mutation strategies, so when the SMT-LIB standard or a solver adds a feature, someone must manually update the tool — slow, effortful, and always lagging behind the new, bug-prone features. LLM-based tools promise to close that gap, because an LLM can read documentation and improvise formulas for new theories, but they bring two serious problems of their own. First, quality: roughly half of the formulas an LLM writes directly are syntactically or semantically invalid — malformed inputs the solver rejects outright, wasting the test and sometimes producing nonsensical bug reports. Second, cost: generating each formula means another round-trip to the LLM, so fuzzing (which needs to run at high throughput, many formulas per second) becomes dominated by slow, expensive model interactions. And there is a subtler gap: much of what makes a formula expose a bug is its structure — the quantifiers and logical connectives wrapped around the core expression — which theory documentation often does not even specify, and which a purely grammar-driven generator therefore cannot produce. What was missing was a way to get the LLM's ability to adapt to new features without paying its per-formula cost or its invalid-output rate, while still producing structurally rich formulas.
This paper's idea

Pay the LLM once to write generators, then fuzz cheaply into real skeletons

Once4All's move is to stop asking the LLM to write formulas and instead ask it, one time, to write generators — small programs that produce reusable terms (logical expressions). It works in two phases. First, LLM-assisted generator construction: the LLM reads the official SMT theory documentation (and informally-documented solver-specific extensions), extracts a context-free grammar (CFG) for each theory, and then synthesizes composable Boolean term generators that obey those grammars. Each generator is self-corrected — Once4All samples terms from it, checks them against real solvers, and feeds any errors back to the LLM to fix, iterating until the generator reliably emits valid terms. Crucially, this LLM work is a one-time investment, repeated only when the grammar actually changes; during fuzzing there are no LLM calls at all. Second, skeleton-guided mutation: Once4All takes real seed formulas and removes their small atomic sub-expressions, leaving behind structural skeletons — the quantifiers and logical connectives that shape solver behavior, with holes where terms go. It then fills those holes with fresh terms cheaply produced by running the synthesized generators, yielding new formulas that are syntactically valid by construction yet semantically diverse and structurally rich. Finally, it runs each formula through multiple solvers and compares — differential testing — flagging any crash or any disagreement (including checking extracted models) as a candidate bug. On Z3 and cvc5, Once4All found 45 real bugs, 43 confirmed and 40 already fixed by developers, while beating state-of-the-art fuzzers on code coverage.

Why this problem is worth solving

SMT solvers are trusted infrastructure that many other correctness tools stand on, so a hidden solver bug undermines everything above it.

An SMT solver is not an end-user application; it is a foundation. Symbolic execution engines call it to decide whether a program path is feasible, verifiers call it to prove or disprove properties, and network and language tools call it to check constraints. When such a solver returns a wrong answer — declaring a satisfiable formula unsatisfiable, or accepting an invalid model — every tool that trusted it inherits the error silently: a verifier might certify buggy code as correct, or a symbolic executor might miss a reachable, vulnerable path. Because these consequences are invisible and can become security vulnerabilities, the reliability of solvers like Z3 and cvc5 is disproportionately important relative to their size. And the only practical way to build confidence in a solver, short of full formal proof of the solver itself, is aggressive testing with formulas that probe its many theories and their corners. That is why better SMT fuzzing is worth real effort: a bug caught in the fuzzer is a bug that never silently corrupts a downstream verification. The difficulty, and the reason the problem is live, is that solvers keep growing new features that old testers do not know how to exercise.

The core realization is that the LLM’s value is in adapting to new features, and you should capture that value once rather than paying for it on every test.

The instinct with LLM-based testing is to let the model produce the test cases directly, one prompt per formula. But that couples two very different things: the rare, valuable act of understanding a newly documented theory, and the frequent, cheap act of emitting yet another formula. Doing both through the LLM means you pay the model’s latency and cost for every single test, and you inherit its roughly fifty-percent invalid-output rate on every single test. Once4All’s insight is to separate them. Understanding the theory — reading the docs, extracting the grammar, writing a correct generator for it — genuinely needs the LLM’s comprehension, but it only has to happen once per theory (or once per grammar change). Emitting formulas is then done by running the synthesized generator, a deterministic program that is fast and valid by construction. This is why the design is called Once4All: invest in the LLM one time, and reuse the result endlessly at fuzzing speed. It converts an ongoing, per-formula tax into a one-time setup cost, and it converts a probabilistic validity problem into a guarantee, because the generator is checked and self-corrected before fuzzing ever begins. Capturing the model’s adaptability in a reusable artifact, rather than re-invoking it constantly, is the crux.

What people did before, and where it broke

Generation-based fuzzing (enumerate from a grammar). Tools like ET generate formulas from predefined grammar or rules. Where it broke. Rigid rules limit diversity, from-scratch generation struggles to reach deep solver states, and the grammar must be manually updated as solvers evolve.
Mutation-based fuzzing (mutate seed formulas). Tools like OpFuzz mutate operators, and HistFuzz reuses historical bug-triggering formulas. Where it broke. Effectiveness hinges on hand-designed mutation strategies, and adapting them to newly introduced features takes substantial manual effort.
LLM writes formulas directly. LaST retrains a model and Fuzz4All prompts an LLM to produce complete formulas. Where it broke. About half the generated formulas are syntactically or semantically invalid, and generating each one requires another costly LLM interaction, so throughput collapses.
Grammar-only generation from documentation. Build generators strictly from what the theory docs specify. Where it broke. Documentation often omits structural elements like quantifiers that are critical to triggering bugs, so a purely grammar-based generator cannot produce them.
The gap. No approach combined the LLM’s ability to adapt to new features with cheap, always-valid, structurally-rich formula generation — capturing the model’s understanding once instead of paying for it per formula.

How Once4All works

From per-formula LLM prompting to one-time generator synthesis plus cheap fuzzing

↓ →
new
↓ →
new
↓ →
new
↓ →
new
↓ →
new

The idea

Generate test cases that are valid by construction and still diverse. Once4All’s generators are synthesized to obey each theory’s grammar and are self-corrected against real solvers before fuzzing, so the formulas they help build are syntactically valid rather than the roughly half-invalid output of direct LLM prompting — while composable term generation and varied skeletons keep them diverse. Solving the twin demand of a test generator for a complex language processor — every input must be well-formed enough to get past the front-end, yet varied enough to probe deep behavior — is the same problem the work on generating diverse and valid test cases for deep-learning compilers (NNSmith) covered elsewhere on this site tackles, using structure to guarantee validity without sacrificing variety. Once4All brings that validity-plus-diversity discipline to SMT formulas by grounding generation in grammar-conforming, self-checked generators.

Reuse real seed formulas to reach deep solver states. Rather than building every formula from scratch, Once4All keeps the structural skeletons of existing formulas — the quantifiers and connectives that steer a solver’s internal execution path — and mutates only the terms inside them, so its inputs land in the deep, feature-specific logic where bugs hide. Leveraging existing artifacts as seeds and mutating them to drive a system into hard-to-reach states, instead of hoping random generation stumbles into them, is the same seed-guided strategy the work on greybox fuzzing for concurrency testing (greybox fuzzing) covered elsewhere on this site relies on, steering exploration toward deep behaviors. Once4All’s skeletons are its seeds, preserving the structural context that documentation-driven generation would otherwise miss.

Cross-check independent implementations to expose wrong answers. Because a solver bug is often a silently wrong sat/unsat answer with no crash, Once4All feeds each generated formula to multiple solvers and treats any disagreement — or an invalid extracted model — as evidence of a bug, since correct solvers must agree on a formula’s satisfiability. Using multiple independent implementations of the same specification as oracles for one another, so that a divergence pinpoints a defect no single run could reveal, is the same principle the work on finding unstable code via compiler-driven differential testing (differential testing) covered elsewhere on this site is built on, turning agreement into a correctness check. Once4All applies this differential-testing oracle across Z3 and cvc5 to catch soundness bugs that would otherwise pass unnoticed.

Following a formula through Once4All

From a documentation page to a confirmed solver bug

A trace, drawn from the paper, of Once4All's one-time setup and its per-formula fuzzing loop.

Step 1 of 5

One-time: the LLM turns docs into a grammar

Once4All prompts the LLM with a theory's documentation — say cvc5's Sequence theory — and the LLM summarizes a context-free grammar for the valid expressions of that theory, covering even informally-documented, solver-specific operations.

This captures new or niche features that hand-written generators lag behind.

Why it works

Generators make validity structural, not probabilistic. Prompting an LLM per formula yields about half invalid outputs → but synthesizing grammar-conforming, self-corrected generators once → so the formulas built from them are valid by construction rather than by luck.
Moving LLM work off the fuzzing loop restores throughput. Per-formula model calls make fuzzing slow and expensive → but investing in the LLM one time and then only running generator programs → so fuzzing runs at high speed with no runtime LLM cost.
Skeletons from real formulas reach deep, bug-prone logic. Building formulas from scratch rarely hits deep solver states → but reusing the quantifier-and-connective structure of real seeds → so the inputs land in the feature-specific paths where bugs actually live.
Skeletons supply structure that grammars omit. Theory documentation leaves out elements like quantifiers → but harvesting those structures from existing formulas → so Once4All produces expressive inputs a purely grammar-based generator could not.
Differential testing catches silent wrong answers. A soundness bug can return a wrong sat/unsat with no crash → but cross-checking multiple solvers and extracted models → so a disagreement exposes the defect that a single solver would hide.

What it costs (trade-offs and scope)

The one-time LLM setup is real work and must be redone when grammars change. Extracting CFGs and synthesizing self-corrected generators takes LLM effort up front, and although it is amortized across all later fuzzing, it has to be repeated whenever a theory’s grammar evolves.
Self-correction reduces but cannot guarantee validity. The paper notes the self-correction loop makes generators reliably produce valid terms but cannot fully guarantee it, so a residual rate of invalid output can remain.
It depends on good seed formulas for its skeletons. The structural richness comes from skeletons carved out of existing formulas, so the diversity of reachable structures is bounded by the seed corpus available.
Differential testing needs multiple comparable solvers. The oracle works by comparing independent implementations (Z3 and cvc5); it flags divergences but still needs human confirmation of which solver is wrong, and bugs where all solvers agree on a wrong answer are harder to catch.
Results are measured on specific solvers and settings. The 45 bugs (43 confirmed, 40 fixed) and the coverage gains are on Z3 and cvc5 with particular theories and configurations; effectiveness on other solvers or under other setups may differ.

The comparison

Fuzzing SMT solvers to find bugs

Property	Grammar / mutation fuzzers	LLM writes each formula	Once4All
Adapts to new solver features
Syntactic validity
Runtime LLM cost
Structural richness
Bugs found (Z3, cvc5)

A comparison of ways to fuzz SMT solvers. Grammar and mutation fuzzers are valid but lag behind evolving features; asking an LLM to write each formula adapts to new features but produces roughly 50 percent invalid formulas at high per-formula cost. Once4All pays the LLM once to read documentation and synthesize self-corrected term generators, then fuzzes cheaply by filling skeletons taken from real formulas and differentially testing across solvers — finding 45 real bugs in Z3 and cvc5 (43 confirmed, 40 fixed) and beating prior fuzzers on coverage. Exact figures should be read from the paper.Underlined values explain themselves when clicked.

Where this stops working

What to keep in mind

This explainer is based on the paper’s full text (the authors’ arXiv copy, 2508.20340, of the ASPLOS 2026 paper). The described system is the paper’s: Once4All is an LLM-assisted SMT solver fuzzing framework that shifts from directly generating formulas to synthesizing generators for reusable terms. In a one-time generator-construction phase, it prompts an LLM to extract context-free grammars for SMT-LIB theories (including solver-specific extensions such as cvc5’s Bag, Set, and Sequence theories) from documentation, and to synthesize composable Boolean-term generators conforming to those grammars, then self-corrects each generator by sampling terms, validating them against real solvers, and feeding errors back to the LLM (the paper describes an iterative loop, e.g. up to ten iterations). In the fuzzing phase, it derives structural skeletons from seed formulas by removing atomic sub-expressions, fills the placeholders with terms produced by running the synthesized generators, and performs differential testing across solvers — flagging crashes, sat/unsat disagreements, and invalid extracted models as bugs (including soundness and invalid-model bugs). The headline results are from its evaluation on Z3 and cvc5: 45 real bugs found, 43 confirmed, and 40 fixed by developers, with higher code coverage than state-of-the-art fuzzers. The abstract states 43 confirmed bugs (40 fixed); the full text gives 45 found, 43 confirmed, 40 fixed. Background on SMT solvers, SMT-LIB, symbolic execution, and differential testing is standard context. The step-by-step walkthrough is an illustration of the described mechanism. Exact algorithm details, the self-correction procedure, and the full evaluation should be read from the paper. Once4All is described as a practical, extensible tool.

Background

Why testing critical infrastructure keeps coming back to valid inputs and cross-checked oracles

It helps to see Once4All within a long line of work on testing complex, correctness-critical software like compilers and solvers. Such systems share a shape: they accept a highly structured input language, they have deep internal logic that only certain inputs reach, and they must be correct because everything downstream trusts them. Testing them well means solving two perennial problems at once — generating inputs that are valid enough to get past the front-end yet varied and structured enough to exercise the depths, and deciding whether an output is right when there is no simple ground truth. The field’s recurring answers are exactly the two pillars Once4All leans on: build generation around the input’s grammar and structure so inputs are well-formed and reach deep behavior, and use independent implementations or invariants as oracles so wrong answers reveal themselves through disagreement. What is new here is using an LLM to keep the generator current as the input language evolves, capturing that adaptability once rather than paying for it per test. This drive to fuzz a complex, evolving system by respecting its message and program structure, rather than throwing random bytes at it, is the same terrain the work on multi-dimensional, message-guided fuzzing for robotic programs (message-guided fuzzing) covered elsewhere on this site occupies, using structure to make fuzzing reach meaningful states. Once4All’s particular contribution is to show that, for SMT solvers, letting an LLM read the docs once and synthesize reusable, self-corrected term generators — then fuzzing structurally via real-formula skeletons and differential testing — finds dozens of confirmed, developer-fixed bugs while staying cheap and valid.

If you remember only three things

1. SMT solvers like Z3 and cvc5 decide whether logical formulas are satisfiable and are foundational to symbolic execution and program verification, so a solver bug silently corrupts everything built on it — making thorough testing essential. But solvers are moving targets: the SMT-LIB language keeps evolving and solvers add their own (often informally documented) theories, and older grammar- or mutation-based fuzzers, tuned to earlier versions, cannot keep pace with the new features where bugs hide. Recent LLM-based fuzzers that prompt a model to write formulas directly can reach new features, but roughly half their formulas are syntactically or semantically invalid and every formula costs another slow, expensive LLM call.
2. Once4All stops asking the LLM to write formulas and instead asks it, one time, to write generators. In a one-time phase, the LLM reads theory documentation (including solver-specific extensions), extracts a context-free grammar for each theory, and synthesizes composable Boolean-term generators that are self-corrected against real solvers until they reliably emit valid terms. During fuzzing there are no LLM calls: Once4All carves structural skeletons from real seed formulas (keeping the quantifiers and connectives that steer solver behavior and that documentation omits), fills them with terms produced by running the synthesized generators — valid by construction, yet diverse and structurally rich — and then differentially tests the results across solvers, flagging any crash, sat/unsat disagreement, or invalid model as a candidate bug.
3. The design (captured in the name: invest in the LLM once, reuse it for all fuzzing) converts a per-formula LLM tax into a one-time setup cost and a probabilistic validity problem into a near-guarantee. On Z3 and cvc5, Once4All found 45 real bugs — 43 confirmed and 40 already fixed by developers — while beating state-of-the-art fuzzers on code coverage. The trade-offs: the one-time setup is real work that must be redone when grammars change, self-correction reduces but cannot fully guarantee validity, structural diversity is bounded by the seed corpus, and differential testing needs multiple comparable solvers and human confirmation of which one is wrong.

Check yourself

Check your understanding

1. Why is fuzzing SMT solvers both important and hard?
2. What two problems do recent LLM-based SMT fuzzers have that Once4All targets?
3. What is Once4All's core idea, and why is it called "Once4All"?
4. How does Once4All build effective test formulas and decide when it has found a bug?

Sources

The paper is “Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators” by Maolin Sun, Yibiao Yang, and Yuming Zhou (State Key Laboratory for Novel Software Technology, Nanjing University), published at ASPLOS 2026, DOI 10.1145/3779212.3790195. It is available on arXiv as 2508.20340.

This explainer is written from the paper’s full text (the authors’ arXiv copy). Once4All is an LLM-assisted SMT solver fuzzing framework that shifts from generating formulas directly to synthesizing generators for reusable terms. It prompts an LLM, one time per theory, to extract context-free grammars for SMT-LIB theories (including solver-specific extensions) from documentation and to synthesize composable, self-corrected Boolean-term generators; during fuzzing it derives structural skeletons from seed formulas, fills them with terms from the generators (no LLM calls), and differentially tests across solvers to flag crashes, disagreements, and invalid models. Evaluated on Z3 and cvc5, the paper reports 45 real bugs found, 43 confirmed, and 40 fixed by developers, with higher code coverage than state-of-the-art fuzzers. Background on SMT solvers, SMT-LIB, and differential testing is standard context. The numbers are the paper’s own; exact mechanisms and full results should be confirmed in the paper.