1 Introduction↩︎

Static vulnerability discovery on real C/C++ projects is a long-standing exercise in trade-offs. Industrial query engines such as CodeQL [1] produce reproducible findings but require the target to be built: an analyst chasing one bug in one demuxer typically stands up the entire toolchain — compilers, headers, flags, vendored dependencies, sometimes a CI environment — before a single query runs. Code-property-graph tools [2] share that auditability; Joern [3] relaxes the build requirement (its C/C++ frontend parses directly, using gcc only optionally for system headers), but CPG construction still gives the analyst no runtime/SMT-grade decision procedure for reachability. The compile-then-query cycle is what keeps declarative analysis a “minimum two-day commitment” for an unfamiliar target.

A second line of work asks whether LLMs can replace the building step. LLMs do help when paired with classical analysers [4] (good at inferring sources, sinks, sanitisers from documentation), but free-form use on whole codebases fails in two consistent ways. First, models confabulate — inventing function names, struct fields, or call relations that read plausibly but are not in the source. Second, they do not scale: parsers like FFmpeg [5] have hundreds of thousands of relevant facts and even a million-token window does not survive “read the codebase, find bugs” without the model losing track (we note that very recent frontier models addresses these issues well, with more cost per target). Recent benchmark work [6] shows ML-based vulnerability detectors trained at single-function granularity systematically over-claim recall: a function may be “buggy” only via how its caller invokes it. NeuroLog’s structural response is to restrict the LLM to per-function fact extraction and delegate cross-function reasoning to Datalog where it can be audited.

This paper explores a different split. We use an LLM only where it has a strong inductive bias — reading one C function and writing its dataflow as typed Datalog facts; reading a SAT model and emitting a Python program producing a plausible crashing input. Between those moments we use formal reasoners — Datalog [7] for cross-function composition and Z3 [8] for path-satisfiability. The analyst needs not to compiles the target: tree-sitter [9] parses incrementally, the LLM reads one function at a time, and Soufflé runs on the fact base directly.

We call the system NeuroLog. The combinations NeuroLog composes — “cheap static analysis narrows SMT” [10], [11] and “Datalog with SMT” [12] — are established prior art (§9). What we contribute is the assembly: a complete, compile-free vulnerability-analysis stack in which an LLM, a Datalog rule mesh, and an SMT solver each handle the part of the work the others are not good at, with the SMT model itself flowing into a downstream LLM crash synthesiser. Concretely:

• An LLM-as-fact-extractor design that removes the build step. Saturn, Pinpoint, SVF, CodeQL, and the Doop family all require a working compilation of the target — LLVM IR, Java bytecode, or a build-wrapper invocation. We replace the IR-lifting compiler with a function-by-function LLM that emits typed Datalog facts (Def, Use, ArithOp, Cast, Guard, FieldRead, Call). The LLM is constrained to the schema: it does not invent relations, only fill tuples. This is what keeps it honest at scale (§5).

• Datalog and SMT in a pipelined arrangement that complements rather than competes with Formulog’s intra-rule combination [12] Soufflé runs to fixpoint on the LLM-supplied facts and produces a finding catalog; a separate Z3 pass encodes, for each finding, only the def-use chain plus the path guards leading to it (Phase A). Phase B adds function summaries plus depth-bounded callee inlining for findings whose dataflow crosses a function call. Soufflé stays at full relational throughput; the SMT calls parallelise trivially over findings (Phase D); and the SAT model is exposed to downstream stages as an artifact rather than collapsed into a yes/no verdict. An optional likely-invariant pass [13] trained from a few corpus seeds further tightens ranges (Phase E2); every demotion is preserved in a secondary tier, never silently dropped (§5).

• Closed-loop crash synthesis from the SMT witness. For each SMT-feasible finding, a multi-shot LLM agent reads the SAT model, the chain of relevant facts, and a small file-format hint, and writes a Python program that produces a candidate crashing input. Inputs are validated against an AddressSanitizer harness [14]; on no-crash, the per-candidate ASan tail feeds back into the next round’s prompt. We calibrate this loop on stb_vorbis CVE-2023-45676 [15]: a 102-byte Ogg/Vorbis file that crashes the harness deterministically emerges in two iterations, with no fuzzer involved (§7). Saturn, Pinpoint, and Snugglebug [16] stop at “feasible / infeasible” — the witness flowing back into a generator is what NeuroLog adds.

• An honest catalogue of where each layer works and where it does not. We re-discover eight CVE-class issues across stb_vorbis, cJSON [17], FFmpeg, and curl (SOCKS + WebSocket) — including CVE-2023-38545 (CVSS 9.8) re-detected via a new project-specific rule — and surface five new memory-safety findings on libarchive [18] HEAD, together with their fixes (all accpeted to be merged in the repo). We document the misses (rule-mesh coverage gaps, the static FP that drove a five-attempt synthesis miss, untriaged FFmpeg flags) in §7 and §8.

The rest of the paper is organised as follows. §2 sketches the technologies the pipeline composes. §3 walks through a single stb_vorbis bug end-to-end; that example carries the narrative for the rest of the paper. §4 describes the pipeline; §5 fills in the phases. §6 reports implementation details. §7 presents the evaluation. §9 positions NeuroLog against neighbouring work and §10 closes.

2 Background↩︎

NeuroLog composes four bodies of work: declarative static analysis with Datalog, query-based vulnerability hunting, SMT-driven feasibility checking, and the recent literature on language models for code. We give just enough background here to make the rest of the paper self-contained; §9 returns to the same literature with a comparative lens.

2.0.0.1 Datalog as a static-analysis IR.

Andersen-style points-to analysis [19] can be written in a few hundred lines of Horn clauses, and a generation of declarative analyses — Doop on Java [20], bddbddb on context-sensitive queries [21], IFDS-style interprocedural distributive frameworks [22] — has shown that making the analysis declarative makes it auditable: every claim of the form “variable \(v\) at line \(\ell\) is tainted” is the conclusion of a derivation tree whose leaves are concrete facts from the program. Soufflé [7] synthesises C++ from Datalog rules and is the engine we use. The Datalog layer in NeuroLog has roughly 30 rules organised in five passes: alias, interprocedural taint, type-safety, memory-safety, and sink. The rules are not the main contribution of this paper; what is new is what feeds them.

2.0.0.2 Code property graphs and CodeQL.

The code-property-graph view [2] and QL [1] both give the analyst a query language over a unified abstract representation of program structure. They share Datalog’s auditability while emphasising graph reachability patterns. Their cost is the build step: producing the IR (CodeQL needs the project to compile under a special wrapper; CPG needs Soot or a comparable IR producer for the host language). NeuroLog is deliberately closer to the Datalog school in its reasoning layer and deliberately further from CodeQL on the front end — the LLM replaces the IR-lifting compiler.

2.0.0.3 Symbolic execution and SMT.

Tools such as KLEE [23] and SAGE-class whitebox fuzzers [24] demonstrate that a SAT-like back-end — usually Z3 [8] — can take a program, encode its execution along a path, and either find an input that drives the program down that path or prove no such input exists. The same machinery can be used post-hoc, on a specific finding rather than on a whole-program execution: encode the def-use chain and the path guards leading to a candidate bug site, ask Z3 whether the bug condition is reachable. This is what Phase A and Phase B of NeuroLog do– optimizing for the path depth, thereby scoping the path explosion. It is much cheaper than a KLEE-style symbolic exploration because the chain is bounded by the Datalog finding rather than by the program’s branching factor.

2.0.0.4 LLMs for static analysis.

Recent work — IRIS [4] is the closest in spirit on a specific part — shows that LLMs do well at the kinds of inference that classical static analysis is bad at: telling apart a sanitiser from a wrapper, guessing which function an unfamiliar API name is a clone of, reading documentation comments and inferring sources and sinks. NeuroLog leans on the same observation but moves the LLM below the rule mesh: rather than taking Datalog’s findings and rewriting the rules, we let the LLM populate the facts the rules consume. Because the LLM is constrained to a typed schema, and because Datalog itself ignores contradictory facts gracefully (a redundant Cast tuple is not a bug, only an inefficiency), the LLM’s mistakes show up as missing recall rather than as fabricated findings.

2.0.0.5 Likely invariants and runtime sanity.

Likely invariants in the sense of Sahoo et al. [13] are program properties that are observed to hold across a small number of normal-input runs — a counter never exceeds \(7488\), an error code is always \(0\). They were originally proposed as a fault-localisation aid; we use them as a precision filter on the SMT pass. The Daikon project [25] introduced a richer invariant language for the same purpose; we deliberately restrict ourselves to range invariants because anything more expressive degrades the “tier, don’t drop” guarantee we want over flagged findings.

2.0.0.6 Failure sketching.

Kasikci et al.’s Gist system [26] introduced an adaptive backward-slice approach for production-failure root-causing: start with a small slice around the suspect site, expand if necessary, and instrument only the locals the slice mentions. We adapt the slice-doubling idea (§5) for our LLM extraction budget — the analyst rarely wants to extract facts for every function in a codebase at once, and a doubled-radius slice gives a clean “stop when growth stalls” rule.

3 A motivating example↩︎

