Paper deep dive

EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming

Kaustuv Mukherji, Jaikrishna Manojkumar Patil, Colton Payne, Paulo Shakarian, Dana Warmsley, Nigel Stepp, Evelyn Kim

Year: 2026Venue: arXiv preprintArea: cs.CRType: PreprintEmbeddings: 93

Intelligence

Status: not_run | Model: - | Prompt: - | Confidence: 0%

Entities (0)

No extracted entities yet.

Relation Signals (0)

No relation signals yet.

Cypher Suggestions (0)

No Cypher suggestions yet.

Abstract

Abstract:Large language models are increasingly used to reason about software vulnerabilities, but their outputs can silently violate domain knowledge, limiting their reliability in safety-critical settings such as medical devices. Prior work either treats that output as a prediction to be scored or constrains it to walks within a single knowledge graph; neither checks whether reasoning over a binary is consistent with an independent body of domain knowledge. We present EntailLLM, which validates each LLM-proposed analyst path by entailment: the path is a traversal of the binary's function call graph, the domain knowledge is represented in a separate graph, and verification aligns the two under temporal annotated logic. Across three CWE classes, four LLMs, three prompting strategies, and seven binaries varying in size from 405 to 12,696 function call-graph nodes, domain knowledge raises pooled entailment from 78% to 98%, with entailment decreasing in only 3% of the experiments. EntailLLM is deployed end-to-end on real medical-device binaries, reaching 98% pooled entailment without per-device tuning. Our system inherits the formal guarantees of generalized annotated logic, providing logical verification of LLM output that is both explainable and grounded in well-defined semantics.

PDF

Open source PDF →Open local PDF →

Trouble viewing inline? Open PDF directly →

Full Text

91,636 characters extracted from source content.

Expand or collapse full text

EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming Kaustuv Mukherji 1∗ , Jaikrishna Manojkumar Patil 1 , Colton Payne 1 , Paulo Shakarian 1∗ , Dana Warmsley 2 , Nigel Stepp 2 , Evelyn Kim 2 , 1 Syracuse University 2 HRL Laboratories kmukherj@syr.edu, jpatil01@syr.edu, crpayne@syr.edu, pashakar@syr.edu, dmwarmsley@hrl.com, ndstepp@hrl.com, ekim@hrl.com Abstract Large language models are increasingly used to reason about software vulnerabilities, but their outputs can silently violate domain knowledge, limiting their reliability in safety-critical settings such as medical devices. Prior work either treats that output as a prediction to be scored or constrains it to walks within a single knowledge graph; neither checks whether rea- soning over a binary is consistent with an independent body of domain knowledge. We present EntailLLM, which validates each LLM-proposed analyst path by entailment: the path is a traversal of the binary’s function call graph, the domain knowledge is represented in a separate graph, and verifica- tion aligns the two under temporal annotated logic. Across three CWE classes, four LLMs, three prompting strategies, and seven binaries varying in size from 405 to 12,696 func- tion call-graph nodes, domain knowledge raises pooled en- tailment from 78% to 98%, with entailment decreasing in only 3% of the experiments. EntailLLM is deployed end-to- end on real medical-device binaries, reaching 98% pooled entailment without per-device tuning. Our system inherits the formal guarantees of generalized annotated logic, providing logical verification of LLM output that is both explainable and grounded in well-defined semantics. 1 Introduction Large language models are increasingly applied to vulner- ability discovery, from detection and triage to exploit rea- soning and patch generation (Sheng et al. 2025). Yet they remain unreliable at identifying and reasoning about vulner- abilities unaided (Ullah et al. 2024), they produce confident inferences that probability-based checks cannot catch (Pan et al. 2023), and they mislead analysts when their sugges- tions go unchecked (Basque et al. 2026). These problems worsen for bespoke reverse-engineering tasks in domains such as medical devices, whose firmware is long-lived, hard to patch, and rarely shipped with source (Das 2022): analysis proceeds on decompiled binaries, where the semantic cues of source code are absent and intent must be reconstructed from low-level structure. In this paper we study the problem of identifying paths through a binary’s function call graph that lead toward a vulnerability and adhere to domain knowl- edge. We present EntailLLM, a system deployed at scale Preprint. Under review. ∗ Corresponding author. Figure 1: An LLM mistake caught by domain knowledge. The green path (with bold arrows) through the codebase was selected; the orange nodes (with faded edges) denote other code blocks in the binary. on real medical-device firmware, that improves an LLM’s ability to find such paths. Figure 1 is a screenshot of Entail- LLM catching erroneous LLM output: the library function memset is correctly assigned to the memory-management class, but the LLM then assumes it can perform an integer size calculation—an inference that is structurally unremark- able yet supported by nothing memset does. EntailLLM does more than flag such violations. Pairing domain knowl- edge with self-refinement raises the fraction of paths entailed from 71% to 97% while increasing the number of entailed paths by 37%, from 1,054 to 1,445—more than any other configuration we evaluate. The distinction that makes this possible is between statis- tical clean-up, pruning candidate paths by structural signals such as the call graph, which an LLM or a graph-based method already does well, and semantic clean-up: rejecting a path that violates the meaning of the domain even when it is structurally plausible. Only a logic-based reasoner supplies the latter. EntailLLM treats each LLM-proposed path as a hypothesis and admits it only if a domain-knowledge graph (DKG) entails it. The trajectory is a traversal of the binary’s call graph while the constraints come from a separate DKG, so verification is an alignment between two graphs rather than a walk within one. The domain encoding instantiates hand-crafted templates over the knowledge graph’s triples, arXiv:2608.01763v1 [cs.CR] 3 Aug 2026 yielding conjunctive, co-dependent-label rules grounded in CWE, MITRE, and device documentation. We assume the domain knowledge itself is accurate; our contribution lies in the machinery that enforces entailment by it. Our contributions are: (i) a reframing of LLM vulnerability analysis as cross-graph entailment checking of analyst traver- sals rather than final answers; (i) a deployed, end-to-end system that localizes and explains non-entailments, report- ing the first unsupported step with the rule firings behind it; and (i) an evaluation across three CWE classes, four LLMs, three prompting strategies, and seven binaries, in which do- main knowledge raises pooled entailment from 78% to 98%, decreasing in only 3 of 94 configurations. Section 2 formal- izes the entailment-checking problem, Section 3 describes the system, Section 4 reports experiments, and Section 5 the deployment. Related Work. Work that reports gains from LLMs on secu- rity tasks pairs the model with structure rather than trusting it alone (Lekssays et al. 2025). Applying LLMs directly to stripped or decompiled binaries recovers source-like code, symbols, and readable decompiler output (Tan et al. 2024; Xie et al. 2024; Hu, Liang, and Chen 2024), improving the representation an analyst works from but not verifying that reasoning over it is consistent with what is known about the vulnerability class. Other work gates LLMs with structure to similar ends, translating a problem into symbolic form for a solver (Pan et al. 2023) or constraining generation to paths grounded in a knowledge graph (Luo et al. 2024a,b); these align reasoning to a walk within a single KG and are eval- uated on natural-language QA. Our arrangement is closest to shielding in safe reinforcement learning (Alshiekh et al. 2018), where the LLM proposes freely and the logic decides what passes. But a shield strong enough to block unsafe be- havior typically blocks useful behavior with it, and here we show that enriching the generator with the domain knowl- edge’s own derived vocabulary admits more logically cor- rect analyst paths than shielding alone. Classical taint-based discovery and its recent LLM-driven variants (Redini et al. 2020; Liu et al. 2025) share our binary-level, source-free set- ting but aim to emit vulnerability alerts; where they use the LLM to produce the analysis, we use logic to check it. A detailed literature review appears in the Appendix. 2 Problem Description Technical Preliminaries. We reason in generalized anno- tated logic (Kifer and Subrahmanian 1992), which supplies a single formal semantics generalizing fuzzy and other real- valued logics, and we work in a tractable fragment that ad- mits exact polynomial-time deduction (Shakarian and Simari 2022) and represents time explicitly (Shakarian, Simari, and Subrahmanian 2012). We recall only what is needed here and refer the reader to that work for the full development. An annotated literal a:μ pairs a literal with an annotation μ = [ℓ,u] ⊆ [0, 1]. The lattice is ordered so that [0, 1]— total uncertainty—is the bottom element, while tight inter- vals such as [1, 1] and [0, 0] sit at the top. This makes the logic open-world: an unobserved literal is not false but merely un- certain, and inference narrows it, so the partial and noisy observations recovered from a binary need not be forced to true or false. A temporal annotated fact (TAF) asserts such a literal at a time point, written a:(μ,t), and rules take the form ℓ 0 :μ 0 ∆t ←− ℓ 1 :μ 1 ∧·∧ℓ m :μ m , where a body satisfied at t makes the head hold at t + ∆t. A program Π is a set of TAFs and rules. An interpretation I maps each ground literal and time point to an annotation; it satisfies a:μ at t when μ ⊑ I(a,t), and is a model of Π when it satisfies every rule and TAF. Deduction iterates a fixpoint operator Γ to convergence, yielding the minimal model I ∗ . Γ is mono- tonic, converges in polynomial number of applications, and decides entailment. Entailment is therefore an exact, decid- able consequence of the program’s semantics rather than a heuristic score, and because every interpretation is produced by an identifiable rule firing, each inference carries a trace of the facts and rules that led to it. Entailment Checking of Analyst Paths. Given a target binary and a weakness class (CWE), the LLM predicts ex- ploration workflows an analyst might follow through the bi- nary’s functions toward a vulnerability of that class. The input is the binary’s function call graph, functions as nodes and calls as edges, with each function labeled with a set of libc labels; the output is a sequence of connected call- graph nodes. Our prompts steer exploration toward the target weakness class and entailed traversals feed a fuzzer down- stream in the deployed system, so the traversal is the in- put to discovery rather than a substitute for it. We evaluate CWE-121 (stack-based buffer overflow), CWE-415 (double free), and CWE-416 (use-after-free). We first fix a domain- knowledge program Π = Π T AF s ∪ Π Rules , assumed correct and fixed, whose facts encode the DKG and whose rules are described in Section 3. We denote a temporally ordered sequence of code blocks as: τ = ⟨CB 0 ,...,CB n ⟩. Then an LLM-proposed candidate analyst trajectory linked by a predicate called stepFrom is encoded by TAFs, and can be written as F (τ ) = analystAt (CB 0 ) : (μ 0 , 0) ∪ stepFrom(CB i−1 ,CB i ) : (⊤,i) n i=1 asserting that each step is proposed at the corresponding time point, and we reason over Π∪ F (τ ), whose minimal model we denote I ∗ . Note that τ and Π live in different graphs: τ is a chain in the binary’s call graph, whose connectivity is guaranteed by construction, while Π’s facts encode the DKG’s vulnerability concepts and typed semantic relations. Entailment is therefore an alignment between the two, not the existence of a path within either. A step CB i−1 → CB i is entailed when the domain knowledge verifies that the analyst can follow F (τ ) to reach CB i at time i: Π∪ F (τ ) |= ent analystAt (CB i ) : (μ,i), μ⪰ μ min where μ min is the minimum admissible bound. If no chain of rule firings can verify it, then the step is a non-entailment, meaning the LLM has proposed a move that contradicts with the domain knowledge. The entire trajectory is entailed Π|= ent τ when every step is entailed, i.e. ∀i∈1,...,n : I ∗ |= i analystAt (CB i ) : μ i , μ i ⪰ μ min The entailment-checking problem is to decide whether Π|= ent τ and, when it does not, to return the first failing step Ghidra decompiler libc labels & call graph LLM path generation Domain Knowledge Reasoner (PyReason) Fuzzer analyst paths entailed paths +DK Figure 2: The end-to-end EntailLLM pipeline. Solid boxes are EntailLLM stages, gray boxes its inputs, and dashed boxes place the system in the larger cybersecurity workflow. i ∗ = mini : Π∪ F (τ ) ̸|= ent analystAt (CB i ) : (μ,i). We retain exactly the entailed trajectories. Because I ∗ is computed exactly and in polynomial time under consistency (Theorems 3.2 and 3.4 of (Shakarian et al. 2011)), this deci- sion and the localization of i ∗ are exact rather than heuristic. We focused development on binary analysis because of our target deployment; the framework itself is agnostic to whether the call graph and its labels come from a decompiler or from source, and we leave source-code analysis to future work, studying a complete binary pipeline here. Several domain- specific reasons motivate the choice. Device firmware ships without source, and the compiled artifact is what runs, and optimization and field patching can leave it diverging from any source tree. We consume decompiler output rather than raw bytes because the decompiler recovers the call graph and, from symbol and relocation tables, the imported libc calls we use as labels—beacons that survive stripping, so no debug information is needed. We verify all traversals rather than only paths terminating in a vulnerability: reverse engineers proceed by beacon-driven exploration, recognizing API calls, strings, and constants to form and test hypotheses (Votipka et al. 2020; Sisco, Dudenhofer, and Bryant 2017; Bryant et al. 2011), so restricting attention to vulnerability terminating paths would discard the exploratory structure that makes the output useful and presuppose the analyst’s conclusion. Finally, admitting only domain-entailed paths reduces the volume of spurious paths a human must triage and yields explainable traces an auditor can inspect. 3 System description Figure 2 shows the end-to-end EntailLLM pipeline. The in- put to the system is the analyzed binary’s call graph together with the libc labels of its code blocks. From these inputs, the pipeline proceeds through two core stages—LLM path gen- eration and logical verification—before emitting the paths that survive verification. Labeled call graph. Ghidra’s static analysis recovers the binary’s structural representation. It disassembles the ma- chine code, reconstructs functions and their boundaries, produces decompiled C-like output, and recovers the inter- procedural call graph with cross-references. From symbol and relocation information it resolves the names of imported libc functions (e.g., strcpy, gets, realloc, system), yielding for each function in the call graph the set of libc calls it references. Domain Knowledge (DK). DK is a CWE-focused, code- centric ontology together with instantiated knowledge graphs for CWE-121, CWE-415, and CWE-416. We note that our approach is agnostic to the underlying knowledge graph, and it does not necessarily have to be associated with a CWE. We treat these as fixed and defer the study of knowledge graph extraction and correctness to other studies. The on- tology used defines a layered class hierarchy—from con- crete Beacons, CodeEntities, CodeOperations, and CodePat- terns, through FaultConditions and OutcomeLevelFaults, to CWE-level VulnerabilityClasses—connected by typed rela- tions such as is_a, can_cause, and mitigates. Each graph is populated by automated extraction from technical corpora (reverse-engineering manuals, security advisories, man pages), then refined by schema validation with tar- geted semantic review; together they span 105–188 entities and 232–403 relations over 14–16 relation types (per-graph counts in Appendix). A central modeling choice represents faults as unsafe variants of otherwise-neutral operations—an out_of_bounds_write as an unsafe_variant_of a genericmemory_write. Safe and unsafe behavior coexist in one graph, and the reasoner can express how missing vali- dation turns an ordinary operation into a memory-corruption event. DK also supplies the mapping rules that lift raw libc labels onto its own vocabulary during reasoning, so the la- bels attached to code blocks are expressed in the terms against which paths are later checked for entailment. For the +DK ex- perimental setting, we pre-run the mapping rules and provide the LLM with additional labels. This supplies the generator with DK’s vocabulary but no entailment verdict: the injected labels come only from running the mapping rules over the labels already in the call graph, before any path is generated. Step 1: LLM Path Generation. The first stage proposes candidate analyst paths. Figure 3 shows the prompt structure. The model is given the target CWE and the binary’s label vocabulary, and asked for an ordered sequence of label sub- sets per path. The constraints ensure that the model cannot attribute behavior the binary does not exhibit, and that they are framed as analyst exploration rather than as vulnerability reports, so not every stage needs to be related to the CWE. What the model returns is not yet a path but a template. Beam search realizes each template against the actual call graph, instantiating every stage’s label subset as a concrete func- tion and discarding any template whose sequence cannot be completed as a connected chain. The surviving realizations, deduplicated, are paths that are then input to the reasoner. Step 2: Entailment Checking. Verification is carried out with PyReason (Aditya et al. 2023), an open-source engine for generalized annotated logic that reasons directly over knowledge graphs. It executes the domain knowledge as a logic program and takes the realized paths as input. The logic program comprises of the DKG’s facts and mapping rules together with 42 non-ground rules obtained by instan- tiating a small set of hand-written templates over the graph’s entity–relation–entity triples. The rules fall into three fami- System role You are a security analyst specializing in defensive binary code review. . . generate realistic code-review paths — ordered sequences of semantic function behaviors an analyst would examine when assessing a binary for a specific weakness type. Context CWE: CWE-121, Stack-based Buffer Overflow (id, name, MITRE description). Label vocabulary: groups of libc labels from Ghidra static analysis, each group co-occurring in one code region, e.g. Group 1: [gets, sprintf, strspn] . . . (N groups per binary) +DK. The only change under domain-knowledge en- richment: each group is augmented with reasoner- derived DK labels, e.g. Group 1 becomes [gets, sprintf, strspn, missing_bounds_check, unchecked_memory_write, stack_pointer_overwrite, ...] Constraints Paths must be mutually diverse; framed as analyst exploration (not every stage need relate to the CWE); use only labels from the vocabulary; one label group per stage, no cross-group mixing; minimum 6 edges per path; at most 50 paths. Output format A single JSON object "paths": [...]; each path has path_id, an ordered cluster_sequence of label subsets, an exploration_score in [0, 1], and a short explanation. No text outside the JSON. Technique (varies for different methods) Zero-shot: “Generate the paths directly.” CoT: first emit a label_analysis triage of eachgroup(immediately_suspicious/ worth_investigating / likely_irrelevant), then generate paths with an added per-stage stage_reasoning field. Self-refinement: Three sequential calls sharing the blocks above. (1) Generate an initial path set (as zero-shot). (2) Cri- tique: the paths are returned to the model, which reviews them for CWE relevance, diversity, ignored labels, and score calibration, replying with plain-text feedback. (3) Refine: regenerate an improved path set addressing that critique. Figure 3: Structured prompt template for CWE-121. Full prompts appear in the appendix. lies: label propagation, transitive closure, and analyst traver- sal with step control, of which Table 1 gives one traversal rule and one label-propagation rule. Verifying a single step may require more than one rule: a label-propagation rule may first combine the raw libc labels at one block into a semantic label, a DK mapping rule lift that label onto a DKG concept, and a transitive-closure rule chains relations across several hops, before a traversal rule can fire and validate the analyst’s move. Because PyReason computes the minimal model of the whole program, the reasoning is exact rather than a heuristic graph walk. If no combination of rules can validate a step, that step is non-entailed by the domain knowledge, and we report the first such step (i ∗ of Section 2) along with the full reasoning trace (Figure 6). 4 Experiments Experimental Setup We evaluate across three weakness classes—CWE-121 (stack-based buffer overflow), CWE-415 (double free), and CWE-416 (use-after-free). Standard target binaries (std) are drawn from BinPool (Arasteh et al. 2025), a dataset of Debian binaries curated from historical CVEs; it spans 603 CVEs across 89 CWE classes, so the CWEs we target are rep- resented by real compiled programs whose call graphs and libc usage resemble production firmware. Real-world targets (rw) are firmware extracted from deployed medical devices, confidentially provided, and are the targets EntailLLM is re- quired to analyze in our production environment. Table 2 lists the seven binaries behind the results reported here. Note that ezurio is evaluated under both CWE-121 and CWE-416. Sizes span two orders of magnitude, from gpac (405 nodes, 571 edges) to unsafelib (12,696 nodes, 40,881 edges), exercising the pipeline on both small and large call graphs. Models. We report four models in the paper: Opus-4.8, GPT-5.5, Llama 4 Scout, and Kimi K2.5, spanning propri- etary and open-weight families. Each model is run under all three prompting strategies and in two conditions—without and with domain knowledge supplied to the generator a pri- ori (+DK)—giving 24 configurations per binary. Our initial selection also included Claude Fable 5, but its built-in safe- guards, which redirect queries on certain sensitive topics in- cluding cybersecurity to a less specialized model, were trig- gered by our vulnerability-analysis prompts and prevented its use as a generator. Hyperparameters. Generation uses greedy decoding (t=0.0) throughout, since we evaluate each model’s most likely output rather than a sample. We request N paths = 50 candidate path templates per call, lowered to 20 for Llama 4 Scout, whose 8,192-token output cap truncates a 50-path JSON. Paths must span at least six call-graph edges, lowered to four for gpac, whose 405-node graph is too shallow to admit many six-edge paths. Beam search relaxes to a maxi- mum hop distance of h = 3. Of its parameters only N sol , the number of realized chains kept per surviving template, was tuned—over 1, 2, 5, 10: smaller values degraded results and larger ones raised runtime and LLM cost for no gain, so we use 5. Full settings and rationale are in Appendix. Metrics. For each configuration we report #Total, the num- ber of unique trajectories that survive beam-search realiza- tion, and #Entail, how many of those the domain knowl- edge entails, with Entailment% = #Entail/ #Total× 100 in parentheses. A trajectory that is realized but not entailed is spurious: a path the LLM found plausible that contradicts the domain knowledge. When aggregating over configura- tions we pool #Entail and #Total rather than averaging per- configuration percentages, so that generations are weighted by the evidence they carry. RuleEnglish Description analystAt(CB 2 ) : μ pair ←− ∆t=1 analystAt(CB 1 ) : [0.25, 1] ∧ hasLabel(CB 1 ,L c ):[0.1, 1] ∧ hasLabel(CB 2 ,L e ) : [0.1, 1] ∧ can_cause(L c ,L e ) : [0.1, 1]∧ stepFrom(CB 1 ,CB 2 ) : [1, 1] If the analyst is at code blockCB 1 , which is labeled withL c , and code block CB 2 is labeled with L e , and the domain knowledge asserts L c can_cause L e , then the analyst may advance to CB 2 . hasLabel(X,copy_operation): [0.9, 1] ←− ∆t=0 hasLabel(X,sprintf ): [0.6, 1]∧ hasLabel(X,strcpy) : [0.6, 1] If code block X is observed to use both sprintf and strcpy, it is inferred with at least 90% confidence to per- form a copy_operation. Table 1: Two example rules from the logic program and their description in natural language. μ pair is a pairwise-minimum bound function over annotations in the rule body, applied to the head atom if the rule is fired. Annotations in the body are bounds that must be contained by any possible grounding during the reasoning process. The full program appears in Appendix. CWEBinaryType Nodes Edges CWE-416 gpacstd405571 mupdf-x11 std3,341 11,883 mutoolstd3,569 14,051 CWE-121 htmldocstd1,086 2,815 insulininject rw1,010 2,774 unsafelibrw12,696 40,881 Bothezuriorw1,155 3,322 Table 2: The binaries used across the target CWEs. Compute. All experiments ran on a single server (AMD EPYC 9755, 128 cores, 754 GiB RAM, Ubuntu 24.04, Python 3.10), with every model accessed through a hosted API (Anthropic, OpenAI, AWS Bedrock). Peak resident memory was∼21 MB for the generation stage and∼931 MB for the reasoner, under 0.3% of available RAM, so the pipeline reproduces on commodity hardware. Results and Discussion Tables 3 and 4 report results for the standard and real-world binaries, respectively. Results for binaries with CWE-415 are provided in the Appendix. Domain knowledge improves entailment for both binary types. Pooled entailment increases from 84.4% to 97.8% for standard BinPool binaries and from 71.4% to 98.0% for real-world medical device binaries, and the number of con- figurations at 100% entailment rises from 17 to 38 and from 16 to 39. Across the 94 configurations with output in both conditions, entailment improves in 59, is unchanged in 32, and only decreases in 3. A one-sided Wilcoxon signed-rank test over those 94 paired configurations confirms the shift (W + = 1905, W − = 48, p < 10 −10 ; median +6.5 points); the 32 unchanged configurations were already at 100% entail- ment and are excluded as ties. The result holds for each binary type separately (std p = 2.3× 10 −9 ; rw p = 4.0× 10 −6 ). We note that configurations are not fully independent, since each model and each binary recurs across strategies. Self-refinement with domain knowledge yields the most entailed paths. It produces more entailed paths than any other configuration: 806 on the standard binaries against 584 for zero-shot and 461 for chain-of-thought (CoT), and 639 on the device binaries against 403 and 413. It is also the only strategy for which domain knowledge raises the entailed count along with the rate, adding 182 paths on standard binaries and 209 on device binaries, and doing so in 26 of its 31 individual configurations against 16 of 32 for zero- shot and 12 of 31 for CoT. Self-refinement explores hardest and is correspondingly the least reliable unaided—60.9% entailment on device binaries—so while it has the most to gain, we see that the logical layer successfully utilizes that exploration into verified output. Results translate to real-world binaries. Unaided entail- ment on the device binaries is lower than the BinPool targets (71.4% vs 84.4%), yet under domain knowledge the two con- verge to 98.0% and 97.8%. The system is able to close the gap without per-device tuning of the logic. Stability across runs. To check that these gains are not an artifact of a single run, we repeated the full pipeline ten times and measured the spread in entailment across repetitions. As expected, LLM API responses varied, but domain knowledge both raised entailment and sharply narrowed its spread across runs under all three prompting strategies. Plots are included in the Appendix. 5 EntailLLM Deployment EntailLLM is deployed end-to-end inside a vulnerability- discovery pipeline, occupying the solid boxes of Figure 2. A decompiler upstream supplies the labeled call graph; Entail- LLM proposes candidate analyst trajectories over it, checks each against the domain knowledge, and passes only the en- tailed ones to downstream tooling such as a fuzzer. Results on the three binaries extracted from deployed medical devices are reported in Table 4. EntailLLM runs as an interactive web application served from a REST API. The interface mir- rors the system’s data flow. Figure 1 is a screenshot of the UI showing the graph of an analyzed binary with an LLM- selected trajectory highlighted. Figure 4 shows a snippet of the analyst knowledge graph on the UI. std:gpac (416)std:mupdf-x11 (416) std:mutool (416)std:htmldoc (121) ModelStrategy#Total #Entail(%) #Total #Entail(%) #Total #Entail(%) #Total #Entail(%) Opus-4.8 Zero-Shot33(100)6940(57.97)5238(73.08)7069(98.57) + DK88(100)101101(100)6259(95.16)9898(100) CoT17 16(94.12) 4738(80.85)55(100)8787(100) + DK1616(100)5858(100)1313(100)5555(100) Self-Refinement88(100)6350(79.37)6564(98.46)6260(96.77) + DK1515(100)7170(98.59)8481(96.43)8686(100) GPT-5.5 Zero-Shot125(41.67)6545(69.23)7660(78.95)7271(98.61) + DK11(100)6661(92.42)4442(95.45)4141(100) CoT22(100)4829(60.42)3030(100)4544(97.78) + DK11(100)3030(100)2727(100)4646(100) Self-Refinement 119(81.82)6135(57.38)7748(62.34)7773(94.81) + DK3333(100)6464(100)5957(96.61)8686(100) Llama-4 Scout Zero-Shot66(100)149(64.29)51(20)7873(93.59) + DK11(100)3030(100)44(100)3636(100) CoT29 19(65.52) 7354(73.97)108(80)6565(100) + DK77(100)1818(100)1918(94.74)2222(100) Self-Refinement55(100)1510(66.67)40(0)2826(92.86) + DK1313(100)3333(100)44(100)3131(100) Kimi K2.5 Zero-Shot1313(100)1414(100)3333(100)167 159(95.21) + DK2929(100)3030(100)2323(100)2020(100) CoT66(100)7979(100)102 83(81.37)3232(100) + DK55(100)4444(100)7264(88.89)3737(100) Self-Refinement 1111(100)9051(56.67) 142 114(80.28) 6060(100) + DK22(100)7258(80.56)8279(96.34)9494(100) Table 3: Unique paths realized (#Total) and entailed (#Entail) for the four standard BinPool binaries, each validated against the DK graph of the CWE shown in parentheses, without and with domain knowledge (+DK). Figure 4: An excerpt of the CWE_121 DK graph in the deployed system. Highlighted portions show how entities like function_pointer relate to theCWE_121 vulnerability class through KG relations like manifestation_of. Scalability. Figure 5 shows the scaling capability of the reasoner. Memory remains mostly constant, while runtime scales linearly with steps of reasoning. (a)(b) Figure 5: Plots showing how (a) reasoning time and (b) peak memory, of the reasoner scales for seven binaries. Trace. For every non-entailment, a reasoning trace, shown in Figure 6, is generated. This shows the exact step that was non-entailed by domain knowledge. On click on the UI, a more detailed trace showing the complete reasoning path leading to the non-entailment conclusion is available, and an example is provided in the Appendix. Compute. The system is deployed on an AWS EC2 r5ad.2xlarge instance (8 cores, AMD EPYC 7571, 64 GB RAM)—an order of magnitude smaller than the experi- ment server of Section 4. rw:insulininject (121) rw:unsafelib (121)rw:ezurio (121)rw:ezurio (416) ModelStrategy#Total #Entail(%) #Total #Entail(%) #Total #Entail(%) #Total #Entail(%) Opus-4.8 Zero-Shot124 106(85.48)47 37(78.72) 29 26(89.66)66(100) + DK3333(100)5454(100)4040(100)2727(100) CoT5148(94.12)67 56(83.58) 2828(100)44(100) + DK3126(83.87)42 41(97.62) 4747(100)44(100) Self-Refinement 7370(95.89)69 47(68.12) 3131(100)22(100) + DK2929(100)8781(93.1)9797(100)1616(100) GPT-5.5 Zero-Shot6960(86.96)53 41(77.36) 2421(87.5)2314(60.9) + DK3737(100)3535(100)6161(100)77(100) CoT4534(75.56)35 24(68.57) 15 14(93.33)99(100) + DK2626(100)4242(100)2828(100)66(100) Self-Refinement 7340(54.79)66 42(63.64) 1614(87.5)118(72.7) + DK8783(95.4)6363(100)1616(100)55(100) Llama-4 Scout Zero-Shot127(58.33)44(100)1717(100)33(100) + DK1515(100)77(100)1212(100)55(100) CoT7058(82.86)3024(80)1717(100)55(100) + DK96(66.67)4242(100)1616(100)0NA Self-Refinement 2222(100)159(60)1818(100)1212(100) + DK3030(100)1313(100)99(100)1616(100) Kimi K2.5 Zero-Shot15857(36.08)136 88(64.71) 62 61(98.38) 1414(100) + DK1111(100)31 25(80.65) 2323(100)1111(100) CoT134108(80.6)69 48(69.57) 18 17(94.44)44(100) + DK4141(100)3333(100)4141(100)1414(100) Self-Refinement 1408(5.71)108 60(55.56) 5047(94)0NA + DK4141(100)83 78(93.98) 6262(100)0NA Table 4: Unique paths realized (#Total) and entailed (#Entail) for the three real-world medical-device binaries, each validated against the DK graph of the CWE shown in parentheses, without and with domain knowledge (+DK). Figure 6: The explainable trace showing entailment (first two, in green) and non-entailment (rest, in red) for the analyst path selected by the LLM in Figure 1. 6 Conclusion and Future Work We presented EntailLLM, a deployed system that pairs LLM generation of analyst traversal paths through a software codebase with logic-programming verification against do- main knowledge. A surviving path is therefore not merely a plausible traversal of the function call graph to a lan- guage model, but provably entailed by the encoded do- main knowledge. Aggregated over the weakness classes we examine—four LLMs, three prompting strategies, and seven binaries—domain knowledge raises pooled entailment from 78.0% to 97.9%, decreasing for only 3 of 94 configurations. The strongest configuration is self-refinement with domain knowledge, which raises entailment from 71.0% to 97.4% while increasing the number of entailed paths by 37%, from 1,054 to 1,445. The effect transfers to deployed firmware: unaided entailment on the medical-device binaries is lower than the BinPool targets (71.4% against 84.4%), yet under domain knowledge both converge to 98.0% and 97.8%. The system is able to close the gap without per-device tuning of the logic. We plan to extend this work in three directions. Currently, we exclusively measure logical entailment. While this is an important problem, it would add value to the system if we could also measure exploitability. We have found validated vulnerability labels for real device firmware to be scarce, and we are working to obtain them through coordinated disclo- sure, vendor collaboration, and expert red-teaming so that EntailLLM can be evaluated against confirmed vulnerabili- ties. Second, we are looking to extend the study to include a measure of coverage of the different strategies. Third, we are extending the pipeline to include a corrector module which takes a non-entailed path as an input, and attempts to produce a logically entailed alternative with minimal edits. Acknowledgments This research was, in part, funded by the Advanced Research Projects Agency for Health (ARPA-H). The views and con- clusions contained in this document are those of the authors and should not be interpreted as representing the official poli- cies, either expressed or implied, of the U.S. Government. Research in this paper is related to the invention described in U.S. provisional patent application 64/077,998: Automatic Vulnerability Analysis of Software Consistent with Domain Knowledge. References Aditya, D.; Mukherji, K.; Balasubramanian, S.; Chaudhary, A.; and Shakarian, P. 2023. PyReason: Software for Open World Temporal Logic. In AAAI Spring Symposium: MAKE. Alshiekh, M.; Bloem, R.; Ehlers, R.; Könighofer, B.; Niekum, S.; and Topcu, U. 2018. Safe reinforcement learn- ing via shielding. In Proceedings of the AAAI conference on artificial intelligence, volume 32. Arasteh, S.; Nikitopoulos, G.; Wu, W.-C.; Weideman, N.; Portnoy, A.; Raghothaman, M.; and Hauser, C. 2025. Bin- Pool: A Dataset of Vulnerabilities for Binary Security Anal- ysis. In Proceedings of the 33rd ACM International Con- ference on the Foundations of Software Engineering (FSE Companion). Basque, Z. L.; Doria, S.; Soneji, A.; Gibbs, W.; Doupé, A.; Shoshitaishvili, Y.; Losiouk, E.; Wang, R.; Aonzo, S.; et al. 2026. Decompiling the Synergy: An Empirical Study of Human-LLM Teaming in Software Reverse Engineering. In NDSS. Bryant, A.; Mills, R.; Peterson, G.; and Grimaila, M. 2011. Software reverse engineering as a sensemaking task. Journal of Information Assurance and Security, 6(6): 483–494. Das, A. 2022. Know Your Infusion Pump Vulnerabilities and Secure Your Healthcare Organization. Technical report, Palo Alto Networks Unit 42. Analysis of over 200,000 infu- sion pumps; https://unit42.paloaltonetworks.com/infusion- pump-vulnerabilities/. Hu, P.; Liang, R.; and Chen, K. 2024. DeGPT: Optimizing Decompiler Output with LLM. In NDSS. Kifer, M.; and Subrahmanian, V. 1992. Theory of General- ized Annotated Logic Programming and its Applications. J. Log. Program., 12(3&4): 335–367. Lekssays, A.; Mouhcine, H.; Tran, K.; Yu, T.; and Khalil, I. 2025. LLMxCPG:Context-Aware vulnerability detec- tion through code propertyGraph-Guided large language models. In 34th USENIX Security Symposium (USENIX Se- curity 25), 489–507. Liu, P.; Sun, C.; Zheng, Y.; Feng, X.; Qin, C.; Wang, Y.; Xu, Z.; Li, Z.; Di, P.; Jiang, Y.; et al. 2025. Llm-powered static binary taint analysis. ACM Transactions on Software Engineering and Methodology, 34(3): 1–36. Luo, L.; Li, Y.-F.; Haffari, R.; and Pan, S. 2024a. Reasoning on graphs: Faithful and interpretable large language model reasoning. In International Conference on Learning Repre- sentations, volume 2024, 14400–14423. Luo, L.; Zhao, Z.; Haffari, G.; Li, Y.-F.; Gong, C.; and Pan, S. 2024b. Graph-constrained reasoning: Faithful reasoning on knowledge graphs with large language models. arXiv preprint arXiv:2410.13080. Pan, L.; Albalak, A.; Wang, X.; and Wang, W. 2023. Logic- LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning. In Bouamor, H.; Pino, J.; and Bali, K., eds., Findings of the Association for Computational Linguistics: EMNLP 2023, 3806–3824. Sin- gapore: Association for Computational Linguistics. Redini, N.; Machiry, A.; Wang, R.; Spensky, C.; Continella, A.; Shoshitaishvili, Y.; Kruegel, C.; and Vigna, G. 2020. Karonte: Detecting Insecure Multi-binary Interactions in Embedded Firmware. In 2020 IEEE Symposium on Secu- rity and Privacy (SP), 1544–1561. Shakarian, P.; Parker, A.; Simari, G. I.; and Subrahmanian, V. V. S. 2011. Annotated probabilistic temporal logic. ACM Trans. Comput. Logic, 12(2). Shakarian, P.; and Simari, G. I. 2022. Extensions to Gener- alized Annotated Logic and an Equivalent Neural Architec- ture. In 2022 Fourth International Conference on Transdis- ciplinary AI (TransAI), 63–70. IEEE. Shakarian, P.; Simari, G. I.; and Subrahmanian, V. 2012. An- notated probabilistic temporal logic: Approximate fixpoint implementation. ACM Transactions on Computational Logic (TOCL), 13(2): 1–33. Sheng, Z.; Chen, Z.; Gu, S.; Huang, H.; Gu, G.; and Huang, J. 2025. LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights. ACM Comput. Surv., 58(5). Sisco, Z. D.; Dudenhofer, P. P.; and Bryant, A. R. 2017. Mod- eling information flow for an autonomous agent to support reverse engineering work. The Journal of Defense Modeling and Simulation, 14(3): 245–256. Tan, H.; Luo, Q.; Li, J.; and Zhang, Y. 2024. Llm4decompile: Decompiling binary code with large language models. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, 3473–3487. Ullah, S.; Han, M.; Pujar, S.; Pearce, H.; Coskun, A.; and Stringhini, G. 2024. Llms cannot reliably identify and rea- son about security vulnerabilities (yet?): A comprehensive evaluation, framework, and benchmarks. In 2024 IEEE sym- posium on security and privacy (SP), 862–880. IEEE. Votipka, D.; Rabin, S.; Micinski, K.; Foster, J. S.; and Mazurek, M. L. 2020. An observational investigation of reverse Engineers’ processes. In 29th USENIX Security Symposium (USENIX Security 20), 1875–1892. Xie, D.; Zhang, Z.; Jiang, N.; Xu, X.; Tan, L.; and Zhang, X. 2024. Resym: Harnessing llms to recover variable and data structure symbols from stripped binaries. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 4554–4568. Supplementary Material EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming Contents A Stability and the Random Baseline1 B Aggregate Analysis5 C Results for CWE-4157 D Scalability of the Reasoner8 E Evaluation Binaries8 F Language Models10 G Pipeline Configuration10 H The Complete Logic Program15 IDeployment: Reasoning Trace Example17 J Prompt Templates17 K Domain Knowledge: Ontology and Graphs21 L Extended Related Work22 A Stability and the Random Baseline To check that the reported experimental results are not an artifact of a single run, and to establish what entailment rate an uninformed generator would achieve, we repeated the full pipeline ten times for each of the four models, three prompting strategies, and two conditions on two cases: insulininject under CWE-121 and mupdf-x11 under CWE-416. Alongside these we ran ten independent rounds of random sampling, in which 25 analyst paths are drawn directly from the binary’s call graph, matched to the LLM conditions on path length and on the label-group constraint, so that the only difference is which labels a path visits. Figures 1–6 show the resulting distributions; all settings are otherwise those of the experimental setup in the main paper. Random sampling attains 18.0± 8.5% entailment on insulininject and 46.4± 9.1% on mupdf-x11. Every model–strategy–combination runs on these two targets exceeds random sampling under a one-sided Mann–Whitney test against the ten random rounds (p< 0.05; most at p< 10 −3 ). Pooled over models, unaided generation sits 57– 64 points above random on insulininject and 32–38 points above on mupdf-x11; with domain knowledge the margins widen to 79–81 and 47–51 points. We make two observations. First, in general our use of LLMs generates better paths across strategies, when compared to a completely random selection of paths. Second, Entailment is further improved by the addition of domain knowledge across several runs. Averaged over the twelve model–strategy cells per target, the standard deviation of entailment across runs falls from 10.7 to 4.2 on insulininject and from 9.7 to 5.8 on mupdf-x11. The effect is largest where un- aided behaviour is least reliable: Kimi K2.5 under self-refinement moves from 54.1± 11.3% to 98.3± 2.8% on insulininject, and GPT-5.5 under zero-shot from 66.3± 9.9% to 99.6± 0.8% on mupdf-x11. Several condi- tions become degenerate under +DK, entailing every realized path in all ten runs. Although generation uses greedy decoding, hosted inference APIs are not bit-reproducible; variable request batching perturbs logits enough to flip near-tied argmax decisions, which is the source of the spread reported here. A run contributes no measurement when the model returns no usable path set. This occurs once in 240 runs on insulininject but in 10.4% of runs on mupdf-x11, and is concentrated in Llama-4 Scout, whose 8,192-token output cap truncates longer responses. Aggregated over all conditions, generation failure accounts for 0% of GPT-5.5 runs, 3.9% of Kimi K2.5, 6.7% of Opus-4.8, and 24.4% of Llama-4 Scout. 1 Figure 1: Zero-shot on insulininject (CWE-121). Each box is ten independent runs: grey is random sampling, blue unaided generation, orange the same model with domain knowledge (+DK). Random sampling attains 18.0± 8.5% entailment. A box collapsed to a single line indicates zero variance across runs. Figure 2: Chain-of-thought on insulininject (CWE-121). Conventions as in Figure 1. 2 Figure 3: Self-refinement on insulininject (CWE-121). Figure 4: Zero-shot on mupdf-x11 (CWE-416). Conventions as in Figure 1; random sampling attains 46.4± 9.1%, so the margin over random is smaller on this target than on insulininject. 3 Figure 5: Chain-of-thought on mupdf-x11 (CWE-416). Conventions as in Figure 1. Figure 6: Self-refinement on mupdf-x11 (CWE-416). Conventions as in Figure 1. 4 Entail%#Entailed BinaryType CWE Random base+DK base +DK dropbearstd41518.4 40.291.3132189 mupdf-x11std41646.4 71.296.8454597 mutoolstd41654.8 80.595.5484471 htmldocstd41588.8 92.3 100.0455473 htmldocstd12185.6 97.2 100.0819652 insulininject rw12118.0 63.696.9618378 unsafelibrw12140.0 68.796.6480514 ezuriorw41568.4 80.7 100.04662 ezuriorw41663.2 87.1 100.081111 ezuriorw12184.8 95.7 100.0311452 Table 1: Pooled entailment and entailed-path counts per binary–CWE pair, over all model×strategy configurations, ordered by unaided LLM entailment within each type. Random is the random-sampling mean. Unaided LLM entailment spans 40.2–97.2% with no consistent std/rw pattern, and tracks the random rate closely; under domain knowledge every pair reaches 91.3–100%. B Aggregate Analysis This section aggregates the per-configuration results of the main paper and of Section C along three axes: by bi- nary, by absolute entailed-path count, and by statistical significance. Unless stated otherwise, figures pool #Entail and #Total over configurations rather than averaging per-configuration percentages, so that each configuration is weighted by the evidence it carries. B.1 Per-Binary Results Table 1 pools every model and strategy for each binary–CWE pair. Two things are visible. Entailment for unaided LLM is ordered almost exactly as random sampling is—dropbear is lowest on both, htmldoc highest—so how well a model appears to do without domain knowledge might be correlated to how permissive the domain knowledge is for that binary. An LLM generator raises the floor over random sampling, but under +DK that ordering disappears: all pairs get to similarly high entailment percentage. B.2 Entailed-Path Counts The main paper reports entailment rates. Table 2 gives the underlying counts. We notice that while the entailment rate always increases for all cases, number of entailed paths fluctuates slightly. Self-refinement shows the best improvements both in rate and number of entailments. B.3 Statistical Significance Across all 118 paired configurations, entailment improves in 77, is unchanged in 38, and decreases in 3; over the 94 configurations of the main paper the counts are 59, 32 and 3. Every subset is significant at p< 10 −5 . On CWE-415 no configuration decreases at all, giving W − = 0 and a maximal effect size. Note that, configurations are not fully independent—each model appears in 30 and each binary–CWE pair in 12—so we treat the per-subset tests as descriptive rather than as independent confirmatory comparisons, and apply no multiplicity correction. 5 Entail%#Entailed TypeStrategybase+DKbase+DKcount up stdZero-Shot82.798.182886614/23 stdCoT82.998.577260410/23 stdSelf-Refinement77.496.8847104317/22 rwZero-Shot72.098.65864308/17 rwCoT82.997.95004156/16 rwSelf-Refinement61.897.845067213/17 Table 2: Entailment rate and absolute entailed-path count by binary type and strategy, pooled over all three weakness classes. Count up is the number of configurations in which domain knowledge raised the entailed count, out of those producing output in both conditions. Self-refinement is the only strategy for which the count rises on both target types; chain-of-thought reduces it in both. Subsetn n ′ W + W − p medianr All three CWEs118 80 318060 3.7× 10 −14 +8.83 0.963 CWE-121 & 41694 62 190548 3.8× 10 −11 +6.54 0.951 std68 46 10783 7.1× 10 −14 +8.14 0.994 rw50 34572231.3× 10 −6 +10.73 0.923 CWE-41646 2532416.0× 10 −8 +6.70 0.994 CWE-12148 37667369.7× 10 −7 +6.54 0.898 CWE-41524 1817103.8× 10 −6 +11.88 1.000 Table 3: One-sided Wilcoxon signed-rank tests on paired (baseline, +DK) entailment percentages. n is the number of configurations with output in both conditions, n ′ the number after excluding ties; every tie is a configuration already at 100% entailment without domain knowledge. Median is the change in percentage points; r is the matched-pairs rank-biserial effect size. The second row is the subset reported in the main paper. 6 std:htmldocstd:dropbearrw:ezurio ModelStrategy#Total #Entail(%) #Total #Entail(%) #Total #Entail(%) Opus-4.8 Zero-Shot8070(87.5)3319(57.58)2620(76.92) + DK5858(100)1919(100)2727(100) CoT4541(91.11)31(33.33)22(100) + DK4242(100)66(100)22(100) Self-Refinement5752(91.23)2111(52.38)1312(92.31) + DK8484(100)1717(100)2929(100) GPT-5.5 Zero-Shot5754(94.74)5216(30.77)74(57.14) + DK6666(100)3932(82.05)0NA CoT4942(85.71)2614(53.85)0NA + DK4848(100)2323(100)0NA Self-Refinement8071(88.75)3911(28.21)98(88.89) + DK7171(100)3731(83.78)44(100) Llama-4 Scout Zero-Shot1919(100)55(100)0NA + DK3636(100)2424(100)0NA CoT0NA4411(25)0NA + DK0NA77(100)0NA Self-Refinement0NA0NA0NA + DK0NA0NA0NA Kimi K2.5 Zero-Shot66(100)0NA0NA + DK4747(100)0NA0NA CoT5656(100)3110(32.26)0NA + DK1010(100)77(100)0NA Self-Refinement4444(100)7434(45.95)0NA + DK1111(100)2823(82.14)0NA Table 4: CWE-415 (double free): unique paths realized (#Total) and entailed (#Entail), without and with domain knowledge (+DK). NA marks a configuration that produced no realized paths. C Results for CWE-415 The CWE-415 evaluation uses ezurio, dropbear and htmldoc, introduced in Table 5. dropbear is the second- smallest in the study after gpac. Results follow the pattern of the two classes reported in the main paper. Pooled entailment rises from 72.1% to 97.6%, entailment improves in 18 of the 24 configurations that produced output in both conditions, is unchanged in 6, and decreases in none. The gain is concentrated where unaided LLM entailment is weakest: dropbear moves from 40.2% to 91.3%, while htmldoc and ezurio start at 92.3% and 80.7% and both reach 100%. Unlike CWE-121 and CWE-416, the entailed count also rises in aggregate here, from 633 to 724 paths. We note that ezurio yields output in only 9 of its 24 configurations—all of Opus-4.8 and three cells of GPT- 5.5. Llama-4 Scout produces nothing at all under self-refinement on any binary, and nothing on htmldoc under chain-of-thought; Kimi K2.5 produces nothing on dropbear under zero-shot. These are the generation failures characterised in Section A, and they are the reason CWE-415 is reported here rather than in the main paper. These results go to show how LLM results can vary significantly between models, and how larger state-of-the-art models often outperform other models. 7 Figure 7: Reasoning runtime versus number of reasoning time steps for all CWE-121 (solid) and CWE-416 (dashed) binaries. D Scalability of the Reasoner Figures 7 and 8 report reasoner runtime and peak memory as the number of reasoning time steps grows, for all CWE-121 (solid) and CWE-416 (dashed) binaries, including rw:ezurio under CWE-416. The horizontal axis is PyReason’s time setting, which we fix to the number of steps in an analyst path: verifying a trajectory of n steps requires the reasoner to run for n time points, so this axis is the length of the trajectory being checked. Each point is an independent run in a fresh reasoner process with time fixed to the value shown. Runtime grows linearly with the number of time steps for every binary, so the slope of each line is the cost of one additional reasoning step. This per-step cost is found to be proportional to how many groundings the reasoner produces at each step. The slopes actually order the binaries by grounding volume: rw:unsafelib produces the most groundings per step (∼1,760) and has the steepest slope (∼1.4 s per step), while std:gpac produces the fewest and has the shallowest. Peak memory is flat at roughly 880 MB for every binary because the footprint is dominated by fixed startup costs—the Python interpreter, the JIT-compiled reasoner, and the loaded rules and knowledge graph—all done before any reasoning occurs. The additional memory per time step of reasoning is small by comparison: running six steps instead of one raises peak RSS by at most ∼16 MB, about 2% of the baseline. The small spread across binaries (878–931 MB) is also found to be proportional to the grounding volume. For deployment, we note that verification cost scales with trajectory length and with the grounding volume of the binary–DKG pairing, not with the number of trajectories checked, since each is verified independently and the program is restarted after every run. As the memory footprint is dominated by startup, a reasoner process sized for the largest binary is then sized for all of them. The deployment instance of 64 GB (Section 5 of the main paper) has roughly 70× the peak requirement of any single run. E Evaluation Binaries Table 5 lists function call graphs for every binary used in the study. Graphs are recovered by Ghidra and restricted to the libc subset: functions that reference at least one imported libc routine, together with the calls among them, since these are the nodes over which entailment is defined. Seven of the eight appear in the main results; dropbear is used only for CWE-415 (Section C). 8 Figure 8: Peak resident set size (RSS) after reasoning versus number of reasoning time steps for all CWE-121 (solid) and CWE-416 (dashed) binaries. The footprint is dominated by fixed startup cost. BinaryTypeCWENodesEdges Standard (BinPool) gpacstd416405571 dropbearstd4158162,416 htmldocstd121, 4151,0862,815 mupdf-x11std4163,34111,883 mutoolstd4163,56914,051 Real-world (medical device) insulininjectrw1211,0102,774 ezuriorw121, 415, 4161,1553,322 unsafelibrw12112,69640,881 Table 5: All binary call graphs, grouped by target type and ordered by size. Sizes span two orders of magnitude, from 405 to 12,696 nodes. 9 Model limitsOur settings ModelRouteContext Max out max-tok n-paths$/1M Opus-4.8Anthropic1,000,000128,00085,53650 5.00 / 25.00 GPT-5.5OpenAI1,050,000128,00085,53650 5.00 / 30.00 Kimi K2.5AWS Bedrock256,00016,38416,384500.60 / 3.00 Llama-4 Scout AWS Bedrock (US)128,0008,1928,192200.17 / 0.66 Table 6: Language models used in our experiments. Context and Max out are the model’s own limits; max-tok and n-paths are the values we request. For Kimi K2.5 and Llama-4 Scout the requested budget equals the model’s output cap, so the cap binds. Prices are per million input / output tokens at the time of the experiments. Temperature is 0.0 throughout. F Language Models Table 6 lists the four models used, together with the routing and generation settings under which each was called. All calls go through litellm, which selects the API key by model-id prefix, and all use greedy decoding (t=0.0). G Pipeline Configuration This section gives the full parameter settings, then reports the two measurements that justify the one parameter we tuned: how many templates a model returns and how many of those the beam search can realize (Section G.2), and what changes when the realization budget is doubled (Section G.3). G.1 Hyperparameters The full hyperparameter values and rationale are shown in Table 7. G.2 Template Generation and Realization A model does not return paths directly: it returns templates, ordered sequences of label subsets, which beam search must instantiate against the actual call graph. Tables 8 and 9 report this funnel per configuration for CWE-121 and CWE-416. Of 8,160 templates requested across the two classes, models returned 4,291 (52.6%), of which 2,683 (62.4%) realized as at least one connected chain, ultimately yielding 7,671 unique paths—a mean of 2.86 per surviving template, below the cap of N sol = 5 because deduplication removes repeats. Roughly a third of what a model produces therefore reaches the reasoner. The rest is discarded by the structural filter before any semantic check is applied. Domain knowledge is provided before generation rather than on realization. The return rate rises from 45.6% to 57.2% under +DK. So, enrichment makes models propose more. G.3 Sensitivity to the Beam-Search Budget N sol , the number of realized chains kept per surviving template, was the only beam-search parameter tuned. Table 10 repeats the entire CWE-121 evaluation at N sol = 10, with every other setting unchanged. Doubling the budget realizes roughly 1.7× as many paths—4,884 against 2,838 without domain knowledge, and 3,413 against 2,026 with it. But, pooled entailment under +DK is 97.2% at N sol = 10 against 98.5% at N sol = 5. The effect of domain knowledge is therefore not dependent on how many realizations the beam search retains, and the smaller budget is preferred on runtime and API cost. 10 ParameterValueRationale Generation (LLM) temperature0.0Greedy decoding, to evaluate each model’s most likely output rather than a sample. n-paths50 (Llama-4: 20)Candidate path templates requested per call.Llama- 4 Scout is reduced to 20 because its 8,192-token output cap truncates a 50-path JSON, most often under chain-of- thought. max-tokens85,536Opus-4.8 and GPT-5.5 16,384Kimi K2.5 (equals the model’s output cap) 8,192Llama-4 Scout (equals the model’s output cap) Beam-search realization h (max hop distance)3Default, not tuned. beam-width100Default, not tuned. max-back-hops3Default, not tuned. hop-weight0.1Default, not tuned; score penalty per hop beyond the first. bh-weight0.2Default, not tuned; score penalty per back-hop. extra-label-weight1.0Default, not tuned; penalty per extra label on a matched node, favouring tight matches. N sol 5Realized trajectories emitted per surviving template. Var- ied over 1, 2, 5, 10; Smaller values do not generate enough results. N = 10 raised runtime, enrichment con- text size, and API cost without providing comparable en- tailment improvements (Section G.3). Path constraint MINPATHEDGES6 (gpac: 4)Minimum path length in edges. Lowered to 4 for gpac, whose 405-node call graph is too shallow to admit many six-edge paths. Table 7: Hyperparameter values and rationale. 11 rw:insulininjectrw:unsafelibrw:ezuriostd:htmldoc ModelStrategy#Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol Opus-4.8 Zero-Shot50252550201550159501515 + DK503017504036503025505044 CoT50121250151550129502019 + DK502012502020502016502523 Self-Refinement50181850181750159501716 + DK503217505046505043504040 GPT-5.5 Zero-Shot501515501513501510501815 + DK501512502017501816501515 CoT501095012950125501010 + DK5012950121250108501212 Self-Refinement50161650201950158502019 + DK50202050202050204502020 Llama-4 Scout Zero-Shot202052020420207202018 + DK202092020220204202018 CoT20201620201520204201515 + DK2033202018202010201515 Self-Refinement20206202042020520209 + DK2020172020920203202011 Kimi K2.5 Zero-Shot505049504035502018505039 + DK505055030155050550505 CoT5030305020145015750308 + DK50151150509502514502010 Self-Refinement504039503030505028502514 + DK505019504039505018505028 Table 8: Template generation and realization counts for CWE-121. #Req is the number of path templates requested, #Ret the number the model returned, and #Sol the number of returned templates that beam search realized as at least one connected call-graph chain. The unique paths that result from #Sol appear as #Total in the main results tables. 12 std:gpacstd:mupdf-x11std:mutoolrw:ezurio ModelStrategy#Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol Opus-4.8 Zero-Shot5010250151550121150154 + DK503019504038503030505023 CoT501055010105012150123 + DK502016502020502016502014 Self-Refinement5014550151550151550122 + DK502112502525505050505030 GPT-5.5 Zero-Shot5015450151350181750166 + DK5020150201950121250152 CoT501215012115010850123 + DK5015150121150121250122 Self-Refinement5016350202050201950205 + DK50261550202050222250201 Llama-4 Scout Zero-Shot20202201542015220102 + DK202052010102010620102 CoT20201020201920422051 + DK20332020202020182030 Self-Refinement20205202052020120205 + DK20201220201820202202020 Kimi K2.5 Zero-Shot50505505045050750208 + DK50452950301150201050156 CoT5015350201950303050151 + DK50156502017502020505023 Self-Refinement5012550403850505050200 + DK5025650302850302750200 Table 9: Template generation and realization counts for CWE-416. Columns as in Table 8. 13 rw:insulininjectrw:unsafelibrw:ezuriostd:htmldoc ModelStrategy#Total #Entail(%) #Total #Entail(%) #Total #Entail(%) #Total #Entail(%) Opus-4.8 Zero-Shot233214(91.85)7863(80.77)3835(92.11)138136(98.55) + DK5656(100)10799(92.52)131131(100)6868(100) CoT10093(93)123107(86.99)3434(100)169169(100) + DK4343(100)9795(97.94)8484(100)111111(100) Self-Refinement127124(97.64)11879(66.95)3838(100)117114(97.44) + DK9291(98.91)126117(92.86)102102(100)167167(100) GPT-5.5 Zero-Shot129114(88.37)8268(82.93)2925(86.21)138137(99.28) + DK3535(100)6868(100)2525(100)8686(100) CoT8565(76.47)5843(74.14)1817(94.44)7574(98.67) + DK2626(100)6262(100)4242(100)6666(100) Self-Refinement13597(71.85)9758(59.79)1614(87.5)142136(95.77) + DK4747(100)9592(96.84)2727(100)134134(100) Llama-4 Scout Zero-Shot2212(54.55)44(100)2929(100)144136(94.44) + DK1515(100)5554(98.18)9990(90.9)4747(100) CoT136123(90.44)6248(77.42)1717(100)130130(100) + DK5956(94.92)4040(100)1515(100)5151(100) Self-Refinement3333(100)2013(65)1818(100)5451(94.44) + DK3737(100)7335(47.94)99(100)7373(100) Kimi K2.5 Zero-Shot296184(62.16)247175(70.85)1414(100)288272(94.44) + DK66(100)5144(86.27)5656(100)4949(100) CoT239194(81.17)13489(66.42)2322(95.65)5050(100) + DK5250(96.15)5454(100)9797(100)6161(100) Self-Refinement27793(33.57)171105(61.4)6356(88.89)9696(100) + DK6260(96.77)225215(95.56)126126(100)104104(100) Table 10: CWE-121 with N sol = 10: unique paths realized (#Total) and entailed (#Entail), without and with domain knowledge (+DK). Pooled entailment rises from 82.3% to 97.2%, against 78.5% to 98.5% at N sol = 5. 14 H The Complete Logic Program The programΠ consists of the 42 non-ground rules listed below, reproduced verbatim in PyReason syntax. The head annotation pairedminimumboundsannfn is the annotation functionμ pair of the main paper: it assigns the head the componentwise minimum of the bounds satisfied by the body clauses, so a step is never given a confidence higher than its weakest supporting evidence. The same program is shared across all three CWEs; only the knowledge graph the reasoner reasons with changes. Throughout the experiments, we take the minimum admissible boundμ min of the main paper’s problem formulation to be [0.25, 1], matching the guard on analystAt(CB1) in the traversal rules: an analyst is considered present at a block if its bound is at least [0.25, 1]. H.1 Analyst-Traversal and Step-Control Rules (8) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lcause):[0.1,1], hasLabel(CB2, Leffect):[0.1,1], can_cause(Lcause, Leffect):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lcontrib):[0.1,1], hasLabel(CB2, Lfault):[0.1,1], contributes_to(Lcontrib, Lfault):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lop):[0.1,1], hasLabel(CB2, Lderived):[0.1,1], derives(Lop, Lderived):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lunsafe):[0.1,1], hasLabel(CB2, Lsafe_concept):[0.1,1], unsafe_variant_of(Lunsafe, Lsafe_concept):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lfault):[0.1,1], hasLabel(CB2, Lcwe):[0.1,1], manifestation_of(Lfault, Lcwe):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lfunc):[0.1,1], hasLabel(CB2, Lop):[0.1,1], implements(Lfunc, Lop):[0.1,1], stepFrom(CB1, CB2) future(Y) <-1 stepFrom(X,Y), analystAt(X):[0.01,1] ~stepFrom(X,Y) <- future(Y), ~analystAt(Y):[0.25,1], ~analystAt(X) The six traversal rules advance the analyst one step per time point (<-1): if the analyst occupies CB1 with lower bound at least 0.25 and the trajectory contains the edge stepFrom(CB1, CB2), the step is entailed whenever some knowledge-graph relation (can cause, contributesto, derives, unsafevariantof, manifestationof, implements) links a label observed on CB1 to a label observed on CB2. The clause thresholds ([0.1, 1] on hasLabel and on the relation, [0.25, 1] on analystAt) act only as gates; the bound assigned to the head is computed by paired minimumboundsannfn, which recovers the (cause, effect) label pairing imposed by the relation clause. For each grounded relation edge it takes the elementwise minimum of the relation’s bound and the hasLabel bounds of the matching labels on the two code blocks, so inference is never mixed across unrelated label pairs, and annotates analystAt(CB2) with the pair attaining the highest lower bound. If no pair meets the threshold, the head retains its default [0, 1], complete uncertainty, and the step is not entailed. The final two rules make that failure explicit for reporting. future(Y) marks the block one step ahead on the analyst trajectory; if the analyst never reaches there, the negation rule drives stepFrom(X,Y) toward [0, 0], contradicting the trajectory edge asserted at [1, 1]. The two formulations converge. The head failing to reachμ min and the resulting bound conflict on stepFrom identify the same step, and is shown in the reasoning trace of Figure 9. 15 H.2 Propagation Rules (28) H.2.1 Label-Propagation Rules (13) These map raw libc labels to higher-level semantic labels through conjunctive clauses. A single libc call is often ambiguous, but the combination is not. Head annotations encode confidence in how strongly a combination implies the semantic label. hasLabel(X, memory_write):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, memmove):[0.6,1] hasLabel(X, memory_write):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, memory_write):[1.0,1] <- hasLabel(X, sprintf):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, memory_write):[0.778,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, memset):[0.6,1] hasLabel(X, memory_write):[0.714,1] <- hasLabel(X, memmove):[0.6,1], hasLabel(X, memset):[0.6,1] hasLabel(X, memory_write):[0.5,1] <- hasLabel(X, memset):[0.6,1], hasLabel(X, snprintf):[0.6,1] hasLabel(X, memory_write):[0.429,1] <- hasLabel(X, memset):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, memory_write):[0.2,1] <- hasLabel(X, fgets):[0.6,1], hasLabel(X, memset):[0.6,1] hasLabel(X, copy_operation):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, memmove):[0.6,1] hasLabel(X, copy_operation):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, copy_operation):[0.9,1] <- hasLabel(X, sprintf):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, input_operation):[1.0,1] <- hasLabel(X, fgets):[0.6,1], hasLabel(X, sscanf):[0.6,1] hasLabel(X, size):[1.0,1] <- hasLabel(X, destination_size_validation):[0.6,1], hasLabel(X, length_calculation):[0.6,1] H.2.2 Relation-Propagation Rules (15) These connect a code block’s observed labels to the domain concepts of the DKG through the graph’s typed relations. Most relations are instantiated in both directions with different bounds, so that strong and weak evidence propagate asymmetrically. hasLabel(CB, Lsemantic):[0.84,1] <-0 hasLabel(CB, Lbinary_feature):[0.7,1], evidence_of(Lbinary_feature, Lsemantic) hasLabel(CB, Lbinary_feature):[0.36,1] <-0 hasLabel(CB, Lsemantic):[0.95,1], evidence_of(Lbinary_feature, Lsemantic) hasLabel(CB, Lparent):[1,1] <-0 hasLabel(CB, Lchild):[0.7,1], is_a(Lchild, Lparent) hasLabel(CB, Lchild):[0.1,1] <-0 hasLabel(CB, Lparent):[0.95,1], is_a(Lchild, Lparent) hasLabel(CB, Lop):[0.87,1] <-0 hasLabel(CB, Lpart):[0.7,1], required_component_of(Lpart, Lop) hasLabel(CB, Lop):[0.25,1] <-0 hasLabel(CB, Lpart):[0.95,1], required_component_of(Lpart, Lop) hasLabel(CB, Lop):[0.32,1] <-0 hasLabel(CB, Lpart):[0.95,1], informative_component_of(Lpart, Lop) hasLabel(CB, Lpart):[0.29,1] <-0 hasLabel(CB, Lop):[0.95,1], informative_component_of(Lpart, Lop) hasLabel(CB, Lop):[0.15,1] <-0 hasLabel(CB, Lpart):[0.95,1], incidental_component_of(Lpart, Lop) hasLabel(CB, Lpart):[0.2,1] <-0 hasLabel(CB, Lop):[0.95,1], incidental_component_of(Lpart, Lop) hasLabel(CB, Lrealization):[0.9,1] <-0 hasLabel(CB, Lop):[0.7,1], possible_realization(Lrealization, Lop) hasLabel(CB, Lop):[0.4,1] <-0 hasLabel(CB, Lrealization):[0.9,1], possible_realization(Lrealization, Lop) hasLabel(CB, Lconcept):[0.41,1] <-0 hasLabel(CB, Lop):[0.9,1], involves(Lop, Lconcept) 16 hasLabel(CB, Lused):[0.3,1] <-0 hasLabel(CB, Lop):[0.95,1], may_use(Lop, Lused) hasLabel(CB, Lop):[0.18,1] <-0 hasLabel(CB, Lused):[0.95,1], may_use(Lop, Lused) H.3 Transitive-Closure Rules (6) These make a DKG relation transitive where its semantics warrant it, letting the reasoner chain multi-hop causal and compositional relationships that no single edge states explicitly. can_cause(E1, E3) <- can_cause(E1, E2), can_cause(E2, E3) contributes_to(E1, E3) <- contributes_to(E1, E2), contributes_to(E2, E3) derives(E1, E3) <- derives(E1, E2), derives(E2, E3) involves(E1, E3) <- involves(E1, E2), involves(E2, E3) is_a(E1, E3) <- is_a(E1, E2), is_a(E2, E3) required_component_of(E1, E3) <- required_component_of(E1, E2), required_component_of(E2, E3) I Deployment: Reasoning Trace Example A reasoning trace accompanies every non-entailment inference. A tree recording which observations and which rule firings produced each bound, rooted at the first step the domain knowledge does not entail. Figure 9 shows the trace for the running example of the main paper, in which an LLM assigns memset to the memory-management class and then assumes it can perform an integer size calculation. The leaves are facts of two kinds: libc hasLabel observations on the code blocks along the path (here userInput and scanf), and the stepFrom edges of the proposed trajectory itself, annotated [1, 1]. Interior nodes are rule firings. A relation-propagation rule fires on the conjunction of observed labels to derive the higher-level stack basedbufferoverflowrisk label, which is what bridges code-level evidence to the CWE121 domain-knowledge graph; traversal and step-control rules then advance the analyst along the prefix that the domain knowledge does entail. At the root, no relation in the domain-knowledge graph connects the labels at the two blocks, so no traversal rule fires and analystAt at that block never reachesμ min . The step-control rule of Section H then makes the corresponding stepFrom bound [0, 0], contradicting the [1, 1] set from the trajectory, and the program reports the conflict as a non-entailment at that step. Because every node records both its bound update and the fact or rule that caused it, an analyst can audit exactly which observations and which rule firings reject the step, rather than receiving an unexplained conclusion. J Prompt Templates All three prompting techniques share an identical base prompt: the system role, the CWE information, the Ghidra label vocabulary, and the constraint and output-format blocks. The techniques differ only in a final technique-specific block and, for self-refinement, in a multi-call structure. We therefore give the base prompt once (Section J.1) and then the per-technique additions (Sections J.2–J.4). The transcript below is the CWE-416 prompt for gpac; the main paper shows the abridged CWE-121 form. Three fields are substituted per target: the CWE information, the label vocabulary, and MIN PATHEDGES, which is 4 here because gpac’s call graph is too shallow for six-edge paths and 6 for every other binary (Section G.1). Under domain-knowledge enrichment (+DK) the only change is that each label group in the vocabulary is augmented with reasoner-derived DK labels (Section J.5); every other block is byte-identical. Prompts are reproduced verbatim. J.1 Shared Base Prompt Sent in full on every call, including each of the three self-refinement calls. Label groups beyond the three shown are omitted for space; a binary typically yields tens of groups. 17 Figure 9: The reasoning trace behind a non-entailment inference, for the analyst path of the running example in the main paper. Green leaves are facts (libc label observations and the trajectory’s own stepFrom edges); orange nodes are rule derivations, each annotated with the bound it assigns; the red root is the first step no domain-knowledge relation entails. Each node records the fact or rule responsible for its bound update. === SYSTEM PROMPT === You are a security analyst specializing in defensive binary code review. You reason about which sequences of function behaviors in a binary are relevant to a given software weakness class (CWE), so that code regions worth reviewing can be prioritized for detection and remediation. Your task is to generate realistic code-review paths - ordered sequences of semantic function behaviors an analyst would examine when assessing a binary for a specific weakness type. These paths describe which code a reviewer would inspect during analysis, not necessarily what they would find. === USER PROMPT === CWE Information: CWE ID: CWE-416 CWE Name: Use After Free CWE Description: Use After Free - a program continues to use a pointer after the memory it references has been freed, allowing an attacker to control the freed region and influence program behavior or execution. Binary Static Analysis Labels: The following are groups of function labels detected via Ghidra static analysis of the target binary. Each group represents functions that co-occur in the same code region. Use these as your label vocabulary when constructing path stages: Group 1: [’__stack_chk_fail’, ’abort’, ’clock’, ’exit’, ’exp’, ’fwrite’, ’gmtime’, ’log’, ’realloc’, ’remove’, ’scanf’, ’sin’, ’sprintf’, ’strcat’, ’strcpy’, ’strtol’, ’vsnprintf’, ’vsprintf’] Group 2: [’abort’, ’fseek’, ’ftell’, ’fwrite’, ’vfprintf’] Group 3: [’__stack_chk_fail’, ’clock’, ’exit’, ’fputs’, ’fread’, ’fseek’, ’ftell’, ’fwrite’, ’log’, ’sprintf’, ’strcat’, ’strcpy’, ’strrchr’, ’strtol’] Path Diversity: The generated exploration paths should be meaningfully different from each other. Each path should represent a different way an analyst might examine the code 18 while assessing it for the mentioned weakness. Exploration Path Framing: Each path represents the exploration journey of a human expert or security researcher navigating through the binary, looking for potential vulnerabilities. Not every stage in the path needs to directly relate to CWE-416 - a human expert would follow interesting code paths, investigate suspicious functions, explore memory management patterns, and sometimes backtrack from dead ends. The path reflects how someone would realistically explore the code, not just the shortest route to a vulnerability. Label Vocabulary Constraint: Every label used in every stage subset must come from the provided label vocabularies. Do not use any label that does not appear in the provided vocabularies. Label Group Selection Constraint: At each stage of the path, select one label group from the provided groups and use only those labels from that group that makes sense for that stage. All labels within a single stage must come from the same group. Minimum Path Length: Each generated path must contain at least 4 edges (transitions between stages). Paths with fewer than 4 edges are invalid. Per Path Reasoning: For each exploration path, provide a brief explanation under the key ’explanation’ describing the analyst’s reasoning - how this sequence of labels represents a plausible region of code to examine when assessing the target weakness. Exploration Likelihood Score: For each path, provide a score between 0.0 and 1.0 under the key ’exploration_score’ reflecting how likely an analyst would examine this trajectory when reviewing the binary. A score of 1.0 means an analyst would very likely follow this path, 0.0 means unlikely. Number of Paths: Generate maximum 50 exploration paths. Each path must be unique and independently valid. You can also decide to generate fewer than 50 paths if you determine that there are not that many high-quality, distinct paths to generate. Do not generate more than 50 paths. Free Label Subset Path Output: Return your response as a valid JSON object with the following structure: "paths": [ "path_id": <integer>, "cluster_sequence": [ ["label1", "label2", ...], ["label1", ...], ... ], "vulnerability_score": <float between 0.0 and 1.0>, "exploration_score": <float between 0.0 and 1.0>, "explanation": "<2 sentence explanation of why an analyst would examine this path when assessing the target weakness>" ] Each entry in cluster_sequence is a subset of one or more labels chosen freely from any of the provided label sets. Labels can be mixed from different sets 19 within the same stage. Do not include any text outside the JSON object. Do not use markdown formatting or code blocks. J.2 Zero-Shot Appended to the base prompt; a single call. Zero-Shot: Using the information provided above, generate exploration paths for the given CWE. Do not ask for clarification. Generate the paths directly. J.3 Chain-of-Thought Appended to the base prompt; a single call returning one JSON object in which a triage phase precedes generation. Chain-of-Thought (CoT): Reason step by step before answering, and return everything as a single JSON object that extends the output structure specified above. Phase 1 - Label analysis. Before generating any paths, examine the label groups provided above. Produce a top-level "label_analysis" object that, for each group you consider relevant, classifies its labels into one of three categories for the target CWE: "immediately_suspicious", "worth_investigating", or "likely_irrelevant", each with a one-line justification. Use this triage to decide which labels to choose for path stages. Phase 2 - Path generation. Then generate the exploration paths. Keep every field required above unchanged (path_id, cluster_sequence, vulnerability_score, exploration_score, explanation). Additionally, for each path include a "stage_reasoning" field: an array with one entry per stage in cluster_sequence, where entry i explains, stage by stage, what the analyst infers from the combination of labels present at stage i - what seeing those labels together in the same code region suggests, and why that leads to the next stage. The final JSON object must have this shape: "label_analysis": ... , "paths": [ <all fields required above>, "stage_reasoning": ["stage 0 inference", ...] ] Do not ask for clarification. Do not include any text outside the JSON object. Do not use markdown formatting or code blocks. Generate the analysis and paths directly. J.4 Self-Refinement A three-call loop. Every call re-sends the full base prompt; only the additions are shown. Call 1 is identical to zero-shot, so the loop’s cost is three generations per configuration. --- Call 1: Generate (identical to zero-shot) --- Iterative Self-Refinement: Using the information provided above, generate exploration paths for the given CWE. Do not ask for clarification. Generate the paths directly. --- Call 2: Critique --- [base prompt + Call-1 instruction], then: --- Here are the exploration paths you generated: [ <JSON path set from Call 1> ] 20 Critically review these paths for the target CWE. What is wrong with them? Are they diverse enough? Are important labels being ignored? Are the vulnerability and exploration scores well calibrated? Respond with concise verbal feedback in plain text only - do not output JSON, code blocks, or paths. --- Call 3: Refine --- [base prompt + Call-1 instruction], then: --- Here are your original exploration paths: [ <JSON path set from Call 1> ] Here is feedback on them: [ <plain-text critique from Call 2> ] Now generate improved exploration paths that address this feedback. Return the refined paths using exactly the same JSON output format specified above. Do not include any text outside the JSON object. Do not use markdown formatting or code blocks. J.5 Domain-Knowledge Enrichment Under +DK the label vocabulary is the only block that changes. Before generation we run the domain knowledge’s mapping rules over the libc labels already present on each code block and append the derived labels to that block’s group. The generator therefore receives DK’s vocabulary but no entailment verdict, and the reasoner has not yet seen any trajectory at this point. A group that reads Group 1: [’gets’, ’sprintf’, ’strspn’] in the baseline condition becomes Group 1: [’gets’, ’sprintf’, ’strspn’, ’missing_bounds_check’, ’unchecked_memory_write’, ’stack_pointer_overwrite’, ...] under +DK. The added terms are DKG concepts rather than libc symbols, so the model can express a stage in the vocabulary the reasoner will later check against, instead of only in terms of the raw calls Ghidra recovered. K Domain Knowledge: Ontology and Graphs The domain knowledge is a CWE-focused, code-centric ontology together with a set of instantiated knowledge graphs, one per weakness class. The ontology defines a layered class hierarchy—from concrete Beacons, CodeEnti- ties, CodeOperations and CodePatterns, through FaultConditions and OutcomeLevelFaults, to CWE-level Vulnera- bilityClasses, connected by a fixed set of typed relations (e.g. is a, unsafevariantof, cancause, mitigates). A central modelling choice is to represent faults as unsafe variants of otherwise-neutral operations: an out ofboundswrite is an unsafevariantof a generic memorywrite. Safe and unsafe behaviour therefore coexist in a single graph, and the reasoner can express how missing or incorrect validation turns an ordinary opera- tion into a memory-corruption event. The layering supports reasoning in both directions: forward, from observable beacons up through the class hierarchy to a CWE-level determination, and backward, from a hypothesised classifi- cation down to the code-level evidence that would confirm or refute it. The relation-propagation rules of Section H implement exactly this, which is why most relations are instantiated in both directions with asymmetric bounds. Each graph is populated initially by automated extraction from technical corpora (reverse-engineering manuals, security advisories, man pages), then refined by automated schema validation with targeted semantic review. We treat the resulting graphs as fixed and assumed correct throughout; the extraction and validation of domain-knowledge graphs is a separate problem that this work does not address. 21 EntitiesRelations DK graphClassesTotalTypesTotalRel./ent. CWE-121 (stack buffer overflow)9188164032.14 CWE-415 (double free)8105143183.03 CWE-416 (use-after-free)8111142322.09 Table 11: The three per-CWE knowledge graphs. All graphs are directed. Classes counts ontology classes instanti- ated in the graph, Types the distinct relation types used, and Rel./ent. the mean number of relations per entity. K.1 Graph Statistics The 16 relation types, taken as the union across graphs, are contributes to, cancause, manifestationof, unsafevariantof, involves, implements, validates, mayuse, derives, possiblerealization, isa, evidenceof, mitigates, requiredcomponentof, informativecomponentof and incidentalcomponentof. CWE-121 uses all 16; CWE-415 and CWE-416 use 14 each, CWE-415 omitting derives and involves and CWE-416 omitting derives and unsafe variantof. Six of the 16 are made transi- tive by the closure rules of Section H, and six adjudicate analyst steps in the traversal rules. L Extended Related Work L.1 LLMs for Vulnerability Detection LLMs are increasingly applied to software vulnerability detection across source code, repair, and binaries; recent surveys chart the rapid growth of this area since 2023 and catalogue the models, datasets, and evaluation setups now in use Sheng et al. (2025). A recurring finding, however, is that current models are not yet dependable on their own: a comprehensive benchmarking study by Ullah et al. Ullah et al. (2024) concludes that LLMs cannot yet reliably identify or reason about security vulnerabilities. Work that does report gains typically pairs the LLM with structure rather than trusting it in isolation—LLMxCPG, for example, uses code-property-graph slices to focus an LLM on vulnerability-relevant context Lekssays et al. (2025). This unreliability is the gap our work targets: rather than treating LLM output as an answer, we treat each proposed analyst path as a hypothesis to be checked against domain knowledge, and we operate on decompiled binaries because source is unavailable for the medical-device firmware we analyse. L.2 LLMs for Binary Reverse Engineering A fast-growing line of work applies LLMs directly to stripped or decompiled binaries: LLM4Decompile trains models to recover source-like code from assembly Tan et al. (2024); ReSym recovers variable and data-structure symbols from stripped binaries Xie et al. (2024); and DeGPT uses an LLM to refine and explain decompiler out- put Hu, Liang, and Chen (2024). Most relevant to our setting, an empirical study of human–LLM teaming in reverse engineering shows that LLMs can accelerate analyst comprehension but also mislead when their suggestions go unchecked Basque et al. (2026). These efforts improve the readability or recovered structure of a binary; they do not verify that an analyst’s reasoning over that binary is consistent with what is known about the vulnerability class. Our contribution is complementary and sits downstream: we take the recovered call-graph structure and libc labels as input and add a logical verification layer over the analyst paths reasoned on top of them. L.3 Logic and Program Analysis for Binary Vulnerability Discovery Classical binary vulnerability discovery relies on static analysis and taint tracking. Karonte propagates taint across the multiple binaries of a firmware image to surface insecure interactions, and its authors note that whole-firmware analysis without such cross-binary reasoning produces overwhelming alert volumes Redini et al. (2020). More 22 recently, LATTE couples an LLM with binary taint analysis, automating the taint-propagation and inspection rules that previously required manual expert customisation and reporting new CVEs in real firmware Liu et al. (2025). These systems share our binary-level, source-free setting and our use of domain rules, but their goal is to emit vulnerability alerts via taint propagation. Ours is a different problem: we verify whether an analyst’s exploration path is logically entailed by a domain-knowledge graph under a temporal annotated logic, retaining the exploratory structure that alert-only pipelines discard while still steering it toward vulnerabilities. Where LATTE uses the LLM to produce the analysis, we use logic to check the LLM output. L.4 Constraining and Verifying LLM Reasoning with Structure Because LLM hallucinations are often confident and cannot be caught by probability-based checks, a growing body of work pairs LLMs with symbolic or structured components. Logic-LM translates a problem into symbolic form, solves it with a deterministic solver, and self-refines from solver errors Pan et al. (2023); knowledge-graph-guided methods such as Reasoning-on-Graphs Luo et al. (2024a) and Graph-Constrained Reasoning Luo et al. (2024b) constrain LLM reasoning to paths grounded in a KG to reduce hallucination on question-answering benchmarks. We share the premise that an independent structured layer must gate LLM output, but differ in kind rather than degree. These methods align reasoning to a walk within a single knowledge graph and are evaluated on natural- language QA. In our setting the object being verified is a trajectory through the binary’s call graph, while the constraints it must satisfy live in a separate domain-knowledge graph, so verification is an alignment between two graphs rather than a walk within one. The temporal, open-world semantics also admit constraints those methods do not model: analyst position is time-indexed, so a step is licensed only at the time point it is proposed, and negation over derived state lets the program assert what the domain knowledge fails to establish rather than only what it establishes (Section H). The target is likewise different—provable, explainable accept/reject inferences in a safety-critical binary domain, rather than answer faithfulness on general benchmarks. L.5 Vulnerabilities in Medical-Device Software The application domain motivates the entire effort. Connected medical devices —infusion pumps, insulin pumps, pacemakers—run long-lived embedded software that is hard to patch and frequently analysable only as deployed binaries. Large-scale analyses underscore the scale of the problem: a study of over 200,000 infusion pumps found that roughly three-quarters carried known security weaknesses, many tied to years-old, unpatched CVEs Das (2022), and reviews of FDA safety communications document repeated device vulnerabilities with direct patient-safety consequences Menon (2026). This is precisely the regime our system is built for: source-free analysis of the deployed artifact, with a logical guarantee that surviving analyst paths are consistent with encoded domain knowledge. L.6 Summary Unlike prior LLM-for-security work, which treats the model’s output as a prediction to be trusted or scored, we treat each LLM-proposed analyst trajectory as a hypothesis and pose its validation as a formal entailment-checking prob- lem against domain-knowledge. To our knowledge, this is the first framework to verify LLM-generated exploration paths—as opposed to final answers or natural-language reasoning—using temporal annotated logic. References Basque, Z. L.; Doria, S.; Soneji, A.; Gibbs, W.; Doup ́ e, A.; Shoshitaishvili, Y.; Losiouk, E.; Wang, R.; Aonzo, S.; et al. 2026. Decompiling the Synergy: An Empirical Study of Human-LLM Teaming in Software Reverse Engineering. In NDSS. Das, A. 2022. Know Your Infusion Pump Vulnerabilities and Secure Your Healthcare Organization. Technical report, Palo Alto Networks Unit 42. Analysis of over 200,000 infusion pumps; https://unit42.paloaltonetworks. com/infusion-pump-vulnerabilities/. 23 Hu, P.; Liang, R.; and Chen, K. 2024. DeGPT: Optimizing Decompiler Output with LLM. In NDSS. Lekssays, A.; Mouhcine, H.; Tran, K.; Yu, T.; and Khalil, I. 2025. LLMxCPG:Context-Aware vulnerability detection through code propertyGraph-Guided large language models. In 34th USENIX Security Symposium (USENIX Security 25), 489–507. Liu, P.; Sun, C.; Zheng, Y.; Feng, X.; Qin, C.; Wang, Y.; Xu, Z.; Li, Z.; Di, P.; Jiang, Y.; et al. 2025. Llm-powered static binary taint analysis. ACM Transactions on Software Engineering and Methodology, 34(3): 1–36. Luo, L.; Li, Y.-F.; Haffari, R.; and Pan, S. 2024a. Reasoning on graphs: Faithful and interpretable large language model reasoning. In International Conference on Learning Representations, volume 2024, 14400–14423. Luo, L.; Zhao, Z.; Haffari, G.; Li, Y.-F.; Gong, C.; and Pan, S. 2024b. Graph-constrained reasoning: Faithful reasoning on knowledge graphs with large language models. arXiv preprint arXiv:2410.13080. Menon, V. 2026. Cybersecurity Breaches in Medical Devices: Analyzing FDA Safety Communications in Response to Patient Security Concerns. Frontiers in Digital Health, 8: 1701551. Pan, L.; Albalak, A.; Wang, X.; and Wang, W. 2023. Logic-LM: Empowering Large Language Models with Sym- bolic Solvers for Faithful Logical Reasoning. In Bouamor, H.; Pino, J.; and Bali, K., eds., Findings of the As- sociation for Computational Linguistics: EMNLP 2023, 3806–3824. Singapore: Association for Computational Linguistics. Redini, N.; Machiry, A.; Wang, R.; Spensky, C.; Continella, A.; Shoshitaishvili, Y.; Kruegel, C.; and Vigna, G. 2020. Karonte: Detecting Insecure Multi-binary Interactions in Embedded Firmware. In 2020 IEEE Symposium on Security and Privacy (SP), 1544–1561. Sheng, Z.; Chen, Z.; Gu, S.; Huang, H.; Gu, G.; and Huang, J. 2025. LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights. ACM Comput. Surv., 58(5). Tan, H.; Luo, Q.; Li, J.; and Zhang, Y. 2024. Llm4decompile: Decompiling binary code with large language models. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, 3473–3487. Ullah, S.; Han, M.; Pujar, S.; Pearce, H.; Coskun, A.; and Stringhini, G. 2024. Llms cannot reliably identify and reason about security vulnerabilities (yet?): A comprehensive evaluation, framework, and benchmarks. In 2024 IEEE symposium on security and privacy (SP), 862–880. IEEE. Xie, D.; Zhang, Z.; Jiang, N.; Xu, X.; Tan, L.; and Zhang, X. 2024. Resym: Harnessing llms to recover variable and data structure symbols from stripped binaries. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 4554–4568. 24

Instant research discovery