We illustrate NeuroLog on CVE-2023-45676 in stb_vorbis [15], [27]. The bug has two useful properties: the source fits on one slide and is obvious once shown, yet it took GitHub Security Lab a manual review to find and it remains unfixed in upstream master despite a 2+-year-old advisory. The interesting question is not whether the pattern is detectable automatically, but which of the obvious automation choices an analyst should reach for.

3.0.0.1 The bug.

Listing [lst:vorbis-bug] shows the relevant region. The function start_decoder parses the Vorbis comment-list header and allocates a string buffer per comment.

[language=C,basicstyle=\footnotesize\ttfamily,
                   numbers=left,numberstyle=\tiny\color{black!50},
                   firstnumber=3652,
                   escapeinside={(*@}{@*)},
                   xleftmargin=22pt,
                   float=tbp,
                   caption={\texttt{stb\_vorbis.c}, lines
                   3652--3676. \texttt{get32\_packet} reads
                   attacker-controlled bytes from the input
                   stream; \texttt{setup\_malloc} forwards to
                   \texttt{malloc}.  The product
                   \texttt{sizeof(char)\,*\,(len+1)} on line~3670
                   wraps to a small value when \texttt{len} is
                   close to \texttt{UINT32\_MAX}, the subsequent
                   loop on line~3673 then writes
                   \texttt{len}~bytes past the under-allocated
                   buffer.  ``\texttt{...}'' marks elided lines;
                   margin numbers track the true source.},
                   label=lst:vorbis-bug]
   len = get32_packet(f);                         /* taint source */
   f->vendor = (char*)setup_malloc(f, sizeof(char) * (len+1)); /* sink (alloc) */
   ...(*@\setcounter{lstnumber}{3659}@*)
   f->comment_list_length = get32_packet(f);      /* taint source */
   ...(*@\setcounter{lstnumber}{3663}@*)
   f->comment_list = (char**)setup_malloc(f, sizeof(char*) * f->comment_list_length); /* sink */
   ...(*@\setcounter{lstnumber}{3667}@*)
   for(i=0; i < f->comment_list_length; ++i) {
      len = get32_packet(f);                      /* taint source */
      f->comment_list[i] = (char*)setup_malloc(f, sizeof(char) * (len+1)); /* sink (alloc) */
      ...(*@\setcounter{lstnumber}{3672}@*)
      for(j=0; j < len; ++j) {                    /* OOB write    */
         f->comment_list[i][j] = get8_packet(f);
      }
   ...(*@\setcounter{lstnumber}{3676}@*)
   }

Two distinct failure modes in a 25-line region. Line 3664 multiplies an attacker-supplied 32-bit length by sizeof(char*), so a comment list of length \(2^{29}\) wraps a 32-bit size_t to zero. Line 3670 adds one to a 32-bit length, so len = UINT32_MAX produces a zero-byte allocation; the loop on 3673 writes UINT32_MAX bytes past it. Both rely on the same primitive: attacker-controlled u32 reaching an arithmetic operation whose result feeds malloc.

3.0.0.2 Why classical static analysis is awkward here.

The pattern is within reach of CodeQL or any CPG-based query — but both presuppose the project has been built into an indexable form. stb is a single-header library intended to be #included into a host project, so running CodeQL on the snippet requires finding or writing a host that uses stb_vorbis.c as a .c file, building under the CodeQL build wrapper, then writing the QL query and iterating. Each step is easy; the cumulative cost rules out opportunistic per-library checks.

3.0.0.3 Why a free-form LLM is awkward here.

A frontier LLM, asked to read stb_vorbis.c (about 5,000 lines) and find “integer-overflow bugs in allocation sizes,” will return an answer in seconds. The answer is variably correct: in our experiments the model would sometimes pick start_decoder immediately, sometimes pick a syntactically similar but semantically uninteresting site, and occasionally invent a bug at a line that does not exist. The deeper problem is not the model’s accuracy on a single prompt; it is that the model’s intuition does not compose. It gives no derivation, no auditable evidence, and no way to ask “would these inputs really reach this site under the i < f->comment_list_length guard?” Adding more files to the prompt strains working memory in ways that depend on prompt phrasing rather than program structure.

3.0.0.4 What NeuroLog does instead.

NeuroLog treats the LLM as a fact extractor over one function at a time. On start_decoder it produces:

  Def(start_decoder, len, 0, 3652)
  Call(start_decoder, get32_packet, 3652)
  ArithOp(start_decoder, 3653, _t, +, len, 1, "u32")
  Call(start_decoder, setup_malloc, 3653)
  ActualArg(3653, 1, size, _t, 0)

which a tree-sitter pre-pass complements with structural facts an LLM would be wasteful for (CFG edges, dominance, FormalParam, raw Call sites). Datalog rules then compose the facts across the function into a derivation that points at the bug (Figure 1).

TaintSourceFunc(get32_packet) composes with extracted Call/ActualArg/Def to produce TaintedVar(start_decoder, len, 3652); an ArithOp consuming that TaintedVar at the DangerousSink-tagged ActualArg of setup_malloc yields NarrowArithAtSink at line 3653, and the taint origin lifts it to the TaintedNarrowArith the report shows. None of these rules know what stb_vorbis is — they are the same rules used on cJSON and FFmpeg.

3.0.0.5 From finding to crash.

Phase A of the symbolic-execution back-end encodes len as a free 32-bit BitVec, walks the def-use chain back to its TaintSourceFunc origin, and proves the size argument at setup_malloc is attacker-controlled along a feasible path. NeuroLog hands that model, the def-use chain, and the local snippet to a synthesis agent that knows Vorbis via Ogg — the capture_pattern 0x4f676753, VORBIS_packet_comment, etc. Its first witness sets \(\texttt{len} = \texttt{0xFFFFFFFF}\), but sizeof(char) * (len+1) wraps to a zero-byte allocation that does not fault; the ASan no-crash tail feeds back, and the second witness sets \(\texttt{len} = \texttt{0x7FFFFFFF}\), whose size argument (computed in 64-bit size_t) is a \(\sim\)​2 GB request. The agent emits a Python program writing a 102-byte file. Fed to an ASan-instrumented harness, ASan reports allocation-size-too-big at line 3653.

3.0.0.6 The total cost.

On a 5-CPU laptop: tree-sitter scans the whole stb codebase in \(<\)​1 s. The LLM extracts \(\sim\)​30 functions on the backward slice from setup_malloc in 37 s (Lite-tier model, parallel over functions). Soufflé takes \(\sim\)​2 s, SMT \(<\)​1 s, synthesis converges in two LLM iterations and \(\sim\)​5 min wall time (mostly network round-trips). End to end the experience is closer to a CTF write-up than a CodeQL pipeline.

4 Architecture↩︎

NeuroLog is a six-stage pipeline. Each stage has a single responsibility and a single output that the next stage consumes, so the analyst can stop after any stage and get a useful artifact (a slice, a fact base, a Datalog finding catalog, an SMT-filtered finding catalog, or an ASan-confirmed crashing input). This essentially means that while NeuroLog has features of being used in autocopilot mode, it is designed for users (e.g. security researchers) to have a more interactive sessions based on their own understanding of the codebase. Figure 2 sketches the data flow and Table 1 maps each stage to its module, input, output, and design role. An optional Phase 0 recon front-end can precede stage 1 to widen what the sink-seeded slice would otherwise miss (§5); it changes no stage’s contract.

4.0.0.1 Tier-don’t-drop.

Each precision step in the pipeline can demote a finding, but no step ever silently drops one. When Phase E2 invariants demote a finding because its observed range excludes the bug condition, the finding is moved to a secondary tier with a back-pointer to the invariant that demoted it; when E1 dependence filtering classifies a finding as a downstream symptom of an upstream root cause, the back-pointer leads to the root. This matters operationally because the most interesting findings — attacker-controlled inputs the corpus never exercised — are precisely the ones the seed-driven invariant pass would otherwise mute. We make this deliberate calibration choice in two places: §5 documents how each pass exposes its tier metadata, and §7 reports the tier breakdowns alongside the headline numbers so a reader can re-tier the data with their own tolerance.

4.0.0.2 Why six stages and not three.

A simpler architecture would collapse stages 1 + 2 into “LLM reads the codebase” and stages 4 + 5 + 6 into “LLM produces crashing inputs.” We tried both ablations during development and report them honestly in §7: the collapsed extractor loses the structural-fact floor and confabulates; the collapsed synthesiser loses the SAT-model anchor and produces blobs that are fluent but rarely reach the bug site. The six-stage decomposition is what keeps the LLM honest at the boundaries the rule mesh expects.

5 Methodology↩︎

This section walks through each stage in detail, using the same running example as §3: the stb_vorbis comment-parsing region of start_decoder (CVE-2023-45676).

5.1 Stage 0 — recon (optional front-end)↩︎

The backward slice (§5.2) is anchored on a catalog of memory-safety sinks, so it never reaches functions that call no such sink — precisely where a large, growing class of bugs lives (connection-reuse credential leaks, incomplete validation, stale-state resets). The recon front-end closes that gap without abandoning the verifiability discipline. A (cost-wise) cheap LLM reads the target file plus its callers and emits two things: (i) additional seed functions that are merged into the slice, so policy/comparison/cleanup functions enter the fact base; and (ii) bug-class hypotheses, each paired with a concrete formal check (a Datalog rule sketch, an SMT constraint, or an ASan trigger). Recon proposes; it never judges: it may raise a class to investigate but only a fired-or-silent formal rule resolves one, and every hypothesis must carry a check or it is dropped. Recon (in-pipeline, cheap model) and the host interpretation loop (which runs the checks) communicate only through a persisted artifact, so the two never need to be co-present.

The enabling primitive is a semantic fact the smell pass emits, FieldSemantic(func, field, role) — “this function plays semantic role (compared / validated / reset / …) over this struct field.” This is the neuro-symbolic bridge in miniature: a syntactic extractor cannot know that Curl_timestrcmp(a->user, b->user) is a credential comparison without hardcoding every comparator name, but the LLM resolves name\(\to\)functionality and tags it role="compared". A small family of omission rules then proves, mechanically, that a handler exercising a role over \(\ge 2\) fields of a struct omits a security-relevant field the struct carries — e.g.a reuse comparator that never compares a credential, or a reset that leaves a secret stale. The rules are self-scoping (the “\(\ge 2\) fields” and “two struct instances” tests identify comparators with no hardcoded function list) and frame-driven (the struct’s own fields, from a syntactic struct scan, are the ground truth for what should have been handled). The LLM perceives; Datalog proves.

5.2 Stage 1 — slicing the function set↩︎

NeuroLog works on a backward slice from a small catalog of sinks: malloc-family allocators, memcpy and friends, FFmpeg bitstream readers, and libc string functions. Tree-sitter [9] parses the codebase incrementally and the call graph is built from identifier references inside function bodies. The slice is the set of functions reachable backward from any sink call site at depth \(\sigma\).

5.2.0.1 Why backward instead of forward.

A forward slice from the program’s entry point is open-ended on demuxer code where dispatch tables turn every public entry into every function. Backward from sinks, the slice is bounded by what Datalog will later query — dataflow can only matter if it touches a sink, and sinks are enumerable. The cost: forward-only paths via function pointers the call graph does not resolve are missed (§8).

5.2.0.2 Adaptive depth (E4).

The radius \(\sigma\) trades extraction cost against recall on deeply-nested wrappers. We use a \(\sigma\)-doubling heuristic [26]: compute the slice at \(\sigma\in\{2,4,8\}\) and take the smallest \(\sigma\) at which the growth-rate to the next falls under 5 %. On the FFmpeg demuxer subset this recommends \(\sigma{=}3\) (109/124/124 functions; 1.6 % growth at \(\sigma{=}4\)); on the small stb codebase the heuristic does not converge and the maximum is recommended. The output is a curation hint, not a hard filter.

5.3 Stage 2 — facts: mechanical floor + LLM smell pass↩︎

The fact base is the pivot: wrong facts cannot be recovered downstream; right facts let surprisingly modest Datalog rules surface real bugs.

5.3.0.1 Mechanical floor.

Tree-sitter contributes the structural facts an LLM would be wasteful for: FormalParam, Call sites, CFGEdge, dominance, basic-block heads. Deterministic and cheap; the LLM never overrides them.

5.3.0.2 LLM smell pass.

For each function in the slice the smell pass invokes a small “Lite-tier” LLM with the function source, line numbers, and an instruction to emit a JSON list of facts using a fixed schema. The schema is deliberately small (twelve relations) and security-aware:

Def(func, var, ver, addr)              ArithOp(func, addr, dst, op, src, operand, type)
Use(func, var, ver, addr)              Cast(func, addr, dst, src, kind, sw, dw, st, dt)
Call(func, callee, addr)               Guard(func, addr, var, op, rhs, polarity)
ActualArg(call_addr, idx, param, var)  FieldRead(func, addr, base, field)
ReturnVal(func, var, ver)              MemRead(func, addr, base, offset, size)
FormalParam(func, var, idx)            FieldWrite(func, addr, base, field, ...)

The prompt requires every emitted fact to be grounded in a specific source line: a fabricated ArithOp pointing at a line that contains no arithmetic must never appear. The fixed schema is the corrective constraint — the model cannot invent non-existent relations, and when unsure it omits, which the rule mesh handles gracefully (a missing Cast is a recall miss, not a false positive).

Figure 3 maps each relation to its producer: mechanical floor for structural facts, LLM smell pass for semantic ones a syntactic AST traversal cannot decide.

5.3.0.3 Concretely.

On start_decoder the smell pass emits, among many others, the facts shown in Listing [lst:vorbis-facts].

Call(start_decoder, get32_packet, 3652)
Def(start_decoder, len, 0, 3652)
Use(start_decoder, len, 0, 3653)
ArithOp(start_decoder, 3653, _t, +, len, 1, "u32")
Call(start_decoder, setup_malloc, 3653)
ActualArg(3653, 1, size, _t, 0)
Call(start_decoder, get32_packet, 3669)
Def(start_decoder, len, 0, 3669)
ArithOp(start_decoder, 3670, _t2, +, len, 1, "u32")
Call(start_decoder, setup_malloc, 3670)
ActualArg(3670, 1, size, _t2, 0)

The mechanical pass adds CFGEdge, FormalParam, and Call sites for any helpers reachable from this function.

5.3.0.4 Cost vs.recall.

On the stb slice (128 functions, 18.6 KLoC) the smell pass takes 36.6 s at $0.005 with a Lite-tier model and 15-way parallelism. The same slice with a frontier model extracting facts alone (no mechanical floor) takes 55 min at $0.30–$0.50 — \(90{\times}\) slower, \(70{\times}\) more expensive, and on bug-relevant functions equal recall (§7).

5.4 Stage 3 — Datalog rule mesh↩︎

The Datalog layer composes facts across functions in five passes — (i) alias, (ii) interprocedural taint, (iii) type safety, (iv) memory safety, (v) sink — with Soufflé’s stratified negation making the pass ordering explicit. The mesh is \(\sim\)​30 rules covering tainted size arguments, allocation overflow, sign-confusion casts, narrowing-cast at sinks, buffer-overflow in loops, double-free, use-after-free, NULL-deref of unchecked allocation, and unbounded counter-as-index. Each family is one or two relations composing dataflow facts in a single rule (Appendix 11).

5.4.0.1 Worked example.

The CVE-2023-45676 finding emerges as the conjunction of four relations. First, TaintSourceFunc(get32_packet) is in the catalog. Source taint propagates to TaintedVar:

TaintedVar(f, v, addr, "ret_from_get32_packet", "ret") :-
    Call(f, "get32_packet", addr),
    Def(f, v, _, addr).

which fires on the Def(start_decoder, len, 0, 3652) above. Standard taint propagation through arithmetic gives TaintedVar(start_decoder, _t, 3653, …) for the result of len + 1. The NarrowArithAtSink relation looks for arithmetic in a declared-narrow type that flows into a sink argument; combined with TaintedVar, it produces:

TaintedNarrowArith(f, ca, callee, dst, w, sign, risk, origin) :-
    NarrowArithAtSink(f, ca, callee, dst, arith_a, w, sign, risk),
    TaintedVar(f, dst, arith_a, origin, _).

That tuple is the report the analyst sees: start_decoder @ 3653, var=_t, narrow=u32, risk=alloc-size.

5.4.0.2 What the Datalog layer is not doing.

It is not deciding feasibility. The taint propagation is a may-flow over-approximation; only the SMT pass below decides whether a path is satisfiable. The split is by design: Datalog stays at full relational throughput (no SAT calls in rule bodies, in contrast to Formulog [12]); SMT stays per-finding and embarrassingly parallel (§5.5).

5.4.0.3 Closing the LLM-temporary gap (Pass 6).

On the libxml2 case study (§7.1) the agent identified a recurring extraction artifact: for an inlined size expression like xmlMalloc(lenn + lenp + 2), the smell pass emits an ArithOp with destination tmp (a synthetic name) but no Def or VarType on it, while ActualArg records the call’s argument as the literal expression string "lenn + lenp + 2" rather than a reference to tmp. The classical NarrowArithAtSink body joins through ActualArg.var\(\to\)ResolvedVarType.var\(\to\)ArithOp.dst, all three of which fail in this shape. Pass 6 (source_arith_sink_bridge.dl) closes the gap with one rule that joins ArithOp and Call directly when the call sits within two lines after the arith and the callee is on a small alloc-class whitelist (xmlMalloc family, av_malloc family, libc allocators). With fewer than thirty lines of Datalog, this resulted in bug detection in libXML2 (see §7.1).

5.4.1 On-demand Datalog queries during reasoning↩︎

The five-pass mesh runs once and produces a finding catalog the host agent reads. That alone is a batch architecture: the agent narrates verdicts from what the mesh materialised. What it adds is the ability to ask new questions of the same fact base during reasoning — “do other functions share this shape?”, “does this intermediate carry a ResolvedVarType?”, “which sister sites in the same module also fire?”. NeuroLog exposes the loop through a single on-demand Datalog tool.

5.4.1.1 The runtime.

neurolog__query_datalog accepts arbitrary Datalog source, a facts directory, the output relations to read back, and optional pre-derived relations to stage (ResolvedVarType, TaintedVar, BlockReach from a prior batch run as TSV CSVs). Soufflé runs in a temp directory with the original facts symlinked in (no copy of 200K-row corpora) and extras as <rel>.facts. The return is structured: ok (rows, capped at 500/relation), error (soufflé stderr plus a line-numbered echo of the rule text so file:line:col diagnostics align with the agent’s own source), timeout, or no_outputs.

5.4.1.2 What this changes.

The host agent’s role moves from “read CSVs, write verdict” to “read CSVs, hypothesise, query, refine, write verdict.” On the libxml2 case study (§7.1) the agent fired 19 ad-hoc queries in one investigation from a one-paragraph user prompt; two had schema mistakes that Soufflé rejected, the agent read the line-numbered echo, fixed them, and resubmitted. The prior-art lineage of “cheap static analysis narrows SMT” (Saturn, Pinpoint, Snugglebug) does not include this loop: those systems produce a finding list and ask SMT for a yes/no per finding. The reasoning agent with its own query tool over the finding list is what this paper adds (eval: §7.1).

5.5 Stage 4 — symbolic execution post-pass↩︎

For each Datalog finding \((\,f, \mathit{addr}, v, k\,)\), the symbex stage encodes the def-use chain leading to \(v\) at \(\mathit{addr}\) and the path guards along the way as a Z3 formula, asserts the bug condition for the bug class \(k\), and asks check().

5.5.0.1 Phase A — intra-procedural.

The encoder walks back from the use of \(v\) at \(\mathit{addr}\) to the most recent reaching def, encoding ArithOp on its inputs recursively, Cast (zero/sign-extension or truncation), and leaving Call return values free. Path guards are collected by walking forward from the last common ancestor in the CFG. For CVE-2023-45676: \(v=\texttt{\_t}\) at 3653 is ArithOp(+, len, 1); len at 3652 is taint-source-defined and left as a free 32-bit BitVec. The narrow_arith_at_sink assertion is len + 1 < len as 32-bit unsigned — satisfiable with len = 0xFFFFFFFF.

5.5.0.2 Phase B — function summaries + depth-bounded inlining.

When dataflow crosses a function call, Phase A’s free symbol misses information the callee provides — a validator returns 0 or 1, an allocator returns non-null, a bitstream reader returns at most \(2^k-1\). Phase B precomputes a small per-function summary (return-value range, write-set, predicate over inputs) and Phase B-2 inlines callee bodies up to depth \(d\) (default \(d{=}3\)) when the summary is not specific enough. Function-prefixed SSA keys prevent local-name collisions on inline.

5.5.0.3 Phase D — parallel verification.

Findings never share encoder state, so the work is naturally data-parallel: one worker per CPU, the FactStore loaded once per worker, findings dispatched in chunks (\(\approx\)​4 chunks/worker). On 378 ffmpeg-demuxer findings with four workers, wall time drops from 1.19 s serial to 0.60 s (\(1.98\times\)); on 260 mov-demuxer findings, \(2.55\times\). The 4–8-worker plateau is per-worker fixed cost (FactStore deserialisation \(\approx\)​50 ms, Python imports); pure Z3 scales linearly past it.

5.5.0.4 Verdict and SAT model.

check() returns sat, unsat, or unknown. Feasible findings carry the model (len_3652 = 4294967295, _t_3653 = 0, ...) which both accompanies the report and feeds the synthesis agent (§5.8). unsat findings drop to a secondary tier with a back-pointer to the excluding guard.

5.6 Stage 4b — likely range invariants (Phase E2)↩︎

Phase A and B see only the source; they do not see what values the program has actually held. Sahoo et al. [13] observe that 8–16 normal-input runs give tight range bounds on hot-function locals, usable as a fault-localisation aid. We use the same observation as a precision filter on SMT.

5.6.0.1 An optional dynamic extension.

This is the first point where NeuroLogruns the target rather than reading it, so it is worth being precise about what changes and what does not. Stages 1–4 are the static core: no build, and a complete tiered finding catalog out the other side. Stages 4b and 5 are an optional extension whose headline purpose is a reproducible proof-of-vulnerability — Stage 5 emits an actual crashing input, which unavoidably runs the code — and, having paid for a runnable target, Stage 4b reuses the same machinery to sharpen SMT ranges from observed values. Both go through a single artifact built once per target: an AddressSanitizer-instrumented executable taking one input file (often the project’s existing libFuzzer harness), at -O0 -g (Figure 2, stage 6). It is the only thing this extension compiles; the static core never does. Crucially, the extension can only re-tier findings, never erase them (tier-don’t-drop, §4): with no harness the analyst still gets the full static catalog; with one, recall is unchanged and only the ranking sharpens.

5.6.0.2 Mechanism.

The runtime data we need is what normal executions did at the Datalog-flagged program points. We collect it by running that harness on a corpus of valid inputs under GDB with a breakpoint at every (func, addr) in the finding catalog. A Python hook enumerates integer-typed locals via frame.block() and prints one INVfunc|addr|var|val| line per local. After the corpus pass we aggregate (min, max, n_obs) per tuple into LikelyRangeInvariant(func, var, addr, lo, hi, n_obs). encode_var(v, def_addr) asserts \(\mathit{lo}\le v\le\mathit{hi}\) when a matching invariant exists.

5.6.0.3 Two-tier matching.

Tier 1 is the exact triple (func, def_addr, var); Tier 2 widens to (func, *, var) (same variable anywhere in the function, union of observed ranges). Tier 2 compensates for compiler line-folding under -O0+. We deliberately do not accept a Tier 3 matching same-named variables across functions: that would import a length field from one parser as a bound on an unexercised attacker input in another, silently demoting exactly the findings an analyst wants to keep.

5.6.0.4 Engineering notes.

The harness must be -O0 -g; LSan must be off (LSAN_OPTIONS=detect_leaks=0, it doesn’t work under ptrace); multi-file projects read per_function_report.json so each breakpoint resolves against its actual source file. On the FFmpeg demuxer subset, three seeds (a 163-byte synthetic Matroska scaffold and two truncations of a real Matroska file) yield 245 invariants from 18 602 observations across 348 breakpoints. Phase B with invariants enabled demotes 13.2 % of the FFmpeg feasible set, including the matroska_parse_webvtt static FP that synthesis spent five attempts on.

5.7 Stage 4c — dependence filtering and parser progress↩︎

Two more lightweight precision passes attach to existing boundaries.

5.7.0.1 E1 — dependence filtering.

The catalog often contains downstream echo findings (a tainted index drives a finding at both the assignment and the sink). Sahoo et al.’s dependence clustering [13] groups by data-flow predecessor; we build a forward def-use graph keyed by (var, addr) and BFS-reach each finding’s source set. Findings whose source set is properly contained in another’s are demoted to a downstream_symptom tier with a back-pointer to the root. Tier annotation only — nothing is removed.

5.7.0.2 E3 — parser progress.

On no-crash, synthesis feeds the previous attempt’s ASan transcript back into the prompt. To focus the next round on how far into the parser the attempt got, we count distinct user-frame functions in the transcript (skip-list: main, LLVMFuzzerTestOneInput, libc) and add “previous attempt reached frames \(A, B, C\); aim deeper” to the next prompt.

5.8 Stage 5 — crash-input synthesis (Phase C)↩︎

Synthesis takes a Phase B-feasible finding plus its SAT model and asks an LLM agent to write a Python program producing a candidate crashing input. Multi-shot loop: \(N\) candidates per round (default \(N{=}3\)), each validated against the harness; on no-crash, the per-candidate ASan tail and parser-progress score feed the next round (Figure 4).

5.8.0.1 Prompt structure: \(P_c\) + \(V_c\).

We decompose synthesis into a path condition \(P_c\) (a working file-format prefix the parser accepts — Vorbis comment packet, MKV D_WEBVTT/SUBTITLES track header) and a vulnerability condition \(V_c\) (the constraint on the trigger variable at the bug site — e.g.the size argument (len+1) exceeds the allocator limit, satisfied at \(\texttt{len}\approx\texttt{0x7FFFFFFF}\)). \(P_c\) is handed to the agent as a scaffold of bytes not to disturb; \(V_c\) as an explicit “Target bug condition” section. The Python emitter is encouraged to produce a small scaffold mutation, not a from-scratch generator. COTTONTAIL’s Constraint/Flexible-Mask decomposition [28] solves the same split at concolic-execution time; we solve it statically.

5.8.0.2 Sanitizer harness as ground truth.

Synthesis validates each candidate against the same sanitizer harness introduced in §5.6 — NeuroLog’s one built artifact. A candidate is a crash iff the harness exits non-zero with an ASan-recognisable signature.

5.8.0.3 Calibration on CVE-2023-45676.

Phase A proves the comment-length value reaches setup_malloc along a feasible path. The synthesis agent recognises Vorbis from context — it knows the Ogg capture_pattern and the comment-packet header. Its first witness sets \(\texttt{len} = \texttt{0xFFFFFFFF}\), but (len+1) wraps to a zero-byte request that does not fault; the no-crash ASan tail feeds back, and iteration 2 sets \(\texttt{len} = \texttt{0x7FFFFFFF}\), whose size argument (in 64-bit size_t) is a \(\sim\)​2 GB request. The resulting 102-byte blob crashes ASan deterministically with allocation-size-too-big at the sibling site start_decoder:3653. End-to-end synthesis \(\sim\)​5 min, almost all of it network round-trips; no fuzzer in the loop.

6 Implementation↩︎

NeuroLog is implemented in roughly 8 KLoC of Python plus the existing rules of the sibling Datalog project, which we take in unmodified. The module layout follows the six pipeline stages of §4.

6.0.0.1 Languages and dependencies.

Tree-sitter via the official tree-sitter-c grammar [9] drives stage 1 and the mechanical floor of stage 2; the grammar gives us language-aware identifier extraction and CFG-edge enumeration without requiring a working build of the target. Soufflé 2.4 [7] runs the rule mesh in stage 3; we invoke it as a subprocess and read its CSV outputs directly. Z3 4.12 [8] is used through the standard Python bindings in stage 4. AddressSanitizer (Clang -fsanitize=address) [14] is the oracle in stage 6, wrapped by libFuzzer [29] for single-input replay or by an equivalent thin C stub for projects that do not ship a fuzzer harness.

6.0.0.2 LLM access and orchestration.

Both in-pipeline LLM stages use the LiteLLM abstraction, so the analysis is provider-neutral. In our experiments the smell pass (stage 2) runs on a Lite-tier model (DeepSeek V4-Flash via an OpenAI-compatible endpoint) and the synthesis agent (stage 5) on a frontier model (DeepSeek V4-Pro). Orchestration uses no bespoke agent framework: NeuroLog exposes its stages and on-demand queries as Model-Context-Protocol (MCP) tools that a host agent — a coding agent such as Claude Code or OpenCode — drives, interleaving NeuroLog’s deterministic tools with its own reasoning and persisting verdicts back through the same interface. Any MCP-capable host, and any model with an OpenAI-compatible API, drops in.

6.0.0.3 Parallelism.

The smell pass parallelises across functions with a thread pool (15-way default; the bottleneck is provider throttling, not local CPU). Stage 4 parallelises across findings with a process pool (§5.5); each worker loads the FactStore once and processes a chunk of findings to amortise startup. The synthesis agent runs \(N{=}3\) candidate emissions per round in parallel and validates each candidate sequentially against the harness (because the harness is single- threaded by default).

6.0.0.4 Caching.

The smell pass writes a per-function cache keyed by a hash of the source plus the prompt template plus the model name; a re-run with the same inputs reads from cache, which keeps iterative analyst work cheap. The Datalog and SMT stages are re-run on every change, since they are seconds-scale and a full re-run is the simplest dependency contract.

6.0.0.5 Per-scan audit log.

Every component that performs a user-visible step (mech-extract per file, smell-pass aggregate, souffle per output relation, agent ad-hoc query, symbex per-batch, Phase C per candidate) emits one tab-separated line into a per-scan log when the NEUROLOG_AUDIT_LOG env var points to a path; the runners set it automatically per eval directory and ignore it on interactive sessions to avoid noise. The log is opt-in, threadsafe, append-only, and fail-safe (an audit-write error never breaks the pipeline). Lines are TSV columns <ISO-timestamp>, <phase>, <action>, <target>, <key=value detail>; the format is parseable. This is the record of what the tool actually did on a given run — which Datalog relations fired and with how many rows, which agent queries returned what, which symbex batches landed where — and is what makes a posthoc audit possible without rerunning the pipeline.

6.0.0.6 Artifact.

The pipeline source, the rule mesh, the prompts, and the eval scripts are released as an artifact; reproducing the stb CVE rediscovery and the FFmpeg precision tables of §7 requires only Soufflé, Python, and an LLM API key. Reproducing the Phase C crash synthesis additionally requires building the ASan harness once (a one-line invocation on stb; a documented configure flag on FFmpeg).

7 Evaluation↩︎

We evaluate NeuroLog along five axes: (i) end-to-end CVE rediscovery (§7.1), (ii) cost and recall of the LLM smell pass against an LLM-only fact-extractor baseline (§7.3), (iii) precision of the symbex post-pass and the Phase E filters (§7.4), (iv) wall-clock scaling of the parallel symbex stage (§7.5), and (v) end-to-end crash-input synthesis (§7.6). We then summarise the honest negatives the evaluation surfaced (§7.7).

The evaluation targets are listed in Table 2. All experiments are run on a single laptop-class machine (5 CPU cores available to the pool) without any accelerator. The two LLM stages call out to remote provider APIs over the network; the wall-clock cost on the LLM side is dominated by provider round-trip rather than local compute.

7.1 End-to-end CVE rediscovery↩︎

Table 3 lists every CVE NeuroLog re-discovered end-to-end in this evaluation. “End-to-end” means: the pipeline produced a Datalog finding pointing at the same source line as the published CVE without that CVE being supplied as input. Validation tier is one of three: fuzzer-confirmed — an independent libFuzzer/ASan run on the project produced a crash matching the static finding’s site; static-confirmed — the rule mesh’s evidence chain (taint source \(\to\) guards \(\to\) sink, with relations cited) matches the published CVE writeup; or partial — the pattern is surfaced but a CVE-class semantics is not modelled (e.g.DoS, no memory-corruption signal).

The two stb CVEs are independently confirmed by a libFuzzer/ASan run on fuzz_vorbis producing 23 unique crashes clustered in the stb_vorbis decode chain at the lines Datalog flagged (\(L_{3664/3670}\to L_{5112}\to L_{5390}\)). The FFmpeg H.264 sentinel-collision is notable because the compound pattern is deliberately not encoded as one rule; the mesh produces four ingredient relations and the host agent composes them. The libxml2 run is a scale demonstration: 40 source files, 2 707 functions, 185 839 facts, full pipeline 73 min (smell pass 22.6 min, Soufflé 16.7 min, symbex Phase A returns 2 226 feasibles). The smell pass agrees with the mechanical extractor on almost all facts (1 addition, 0 corrections in 2 707 calls).

We also tested whether the mesh re-discovers CVE-2025-6021 [37] in libxml2’s xmlBuildQName and four sister sites, this time using the pipeline as intended: handing the artefacts to the host agent with the on-demand neurolog__query_datalog tool (§5.4.1) and a one-paragraph prompt. Across 89 events the agent fired 19 ad-hoc Datalog queries that authored their own schemas, joined precomputed relations against raw facts, and recovered from two schema-arity errors after reading Soufflé’s line-numbered echoes. The agent’s diagnosis was sharper than ours: the affected set is six functions, not four (two more recovered by enumerating ArithOp facts with destination tmp and operands \(\{\)lenn, lenp\(\}\)); the recall miss is compound, not single-rule (LLM-introduced tmp carries no ResolvedVarType; ActualArg records the literal expression string, not a reference to tmp). The fix is a small bridging rule plus an extraction-layer patch, shipping as Pass 6 (source_arith_sink_bridge.dl, §5.4). Re-run on the same fact base, Pass 6 recovers 6 of 6 CVE-2025-6021 sites in 181 candidate (function, sink) pairs across 2 707 functions; applied to FFmpeg facts the same rule surfaces 41 candidates on the combined demuxer corpus and generalises to unrelated targets like matroska_decode_buffer:1707. The on-demand-query architecture is earning its keep.

7.1.0.1 CVE-2023-38545: rule developed end-to-end.

The two curl SOCKS rows share a structural pattern no existing rule covered: separate bounds checks on two operands (plen, hostnamelen) each individually sound, but whose joint bound vs.destination capacity is never asserted. We encoded the pattern as joint_buffer_bound.dl; on curl 8.3.0 it fires at do_SOCKS4:430 (the SOCKS4a strcpy upstream patch 01057d6161 later guarded) and at the do_SOCKS5:907 sister site that became CVE-2023-38545. Both fires reach the synthesis stage and ASan confirms a 3-byte overflow for the SOCKS4a path and a 2000-byte overflow for the CVE-2023-38545 path (the latter requires driving the async-yield state-machine bug that resets the local socks5_resolve_local flag on re-entry; an 800 ms stub delay suffices). This is the first eval target where we wrote a new rule because of the audit and watched it generalise: the do_SOCKS5 fire was not the bug we set out to find.

7.1.0.2 WebSocket: mesh localises, LLM reads the neighbourhood.

Auditing lib/ws.c re-discovered 6 of the 13 fixes that landed upstream between 8.3.0 and HEAD; beyond the three in Table 3 the system also surfaced a wrong-offset multi-fragment memcpy (silently fixed in #12945), missing RSV-bit validation (#16069), and an uninitialised send-count leak in Curl_senddata. Tellingly, the last two came not from a rule fire but from the LLM reading the decoder a mesh fire had already pointed it at — the neuro-symbolic loop working as intended. The 6 misses cluster into two classes the mesh did not yet cover, cross-function state-machine invariants and resource-cleanup paths, which directly motivated Pass 15 (state_machine_invariants.dl) and Pass 16 (lifecycle_audit.dl).

7.1.0.3 Recon front-end: a credential-scope case study.

The two miss classes above are exactly what the recon front-end (§5.1) targets. As a capability check we pointed recon at curl’s connection-reuse logic (lib/url.c), which the sink-seeded slice never reaches. Recon proposed the reuse comparators as seeds and a connection-reuse credential-scope hypothesis with a Datalog check; the smell pass then tagged each compared field via FieldSemantic, correctly recognising Curl_timestrcmp(needle->user, check->user) as a credential comparison. The omission rule fired on exactly one site — proxy_info_matches, which gates proxy-connection reuse on host/port/type but never on the proxy user/passwd the struct carries — and correctly cleared ConnectionExists (which does compare its credentials) and an age-check helper. This is the connection-reuse credential class that dominates the 2026 curl advisory wave, a class no memory-safety rule models; we report it as a demonstration of the LLM-perceives/Datalog-proves loop on a non-memory class rather than a novel finding (the underlying issue is plausibly a rediscovery), and leave a broad multi-target evaluation of the front-end to future work.

7.2 Novel-bug discovery on libarchive HEAD↩︎

To test whether the mesh surfaces novel issues on current code, we audited libarchive master at commit a651b4fc (HEAD, 2026-05-19) across five formats (XAR/WARC/7zip writers; cpio and iso9660 readers). The mesh’s LifecycleAudit, ResourceCleanupMiss, and a host-authored free-while-linked lens produced five candidate sites, all hand-validated under ASan/LSan: one use-after-free + double-free in the cpio reader (issue #3053 [38]); three resource-leak bugs in the XAR reader, WARC writer, and 7zip writer [39]–[41]; and one OOB read into adjacent .rodata in the XAR writer’s make_fflags_entry (issue #3059 [42]).¹ All five sites are filed upstream; per-bug source locations, ASan witnesses, reproducers, and proposed patches are in the linked issues.

The cpio finding is the most interesting individual result: a regression that the upstream commit which introduced it (a leak fix, 23 days earlier) made worse, not better. On opening the issue, maintainer acknowledged and opened PR #3055, crediting the reporter as commit author, with the fix following our proposed shape. The XAR-reader leak finding (issue #3058) was similarly acknowledged with fix PR #3060, whose body restates our issue text verbatim. At submission, the 7zip-writer (PR #3062) and XAR-reader (PR #3060) fixes are merged and the XAR-writer OOB read is resolved upstream via PR #3041; the WARC-writer (PR #3061, approved) and cpio (PR #3055) fixes remain in review.

The audit yields a small taxonomy of “where the mesh found bugs fuzzing did not”: no test exercises writer-side error paths (two leaks); cleanup that misses one of many struct members because the populator lives in a sibling translation unit (one leak); string-literal lookup tables whose fast pre-filter trusts the null terminator (one OOB read); ENOMEM-gated paths fuzzers under-explore (the cpio UAF). None are reader-side parser bugs OSS-Fuzz would have surfaced — evidence that NeuroLog complements fuzzing rather than competing with it.

7.3 Cost and recall of the LLM smell pass↩︎

The mechanical floor + smell pass is one of the two extractor configurations in §5.3; the other is a frontier-model-only extractor reading the full function source without the tree-sitter floor. Both run on the same 128-function stb slice (Table 4).

\(90{\times}\) faster, \(70{\times}\) cheaper, recovers coverage on three bug-relevant functions the frontier extractor truncated, matches CVE-class recall. This is the empirical license for §5.3: the LLM is best at function-local augmentation, not whole-codebase reading.

7.4 Symbex precision and Phase E filters↩︎

We measure precision at three points: Phase A \(\to\) B flips, Phase E1 root-vs-symptom split, and Phase E2 invariant reduction.

7.4.0.1 Phase A \(\to\) Phase B (Tab. 5).

Phase A path-guard filtering does most of the work — 28–38 infeasibles per FFmpeg target with no catalog. Phase B summaries flip exactly one finding overall: slice_type in ffmpeg_h264_801, where get_ue_golomb_31’s catalog summary (return \(\in[0,31]\)) tightened the constraint. Demuxer callees flow through ebml_* / avio_* variants we have not catalogued, so summaries do not bind there.

7.4.0.2 Phase E1 dependence filtering (Tab. 6).

Symptom share is lower than Sahoo et al.’s 58 % [13]: their dataset was real-bug-centric (single root, many symptoms); ours is broad static coverage with many independent reads. The cluster structure remains useful: mov_read_header has 7 symptoms behind 2 roots (2 bugs to investigate, not 9); matroska_parse_laces has 1 symptom behind 6 roots (a tightly-coupled region readable top-down).

7.4.0.3 Phase E2 likely-invariants (Tab. 8).

On stb, eight Vorbis seeds give 43.3 % reduction, all in start_decoder’s loop counters; CVE-2023-45676 /45681 sites are unaffected because they live in relations Phase E2 does not consume (SignConfusionCast, TypeSafetyFinding). On FFmpeg demuxer, three Matroska seeds give 13.2 %; relations asking about “out-of-range arithmetic” are demoted the most (NarrowArithAtSink 80 %) because the corpus provides direct counter-examples.

7.5 Phase D — parallel symbex scaling↩︎

Table 9 reports wall-clock serial vs.at \(N{=}2,4,8\) workers (parity against serial verified).

The 4-worker plateau is per-worker fixed cost (\(\approx 50\) ms FactStore + Python imports), not Z3 saturation: on ffmpeg_demuxer_full the 8-worker speedup (\(2.3\times\)) does extend past 4-worker, leaving room at codebase scale.

7.6 Phase C — crash-input synthesis↩︎

7.6.0.1 Calibration on stb_vorbis.

On CVE-2023-45676, the Phase B finding start_decoder:3670 tmp unbounded_counter_at_sink feeds the synthesis agent with the SMT model (\(\texttt{vendor\_length}=\)0x7FFFFFFF), the def-use chain back to get32_packet, the snippet, and a Vorbis format hint. At \(N{=}3\) candidates/round, iteration 2 produces a 102-byte Ogg/Vorbis blob crashing fuzz_vorbis (ASan: allocation-size-too-big at start_decoder:3653, the sibling site of the same CVE class). End-to-end \(\approx\)​5 min, mostly network round-trips. Reproducible via fuzz_vorbis stb_mechanical_smell/synth_crash.bin. No fuzzer was used in the synthesis loop; the only fuzzer contact is the ASan oracle in stage 6.

7.6.0.2 FFmpeg matroska_parse_webvtt:3853 — honest negative.

On the FFmpeg matroska demuxer’s text_len finding (Phase B feasible without invariants), five iterations of progressively-better setups (matroska-specific harness, scaffold seeding, \(P_c/V_c\) prompts) produced 161–169-byte mutations of the 163-byte scaffold; GDB confirmed candidate 0 of synth 5 reaches the target function. No crash. Investigation showed a static FP: text_len = q - p where \(q=\texttt{data}+\texttt{data\_len}\) and \(p=\texttt{data}\), so \(q < p\) is unreachable. This is the case Phase E2 was designed for: running E2 on a three-seed Matroska corpus demotes the finding (Tab. 8). The closed-loop story: synthesis exhausted five attempts on a static FP, the analyst recognised it, ran E2 once, the next pipeline run no longer flags the site.

7.6.0.3 What this validates and what it does not.

The framework is end-to-end functional on real-world FFmpeg — ASan-instrumented per-demuxer harnesses build cleanly, scaffold synthesis produces correctly-structured mutations that reach the target function, and the chain-walker fix following plain assignment edges is permanent. What FFmpeg does not demonstrate is novel-CVE discovery on its own corpus: the matroska finding was a static FP, and the other demuxer feasibles remain to be triaged manually.

7.7 Honest negatives↩︎

We summarise the negatives the evaluation surfaced so a reader can calibrate the headline numbers. These negatives also constitute our future work in this direction.

• Fact-extraction recall on LLM-introduced intermediates. On the libxml2 xmlBuildQName site and its five sister patterns in xmlregexp.c, the smell pass emits an ArithOp for tmp = lenn + lenp + 2 but no Def / VarType / ResolvedVarType on tmp, and the call’s ActualArg records the literal expression string rather than a reference to tmp. The headline int + int arithmetic-overflow rule misses all six sites until the bridging Pass 6 (§5.4) is added. The underlying gap — the LLM does not type its synthetic intermediates — is the worst LLM-recall failure mode the evaluation surfaced and the most plausible source of further silent misses in the long tail.

• Rule-mesh coverage gaps. The mesh does not model: DoS-by-recursion, UAFs whose free is conditional on a callee return, and compound patterns like FFmpeg’s H.264 32-bit-counter-into-16-bit-sentinel collision (the four ingredient relations exist; rule-level composition does not). The H.264 case is handled by the host agent composing relations after the fact; mesh recall on that family is bounded by the agent’s compositional ability (but this is also the design philosophy of NeuroLog— on-demand datalog queries).

• Phase B catalog effects are small. The targeted catalog of bitstream readers (get_ue_golomb_31 and friends) flips one finding total in our evaluation. The mechanism works — the flip is genuinely the right call — but the catalog is small relative to the function space, so its overall precision contribution is modest.

• Phase E1 symptom share is low. At 2 – 13 % across targets, much lower than Sahoo et al.’s 58 % [13]. The likely cause is workload structure: their dataset was real-bug-centric (single root, many symptoms); ours is broad static coverage (many independent reads). The cluster structure is still useful for triage even when the percentage is small.

• Phase E2 ordering bug cost five synthesis iterations. We spent five Phase C rounds confirming that matroska_parse_webvtt:3853 cannot crash before recognising it as a static FP and running E2. Phase E2 should run before Phase C; the current ordering is an artifact of when each pass was developed. Re-ordering is mechanical (§8).

• Soufflé is the dominant non-LLM cost at scale. On libxml2 (185 839 facts, 2 707 functions), the five-pass mesh takes 16.7 min — larger than the LLM smell pass at 22.6 min at 15-way parallelism, but the same order. At codebase scales above libxml2 the Soufflé runtime will dominate; we have not investigated the standard mitigations (table partitioning, incremental evaluation).

• No head-to-head against industrial baselines. We did not run CodeQL or Joern on the same targets. CodeQL requires a working build (which our targets either lack or require significant scaffolding for), and Joern’s open-source C/C++ frontend does not carry a runtime-grade decision procedure for path feasibility. The precision and recall claims in this paper are therefore absolute rather than relative; an apples-to-apples comparison on Magma is the natural follow-up benchmark (§8).

• Triage backlog. The smell pass produces several hundred possible_uninit_free flags on FFmpeg that we have not reviewed; the E2-filtered FFmpeg demuxer feasible set (295 findings) is also untriaged. These remain the most plausible source of additional high-confidence findings on the codebases evaluated, but per-flag manual review is the bottleneck we have not yet paid.

8 Discussion↩︎

8.1 Threats to validity↩︎

8.1.0.1 Silent recall misses from the LLM.

The biggest threat is that the smell pass omits a fact the rule mesh needs — a missing Cast silently kills an ImplicitTruncation finding. We mitigate three ways: (i) the mechanical floor produces structural facts deterministically, so the LLM cannot omit them; (ii) the schema is small and security-aware, keeping the prompt focused; (iii) §7.3 matches CVE-class recall against a frontier-model-only baseline on a held-out slice. None of these prove the LLM doesn’t miss in the long tail; the libxml2 xmlBuildQName miss is exactly this category.

8.1.0.2 Compile-free trade-offs.

NeuroLog gives up the precision benefits of a full build: the preprocessor is not run, so macros that conditionally insert guards or sinks are invisible; the type system is not lifted, so struct-definition-driven disambiguation is unavailable. We pay this knowingly to gain the property that an analyst can run on an unfamiliar codebase in seconds. A build-based front end could extract the same facts better; we claim the cost difference is worth the precision gap on the codebases we evaluated.

8.1.0.3 Rule-mesh coverage.

The mesh is the union of two prior efforts (the sibling project’s binary-side rules plus source-side extensions). It does not cover every CVE class: DoS-by-recursion, certain UAFs where the free is conditional on a callee return, and the H.264 sentinel-collision compound pattern are all under-covered. The H.264 case is honest: four ingredient relations surface and the agent layer composes them. Mesh recall is bounded by the agent’s compositional ability on findings the mesh did not directly flag. However, the users can add new rules based on their target’s audit as NeuroLog is expandable by design.

8.1.0.4 Single LLM provider.

Both LLM stages were exercised against DeepSeek V4 in our experiments. The smell pass is generic to any OpenAI-compatible endpoint; the synthesis agent uses provider-neutral LiteLLM. We have not done a head-to-head with other providers, so we do not claim provider-independence; only that the design uses no provider-specific features (no fine-tuning, internal APIs, or proprietary tools).

8.1.0.5 Scale of the evaluation.

Eight rediscovered CVE-class issues plus five novel libarchive findings across six codebases is a moderate envelope. Magma [44] is the natural next benchmark, but a fuzzer-targeted benchmark (manually-injected bugs, crashes-found labels) is structurally different from a static-analyser evaluation; we kept this paper’s targets comparable to the manual review practitioners do today.

8.2 Design decisions revisited↩︎

8.2.0.1 LLM as fact extractor, not query composer.

The most natural alternative design uses the LLM at query time: the analyst describes a vulnerability pattern in natural language, the LLM emits a Datalog query, the engine runs it, and the analyst iterates. Such a design suits a setting where the fact base already exists — typically because a production analyser has lifted the project to an IR — and the analyst’s bottleneck is expressing the pattern, not extracting the facts. NeuroLog takes the opposite tack because on unbuilt source fact extraction is the bottleneck and because a fact base is auditable in a way an ad-hoc query is not (we can diff two runs and identify which tuples appeared/disappeared). We move the LLM below the rule mesh: it fills tuples, the rules express patterns once and reuse them across targets.

8.2.0.2 SMT as a post-pass, not in the rule body.

Discussed in §9 and §5.5; the deliberate trade is full Soufflé throughput + per-finding parallelism + an exposed SAT model that downstream stages consume. Formulog’s intra-rule integration buys earlier pruning at the cost of a bespoke evaluation strategy and an unexposed model. The two designs are not strictly comparable on benchmarks (different workloads), but post-pass is the simpler retrofit onto an existing rule corpus — our need.

8.2.0.3 Tier-don’t-drop vs.aggressive filtering.

Every Phase E pass exposes a tier rather than removing findings, guarding against mute-then-miss: an attacker input the corpus did not exercise would be exactly what an aggressive filter would mute. We trade a longer finding list for correctness, assuming a report UI shows tier-1 by default and expands lower tiers on demand.

8.3 Future work↩︎

8.3.0.1 Re-order Phase E2 to run before Phase C.

The matroska FP of §7.6 cost five synthesis iterations because E2 was implemented after C in our timeline. Re-ordering is mechanical and should be done before the next campaign.

8.3.0.2 Magma benchmark with patch/unpatch.

Magma [44] ships curated real vulnerabilities in libtiff, libxml2, libpng, poppler, etc., each toggled by a one-line patch. Patched tree should give zero high-confidence findings at the site (FP rate); unpatched should surface the finding (TP recall). A direct comparison with classical static analysers and fuzzers on the same labelled set is the obvious next experiment; because Magma supplies the harness, the only per-target variable is the sink catalog.

8.3.0.3 Cross-codebase invariant transfer.

Phase E2 invariants are project-local. Whether range invariants extracted on one codebase — e.g., “a length field after varint decode is \(\le 2^{32}-1\)” — transfer to other codebases using the same protocol family is open. If so, the seed cost amortises across projects.

8.3.0.4 Concolic-style \(P_c\)-byte mapping.

Synthesis currently hands the SMT model to the LLM as text; the LLM maps model values back to byte offsets. COTTONTAIL’s runtime concolic tracing [28] gives a more direct mapping at the cost of running the target. A static approximation — track each \(P_c\) symbol back through the parser to a byte offset, even imperfectly — is reachable.

8.3.0.5 Richer rule-mesh coverage.

Use-after-free with conditional frees, type-confusion across union members, and DoS-by-recursion are all recall gaps we identified during evaluation. Adding rules is mechanical; the limit is analyst time rather than theoretical complexity.

9 Related work↩︎

NeuroLog is most usefully positioned as a re-application of an old idea in a new substrate. We organise this section around the four threads of work it touches: (i) Datalog-based static analysis, (ii) the Datalog + SMT combination specifically, (iii) the broader “cheap static analysis narrows SMT” lineage, and (iv) LLMs for vulnerability detection and structured input generation.

9.0.0.1 Datalog-based static analysis.

The Datalog school of static analysis has matured into the production tooling we treat as a substrate. Doop’s points-to analysis [20] demonstrated that sophisticated context-sensitive pointer reasoning fits in a few hundred lines of Horn clauses; Soufflé [7] synthesises parallel C++ from such rules and is the engine NeuroLog uses unmodified. CodeQL [1] packages a Datalog-style query language for industrial security review. Code property graphs [2] share Datalog’s auditability while emphasising graph reachability patterns. NeuroLog reuses the rule mesh idiom of these systems but moves the IR producer — the part that would normally consume LLVM, the Java bytecode, or a build-wrapper-instrumented C compiler — to a language model that reads source directly.

9.0.0.2 Datalog with SMT.

Formulog [12] introduced an SMT-aware Datalog dialect in which is_sat() is callable from a rule body; the engine schedules SMT queries during semi-naive evaluation. The 2024 follow-up [45] shows that an unconventional “eager evaluation” strategy gives \(5{-}7\times\) speedups on SMT-heavy workloads. Formulog’s three case studies include refinement-type checking, Java pointer analysis, and a Datalog-encoded symbolic execution. The relationship to NeuroLog is sibling, not ancestral: Formulog puts SMT inside the rule body, NeuroLog runs SMT as a post-pass over Soufflé’s findings. The two designs trade differently: intra-rule SMT can prune derivations as they form but requires a bespoke evaluation strategy; post-pass SMT keeps Soufflé at full relational throughput and lets Z3 calls parallelise trivially over findings (§5). Concretely, our Datalog phase runs in \(\approx 2\) seconds on a 200K-fact libxml2 input and our SMT phase in \(\approx 1\) second on roughly 300 findings; Formulog’s benchmarks are in the same ballpark but on different workloads, so we do not benchmark them head-to-head.

9.0.0.3 Static analysis narrows SMT (NeuroLog’s analytical lineage).

The shape of NeuroLog’s symbex stage — “cheap static analysis produces dataflow chains; SMT checks each chain” — is well-established prior art. Saturn [10], [46] introduced compositional SAT-based bug finding using function summaries; Snugglebug [16] computes weakest preconditions backward from a target site, demand-driven; Pinpoint [11], built on SVF [47], scales path-sensitive value-flow plus SMT to million-line targets. NeuroLog is best read as a re-application of this lineage with three substantive changes: the dataflow substrate is Datalog rather than a bespoke value-flow IR, so the analyst can extend and audit it with the same idiom they would use for a new taint rule; the substrate is fed by an LLM rather than a compiler, so no build is required; and the SMT artifact is the SAT model itself, not a yes/no verdict — the model flows into NeuroLog’s crash-synthesis stage. None of the four cited systems do crash synthesis from the SMT witness.

9.0.0.4 LLMs for vulnerability detection.

IRIS [4] demonstrated that LLMs are good at inferring missing taint specifications — sources, sinks, sanitisers — and that combining them with CodeQL improves recall on Java vulnerabilities. NeuroLog generalises the same observation: once the LLM has been told which schema of facts to emit, it is good at producing those facts on a function-by-function basis, including the structural facts (ArithOp, Cast, FieldRead, Guard) that go beyond IRIS’s specification-only role. Where IRIS uses the LLM to enrich a classical analyser’s input, NeuroLog uses it to produce that input; CodeQL’s IR-lifting compiler is replaced rather than augmented.

9.0.0.5 LLM-driven concolic / structured input generation.

COTTONTAIL [28] couples LLM-driven concolic execution with built-target instrumentation for highly structured input formats. Their LLM “Constraint Mask / Flexible Mask” decomposition — the LLM marks regions of the input that are constrained by the path condition versus regions the solver may freely choose — is the closest analogue to NeuroLog’s \(P_c\) / \(V_c\) scaffold split (§5). The integration is again sibling rather than ancestral: COTTONTAIL runs concolic on a built target and the LLM steers input mutation; NeuroLog’s synthesis stage runs from a static SAT model with no concolic execution, and the LLM is told both the scaffold (a known-good prefix to leave undisturbed) and the \(V_c\) bug condition. The two systems are complementary: a static NeuroLog finding could feed COTTONTAIL’s mutation budget on codebases where the target compiles.

9.0.0.6 Failure sketching and likely invariants.

Kasikci et al.’s Gist [26] introduced adaptive backward-slice tracking with hardware watchpoints for production failure root-causing. Their \(\sigma\)-doubling slice-expansion idea is the source of NeuroLog’s Phase E4 adaptive-slice heuristic. Sahoo et al. [13] introduced range invariants from a small number of normal-input runs as a fault-localisation aid; NeuroLog repurposes them as a precision filter on the SMT pass and adopts the dependence-clustering idea (E1) directly. We deliberately do not adopt their ddmin-style character rewriting for input generation, because Phase C uses an LLM with a file-format prior instead.

9.0.0.7 Symbolic execution and concolic platforms.

KLEE [23] and SAGE-class whitebox fuzzers [24] are the established way to ask SMT questions about whole-program behaviour, and angr [48] provides the canonical binary-side platform for the same family of techniques. They explore the program’s path space directly; NeuroLog’s symbex stage instead encodes only the def-use chain that a Datalog finding has already identified. This is what makes the SMT cost in NeuroLog sub-second-per-finding rather than the open-ended exploration cost that KLEE-class tools incur. We see the two as different points on the same axis: NeuroLog gives up KLEE/angr’s ability to discover paths the analyst did not anticipate, in exchange for predictable wall-clock costs at codebase scale.

9.0.0.8 Code-level fuzzing dataset.

The Magma fuzzing benchmark [44] provides ground-truth bug labels in libtiff, libxml2, libpng, and other parsers. A larger version of the present evaluation would draw its CVE set from Magma rather than from an ad-hoc list; we leave that as future work.

10 Conclusion↩︎

NeuroLog is a small empirical argument for an old idea applied to a new substrate. The old idea is that LLMs, declarative static analysis, and SMT solving each have a part of the vulnerability-analysis task they are uniquely good at, and that a pipeline assigning them complementary roles is the natural arrangement. The new substrate is source code without a build: a setting where a frontier LLM is the only tool that can lift the program to a usable representation, where a Datalog rule mesh can do that lifting’s downstream work much more efficiently than the LLM can on its own, and where an SMT post-pass can then cheaply filter the results because the rule mesh has already shrunk the search.

The resulting pipeline re-discovers five published CVEs end-to-end, two of them fuzzer-confirmed, and synthesises a 102-byte ASan-confirmed crashing input for one of them with no fuzzer in the synthesis loop. A likely-invariant filter collected from three corpus seeds eliminates 13.2 % of the FFmpeg-demuxer feasible set, including the static false positive that the synthesiser had spent five attempts trying to crash. The cost-and-recall comparison with a frontier-model-only extractor is one-sided: 90\(\times\) faster, 70\(\times\) cheaper, no recall loss on the bug-relevant functions.

The honest negatives matter and we have presented them at the same volume as the positives. No novel CVE was surfaced; the libxml2 source-side run missed an entry we expected to find; the FFmpeg demuxer slice has a 295-feasible E2-filtered set we have not yet triaged manually; and the most painful single incident was a five-iteration synthesis attempt against what turned out to be a static false positive that an earlier Phase E2 run would have caught.

We see NeuroLog as a starting point. The task split it proposes — LLM for fact extraction at the function level and crash synthesis at the format level, Datalog for cross-function composition, SMT for path feasibility, runtime invariants for sanity, ASan as the ground-truth oracle — is meant as a template. We believe each role can be tightened independently of the others, that a richer rule mesh and a Magma-class evaluation [44] would extend the empirical envelope, and that the compile-free property is the right constraint to keep around: it is what makes the system feel, to an analyst opening an unfamiliar codebase, more like grep than like CodeQL.

Acknowledgements↩︎

We thank Anthropic Claude (Opus 4.7, 1M-context) for substantial assistance in implementation, ablation, and writing. Decisions about methodology, claims, and conclusions remain the sole responsibility of the human author.

11 The NeuroLog rule mesh↩︎

This appendix lists every output relation the rule mesh produces, grouped by the bug family it targets. The relations are the shared interface between Datalog (which materialises them) and the symbex / synthesis stages (which consume them). Each relation is keyed on (func, addr, var) or a small extension of that tuple; the full schemas are in the public artifact’s rules/ directory.

11.0.0.1 Taint propagation (interprocedural).

TaintSourceFunc and DangerousSink are the two catalogs the analyst can edit; TaintedVar is the fixpoint over them.

• TaintedVar(func, var, addr, origin, kind) — variable var at addr carries a value derived from external input identified by origin.

• TaintedSink(caller, callee, ca, idx, var, risk, reason) — a tainted var reaches argument idx of a dangerous sink call.

• UnguardedTaintedSink(...) — as TaintedSink but with no CFG-reachable guard between the taint and the sink.

11.0.0.2 Integer / type-safety bugs.

• NarrowArithAtSink — arithmetic in a declared-narrow type whose result feeds a sink argument (e.g.a 32-bit add feeding a 64-bit size_t parameter of malloc).

• TaintedNarrowArith — as above, with TaintedVar on the arithmetic destination.

• ImplicitTruncation — assignment of a wider type into a narrower lvalue without an explicit cast on a value that may not fit.

• TaintedTruncation — as above, with TaintedVar on the truncated value.

• SignedArgAtSink — a signed-typed value reaches a sink argument whose contract requires unsigned (e.g.a signed int feeding the n parameter of memcpy).

• TaintedSignedAtSink — signed-arg-at-sink with taint.

• SignednessMismatch / SignConfusionCast — cast between signed and unsigned of differing widths whose effective range silently changes.

• PotentialArithOverflow — arithmetic whose result type cannot represent the sum or product of the operand range.

• OverflowAtSink — PotentialArithOverflow whose result reaches a sink.

• TaintedOverflowAtSink — ditto with taint.

11.0.0.3 Counter / loop-bound bugs.

• UnboundedCounter — a variable incremented in a loop with no upper-bound guard.

• TaintedUnboundedCounter — as above, with taint.

• CounterUsedAsIndex — a loop counter used as a buffer index without a per-iteration bound check.

• TaintedCounterAsIndex — ditto with taint.

• TaintedLoopBound — the loop’s terminating condition is itself a tainted variable.

• BufferOverflowInLoop — a tainted loop bound combined with a buffer write in the loop body and no per-iteration bound check.

11.0.0.4 Memory-safety bugs.

• UncheckedAlloc — the return value of an allocator is dereferenced without a NULL check on the CFG-reachable path.

• DoubleFree — two free calls on the same pointer without an intervening reassignment, with both calls reachable from one CFG entry.

• TaintedHeapObject — a heap object whose initialisation depends on taint (relevant for downstream type-confusion checks).

• AliasTaintedVar — alias-aware extension of TaintedVar for pointer-aliased writes.

11.0.0.5 Compound / summary relations.

• TypeSafetyFinding(func, addr, category, var, detail) — the union of all type-safety relations into one per-finding row, used by the symbex stage.

• MemSafetyFinding(...) — the analogous union for memory-safety relations.

• TaintReachableFunc — functions reachable from any TaintSourceFunc call site, used both for call-graph pruning and as a sanity check.

The complete rule mesh is approximately 30 rules across the five files (source_taint.dl, source_type_safety.dl, source_memsafety.dl, source_interproc.dl, source_sink_pass.dl); none of them is novel as a declarative pattern — the contribution of NeuroLog is that the facts that feed them come from an LLM rather than a compiler IR.

References↩︎