arXiv:2607.12316v1 [cs.CR] 14 Jul 2026
Antiproof: Synthesizing Vulnerability Detectors and Proofs of Exploitability Alon Shakevsky
Corban Villa
Ion Stoica
Raluca Ada Popa
UC Berkeley [email protected]
UC Berkeley
UC Berkeley
UC Berkeley
Abstract—Discovering vulnerabilities before attackers exploit them requires high recall and reliable automatic validation, but existing approaches struggle to achieve both without prohibitive cost. We present Antiproof, an end-to-end vulnerability discovery system that combines neuro-symbolic detector synthesis for high-recall discovery with proof-of-exploitability oracles for automatic validation. Antiproof learns and iteratively refines static detectors from vulnerability datasets, then validates candidates by verifying whether executable proofs demonstrate concrete attacker capabilities. Evaluated on BountyBench and our curated KEVBench dataset, Antiproof detects 64 of 66 vulnerabilities, improving recall by more than 60 percentage points over static-analysis and neuro-symbolic baselines. In a scan of 50 widely deployed systems, Antiproof uncovered several hundred previously unknown vulnerabilities. We are responsibly disclosing all confirmed zero-days and have received 12 CVE assignments to date, including remote code execution vulnerabilities in Ray, SGLang, vLLM, and LiteLLM that could allow attackers to take over LLM training and inference systems.
1. Introduction Exploitable vulnerabilities are the most common initialaccess vector in organizational data breaches [1], [2] and the leading root cause of ransomware incidents [3]. Because the general problem of discovering such flaws is undecidable [4], practical systems must approximate and trade off recall, precision, and cost. Addressing this tradeoff has become urgent as exploitation timelines have shrunk from years to hours [5], [6], leaving defenders less time to discover and remediate vulnerabilities. An ideal solution for discovering exploitable flaws before attackers exploit them should provide high recall, reliable automatic validation (high precision), and low cost. Automated vulnerability discovery has been extensively studied, but no existing method achieves these properties simultaneously across a broad range of vulnerability classes [7], [8]. Static analysis tools can scan large systems [9], [10], but require experts to specify vulnerability patterns and manually review findings. These tools often prioritize precision over recall to reduce false positives and review overhead [10]. Dynamic approaches, such as fuzzing and symbolic execution, are effective in finding
Iterative Refinement
Synthesize
Detect
Validate
Figure 1. Antiproof synthesizes and iteratively refines high-recall static detectors from vulnerability datasets, scans target repositories for vulnerability candidates, and validates them with executable proofs of exploitability.
memory-safety vulnerabilities, but do not easily generalize to vulnerability classes that lack reliable bug oracles. These approaches often become prohibitively expensive for scanning large systems due to path explosion and deep program states [11], [12], [13], [14]. Large language models (LLMs) have shown strong codereasoning capabilities that can help address this challenge by automating parts of vulnerability discovery, exploitation, and patching [7], [33], [34], [35]. Proprietary LLM agents, such as Claude Mythos [23], [36] and Codex Security [24], [37], demonstrate that LLM-based systems can uncover thousands of vulnerabilities in production software. Despite this promise, LLM-based vulnerability discovery remains difficult to scale because LLM performance relies on careful context management [38], and a single project scan can require hundreds of millions of tokens and multiple days [39]. Continuous scanning is therefore impractical on large systems such as the Linux kernel. Moreover, high false-positive rates from LLM hallucinations and reward hacking create a validation bottleneck that requires expensive expert review to determine whether a finding is an exploitable vulnerability or a false positive [39], [40], [41]. For example, Anthropic reports running Claude Mythos roughly a thousand times on OpenBSD at a total cost of USD 20,000 and hiring security experts to manually validate its reports before disclosure [23]. Recent work combines LLMs with static analysis [19], [20], symbolic execution [29], and proof-ofconcept generation [30], [31], [32], but remains limited to specific vulnerability classes or still requires manual expert review to validate exploitability. As shown in Table 1, these limitations motivate an end-to-end system that achieves high recall, automatic executable validation, and low cost.
This work has been submitted to the IEEE for possible publication. Copyright may be transferred without notice, after which this version may no longer be accessible.
TABLE 1. Q UALITATIVE COMPARISON OF VULNERABILITY DISCOVERY AND VALIDATION SYSTEMS . Approach
Representative systems
Discovery Learned patterns
Static analysis Neuro-symbolic detectors LLM-guided auditing LLM security agents Fuzzing** Symbolic execution** PoC generation Antiproof
Class coverage
Validation Low cost
Executable Exploitability evidence oracle
Low cost
CodeQL [15], Semgrep [16] IRIS [17], QLCoder [18], KNighter [19], MoCQ [20] RepoAudit [21], Co-RedTeam [22] Claude Mythos* [23], Codex Security* [24] AFL++ [25], OSS-Fuzz [26], Syzkaller [27] Mayhem [11], Arbiter [28], SAILOR [29] AnyPoC [30], FaultLine [31], CVE-GENIE [32] This work
, , and denote full, partial, and no support, respectively. * We do not evaluate proprietary systems because we do not have access to their source code, and we use public reports for comparison. ** Fuzzing and symbolic execution are limited to specific vulnerability classes, primarily memory safety.
3)
In this work, we propose Antiproof, an end-to-end system that provides all three properties for a wide range of vulnerabilities. Our key insight, as shown in Figure 1, is to combine high-recall discovery with proofs of exploitability. To achieve this, we contribute two techniques: (1) Antiproof uses LLMs to synthesize reusable detectors and iteratively refine them for high-recall detection on a dataset of known vulnerabilities. To find vulnerabilities that data-flow analysis tools miss, including semantic vulnerabilities, we introduce eCPG traversals. An eCPG is a graph representation of code that extends the code property graph [42] with detectorspecific virtual nodes and edges to support modeling new vulnerability classes. (2) Antiproof uses LLMs to create validation environments to validate the detected vulnerability candidates and generate proofs that demonstrate a concrete attacker capability, such as code execution, file access, SSRF, or authentication bypass. Antiproof implements proof-of-exploitability oracles that verify the proofs in a challenge-response protocol that rejects LLM hallucinations. This reduces vulnerability validation to proof search under a deterministic oracle. Building a practical system from this insight raises three challenges: 1)
2)
Exploitability validation. LLMs can generate plausible but incorrect vulnerability reports and create a validation bottleneck that requires experts to manually review the reports. Automatic validation requires oracles that execute against the target system and check whether the vulnerability candidate enables an attacker-controlled security violation. These oracles must reject proofs that do not demonstrate practical risk to scale vulnerability validation.
Antiproof addresses these challenges and manages the inherent tradeoff between recall, precision, and cost. The system refines vulnerability detectors for high recall rather than precision against a vulnerability dataset. Antiproof uses proofs of exploitability to shift the manual review bottleneck from every vulnerability candidate to a small set of validation environments and oracles. To run the synthesized detectors at scale, we implement Antigraph, a native engine that constructs the eCPG and evaluates detector traversals an order of magnitude faster than existing CPG tools (see Section 5.5), which allows Antiproof to continuously scan large systems without expensive LLM inference. This design aims to improve recall as the vulnerability dataset covers more patterns and as LLMs become more capable. We evaluate Antiproof on known-vulnerability benchmarks and real-world zero-day discovery. We curate KEVBench, a dataset of CISA Known Exploited Vulnerabilities [43] in 2025 and 2026. Antiproof detects 44 of 46 BountyBench [44] vulnerabilities and 20 of 20 KEVBench vulnerabilities, outperforming evaluated baselines by over 60 percentage points in recall. Across 50 widely deployed systems, Antiproof generated 510 proofs of exploitability. Due to time constraints, we selected 100 findings for manual review and coordinated disclosure. We have received 12 CVE assignments to date and discovered three vulnerabilities before their CVEs were publicly disclosed. Antiproof uncovered critical and high-severity flaws, including remote code execution vulnerabilities in Ray, SGLang, vLLM, and LiteLLM that allow attackers to take over LLM training and inference systems, steal GPU resources [45], and poison production LLM models.
Detectors that generalize. Synthesized detectors must capture the underlying vulnerability pattern rather than overfit to a specific vulnerability or project. Overly specific detectors may miss variants of the vulnerability class (low recall), while overly broad detectors produce too many candidates for validation (high validation cost). The system must generalize across project sizes, programming languages, frameworks, and vulnerability classes, including logic and semantic flaws that conventional static analysis struggles to express. Project-scale discovery. Large systems with millions of lines of code, such as the Linux kernel, do not fit in a single LLM context window. The system must have high code coverage and construct only the minimal context that an LLM agent requires to validate each vulnerability candidate while avoiding prohibitive LLM inference cost.
2
eCPG path Vulnerable code 1 2 3 4 5 6 7 8 9 10 11 12
// attacker-controlled (state.c): setenv("USER", value, 1);
eCPG virtual edge eCPG traversal net_read
start_login
getenv
setenv
sink
Candidate context main
// expand_line (utility.c): p = getenv("USER"); obstack_grow(&obs, p, strlen(p)); ... cmd = obstack_finish(&obs); // start_login (pty.c): argcv_get(cmd, "", &argc, &argv); execv(argv[0], argv);
candidate
execv
### Enclosing function // telnetd/pty.c:112-138 void start_login(...) { ... argcv_get(cmd, "", &argc, &argv); execv(argv[0], argv); } ### Static analysis observations - sink: command_injection at pty.c:135 - env writer: setenv at state.c:1495, 1514 - env reader: getenv("USER") at utility.c:1740 - attack surface: main reaches start_login via telnetd_setup
Figure 2. Motivating example (simplified): CVE-2026-24061 in GNU InetUtils telnetd allowed unauthenticated attackers to gain root access to over 212,000 internet-exposed devices. The root cause is that a remote attacker can set the USER environment variable, which telnetd injects unsanitized as an argument to the login program. Left: the path from the attacker-controlled setenv to the execv sink, which traditional data-flow analysis (CodeQL, Joern) misses without a propagation model for the custom allocator (obstack). Middle: eCPG detects the path from attacker-controlled input (net_read) to a dangerous sink (execv) and adds an observation about the setenv write and getenv read via a virtual edge. Right: the context Antiproof prepares for the vulnerability candidate.
2. Background
infer deployment configurations and trust boundaries from official documentation. We assume that the attacker controls inputs that a realistic deployment receives across a trust boundary, such as network requests, RPC messages, and serialized objects. We focus on systems where a validation environment can demonstrate exploitability using Docker containers, QEMU [50], or virtual machines. We define an exploitable vulnerability as a software flaw that enables an attacker to gain a new capability on a deployed system or on a user’s system, such as code execution, file read, file write, authentication bypass, or denial of service. We do not consider flaws that do not enable new capabilities or are not reachable by the attacker as exploitable. We define a vulnerability as known, or one-day, if it is publicly tracked with a CVE or explicitly acknowledged in an official advisory or project documentation. We define a vulnerability as previously unknown, or zero-day, if it affects the latest release at the time of discovery and was not publicly documented when Antiproof found it.
2.1. Motivating Example Consider CVE-2026-24061, an authentication bypass vulnerability in GNU InetUtils telnetd [46] from CISA’s Known Exploited Vulnerabilities catalog [43] that allowed attackers to gain unauthenticated root access to over 212,000 internet-exposed devices. The root cause is that telnetd passed unsanitized user-controlled input to the login program and an attacker could inject an argument that skips password verification, as shown in Figure 2. Leading static analysis tools such as CodeQL [15] and Joern [42] miss this vulnerability without a propagation model for the custom allocator (obstack_grow) that GNU InetUtils uses, which hides the flow between the source (getenv) and the sink (execv). Even with a complete model specified by an engineer or an LLM, taint analysis cannot verify whether the input is sufficiently sanitized. For example, CVE-2026-28372, disclosed four weeks later, exploits the insufficient sanitization in the patch to CVE-2026-24061. Since this vulnerability is not a memory-safety bug, approaches that rely on memory sanitizers [47], [48], [49], including fuzzing, are not effective in detecting it. This gap motivates our approach, which combines high-recall static detection with executable validation to discover and confirm such critical vulnerabilities.
2.3. Code Property Graphs A code property graph (CPG) is a graph representation of code that combines the abstract syntax tree, controlflow graph, and data-dependence graph into a single graph. CPGs have shown promise for modeling security vulnerabilities [42] with graph traversals [51]. Joern is an open-source tool that analyzes code through CPG queries and supports languages such as C/C++, Java, Python, JavaScript, PHP, and Go. In this work, we introduce extended CPG (eCPG) traversals to model vulnerabilities that are missed by dataflow analysis tools, such as CodeQL and Joern. Antiproof
2.2. Threat Model We define the attacker as an untrusted actor interacting with the target system across a deployment trust boundary. As the systems under evaluation do not have precise definitions of their threat model, we use LLM agents to
3
refine detectors
Synthesis
õ
_
Vulnerability dataset
Detection
Validation
Synthesis agent
_ Synthesized detectors
Ñ
Û
.
Target repository
Run static detectors
Candidates
_
á Prepare environments
Generate proofs
Validated finding
Figure 3. Antiproof system architecture. Synthesis learns high-recall heuristics from a vulnerability dataset and refines them from observed false positives and false negatives. Detection runs the detectors on a target repository to find vulnerability candidates. Validation prepares a reusable PoE environment and a candidate-specific PoV environment, generates proofs, and checks each proof with its environment’s oracle.
3. Design
uses LLMs to generate and refine eCPG queries that detect a wide range of vulnerability classes.
Antiproof is designed to find exploitable vulnerabilities in large-scale systems with high recall, automatic validation (minimal manual review), and low inference and compute cost compared to direct LLM scanning. It consists of three subsystems: Synthesis, Detection, and Validation, as shown in Figure 3. Synthesis generates and refines static detectors once per vulnerability class, Detection runs them on a target repository to find vulnerability candidates, and Validation generates and checks a proof of vulnerability and a proof of exploitability for each candidate. Candidate detection and validation tasks are embarrassingly parallel, and Antiproof runs them with concurrent workers. Antiproof scans generate the following three artifacts:
2.4. Proofs of Vulnerability and Exploitability We define a proof of vulnerability (PoV) as an executable test that uses a bug oracle, such as a test harness with assertions, to demonstrate a violation of a security property in isolation. The most widely deployed bug oracles are memory sanitizers [47], [48], [49], which detect memory-safety bugs by instrumenting a program such that a memory violation crashes the process. Bug oracles are effective for a limited set of vulnerability classes, but they do not generalize to vulnerability classes that lack a reliable bug oracle. They also require expert review to validate exploitability, since the test harness may require high privileges and the bug may not be an exploitable vulnerability (for example, systemlevel mitigations may prevent exploitation, and some bugs are challenging to exploit on their own, such as an out-ofbounds read of a single byte). We define a proof of exploitability (PoE) as an end-toend test that demonstrates an attacker capability against a deployed system, such as code execution, file read or write, authentication bypass, or denial of service. In this work, we create validation environments and exploitability oracles to verify such a capability without requiring a precise bug oracle. PoEs must demonstrate an attack in a realistic environment and may require a chain of multiple vulnerabilities.
• •
•
Static hits. Synthesized detectors detect vulnerability patterns from source code analysis. Proofs of vulnerability. For each static hit, Antiproof generates an executable proof and accepts it only if the PoV environment’s crash oracle observes the target’s violation of the reported security property. Proofs of exploitability. For each verified proof of vulnerability, Antiproof generates an executable proof that demonstrates an attacker capability and the proof-of-exploitability oracle verifies it.
3.1. Synthesis
2.5. Known Exploited Vulnerabilities (KEVs)
The Synthesis subsystem uses LLM agents to synthesize static detectors that identify vulnerability candidates in a target repository. Its design goal is to generate detectors that generalize across programming languages, frameworks, and vulnerability classes. To achieve this goal, Antiproof uses a vulnerability dataset that we curate from public vulnerability reports and fixes. The dataset includes vulnerable versions and ground-truth labels that specify vulnerable source code locations for recall measurement. Antiproof updates its detectors whenever a new vulnerability is added to the dataset.
The Known Exploited Vulnerabilities (KEV) catalog [43] is a curated database maintained by the U.S. Cybersecurity and Infrastructure Security Agency (CISA) containing flaws that are actively exploited in real-world attacks, including data breaches and ransomware incidents. In this work, we curate a benchmark of KEVs to demonstrate the effectiveness of our approach in finding vulnerabilities with real-world impact.
4
eCPG virtual edge
3.2. Detection
candidate
The Detection subsystem runs the synthesized detectors against the target repository. Detectors are heuristics for known vulnerability patterns that Antiproof optimizes for high recall and low noise. The synthesized detectors use eCPG traversals with detector-specific virtual edges and observations that over-approximate potential vulnerability candidates to achieve high recall. We demonstrate an example of effective detection via eCPG traversals of source-to-sink (taint-style) vulnerabilities. Source-to-sink is a vulnerability pattern where attackercontrolled input (source) can reach a dangerous function call (sink). Figure 2 shows our motivating example, a KEV in telnetd that static taint analysis tools fail to detect without a custom taint propagation model. Antiproof overcomes this challenge by using breadth-first search (BFS) reachability instead of taint analysis: for every sink, it computes the set of methods that reach it, RS , as well as the set of methods that can be reached from attackercontrolled entry points RE , and adds the sink as a candidate if it is attacker-reachable, that is, RS ∩ RE ̸= ∅. For the motivating example, net_read reaches a setenv that writes the USER environment variable, and a getenv that reads the same USER variable reaches the execv sink. The detector links this write and read with a virtual edge over the shared variable, and uses eCPG traversals to detect the vulnerable flow. Antiproof additionally detects dynamic dispatch and polymorphism patterns in dynamic languages such as Python and JavaScript by over-approximating with BFS over eCPG virtual edges. As shown in Figure 4, Antiproof uses eCPG traversals with virtual nodes and edges to detect semantic flaws that taint analysis cannot model. To achieve scalable continuous scanning, Antiproof uses several optimizations. First, since eCPG traversals use BFS rather than data-flow propagation, Antiproof avoids constructing the Program Dependence Graph (PDG), which is typically more expensive to construct than the Abstract Syntax Tree (AST) or Control Flow Graph (CFG). Second, it extensively uses caching, for example to store the call graph, attack surface, and reachability trees. Third, it compiles the detectors and precomputes shared state. Finally, it uses a native engine rather than Joern, both to model languages that Joern does not support (such as Erlang) and to reduce scan time by an order of magnitude (Section 5.5).
shared resource .git/config.worktree
write_pair
parse_value
branches: {‘\n’,‘\t’, ‘\\’,‘"’}
branches: {‘\n’,‘\t’, ‘\\’,‘"’, ‘\r’}
branch-set diff: {‘\r’} read (write (X )) ̸= X Figure 4. An example of a detector that uses eCPG traversals to find a semantic vulnerability, KEV CVE-2025-48384 in Git. The root cause is an asymmetry between a configuration reader and a writer. Antiproof adds a virtual node for the shared .git/config resource, links the writer (write_pair) and reader (parse_value) through it, and detects the asymmetry in their escape-character handling.
To scan large systems effectively, Antiproof refines the following three detectors: 1)
2)
3)
The Scope detector decomposes a repository into subsystems. Antiproof uses it to improve performance by building eCPGs for each subsystem rather than building one for an entire system, as smaller eCPGs are faster to analyze. The Attack Surface detector locates entry points that cross a trust boundary, including HTTP, RPC, and framework callbacks. Antiproof uses it to reduce the search space and focus on code paths that attackers can reach. The Candidates detector searches for vulnerability candidates in paths that the attack surface reaches in each scoped eCPG. Each detector uses eCPG traversals to model a vulnerability class.
3.3. Validation
Rather than optimizing for precision, Antiproof optimizes for recall and reduces the resulting false positives with structural checks and iterative refinement. Each refinement round samples a detector’s hits, classifies false positives that do not fit the structural requirements of the vulnerability class, and fixes the detector until it achieves high recall (zero false negatives) with low noise (few false positives). Antiproof uses LLM agents and deterministic tests to verify that the detectors model a vulnerability class without overfitting to a specific CVE or project during synthesis.
The Validation subsystem determines whether a vulnerability candidate is exploitable in a realistic target configuration. Antiproof prepares a validation environment that is reused across candidates with the same target configuration and oracle. For each candidate, it also prepares an instrumented PoV environment with a crash oracle. Antiproof generates PoVs and PoEs and checks each proof with its environment’s oracle. These validation environments can also be used to automatically validate candidates produced by other vulnerability detection systems.
5
Algorithm 1 Antiproof end-to-end vulnerability discovery Validation Environment
Input: vulnerability dataset D , target repository R, oracle library O Output: validated bugs B, validated exploits X Synthesis (once, reused across repositories): 1: (S COPE, ATTACK S URFACE, C ANDIDATES) ← S YNTHESIZE(D) Discovery (per repository R): 2: (B, X ) ← (∅, ∅) 3: S ← S COPE(R) ▷ scoped subsystems 4: G ← B UILD CPG(R, S) ▷ scoped graph 5: A ← ATTACK S URFACE(G) ▷ trust-boundary entry points 6: C ← C ANDIDATES(G, A) Validation: 7: E ← P REPARE VALIDATION E NVS(R, O) 8: for all c ∈ C do 9: EPoV ← P REPARE P OVE NV(c) 10: E ← S ELECT VALIDATION E NV(E, c) 11: πv ← G ENERATE P OV(EPoV , c) 12: πe ← G ENERATE P O E(E, c) 13: if C HECK P ROOF(EPoV , πv ) = 1 then 14: B ← B ∪ {(c, πv )} 15: end if 16: if C HECK P ROOF(E, πe ) = 1 then 17: X ← X ∪ {(c, πe )} 18: end if 19: end for 20: return (B, X )
Prover
á Target
Oracle challenge
proof of exploitability
verify
¥ accept
q reject
Figure 5. An exploitability oracle as a challenge–response protocol. The oracle generates a challenge in the validation environment. The Prover, an LLM agent, connects over the network and executes a proof of exploitability against the target system. The oracle then verifies the state of the validation environment and accepts the proof if and only if the observed response correctly solves the challenge.
ity oracle, a small trusted program that checks a single attacker capability, for example, code execution, arbitrary file access, SSRF, authentication bypass, or service crash. The Prover, an LLM agent, generates and executes a proof against the validation environment. The oracle independently checks the resulting environment state and accepts the proof only if it demonstrates the required attacker capability. This validation is inspired by CTF (Capture The Flag) challenge validation [52], [53], such as kernelCTF [54], which verifies whether an attacker can achieve code execution on the Linux kernel. We extend the notion of CTF validation to capability-based challenges that prove attacker primitives beyond code execution and crashes. With a deterministic verifier, proof generation becomes a search problem, allowing LLMs or fuzzers to validate vulnerabilities beyond memory safety and capabilities beyond code execution. Proof-of-exploitability validation shifts the review bottleneck from each vulnerability candidate to a smaller set of trusted oracles (once per capability) and reusable validation environments (once per target configuration). A single exploitability oracle can automatically validate many vulnerabilities and save manual review effort. A vendor that trusts a validation environment can use it to automatically validate vulnerabilities in their system, similar to how Google automatically validates Linux kernel vulnerability reports using kernelCTF (but not limited to code execution). To ensure that proof-of-exploitability oracles accept a proof if and only if it demonstrates the attacker capability, we carefully review them using LLM agents and manual review. Antiproof implements exploitability oracles that use a cryptographically secure secret s and a mounted challenge directory /challenge, for example:
Triage. To manage the cost of LLM inference, Antiproof supports LLM-based triage of static analysis findings to deduplicate, rank, and classify findings. This allows Antiproof to prioritize realistic findings before investing in environment preparation or proof generation. The triage LLM agent can use the threat model of the system for classification, if available, to ignore findings outside of the threat model. The system can choose whether to remove findings, which may reduce recall, or to prioritize them within a budget. Validation Environment Preparation. Antiproof uses an LLM agent and reusable templates to prepare a reusable validation environment per target configuration to validate vulnerability candidates. A validation environment includes an execution environment, the deployed system, and a proofof-exploitability oracle. The execution environment may be a Docker container (e.g., for web applications), a virtual machine with GPUs (e.g., for LLM inference serving), or an emulator such as QEMU (e.g., for operating system kernels such as Linux). Antiproof verifies that the deployed system version, dependencies, feature flags, and deployment options match the vulnerability candidate using deterministic verifiers. For each candidate, Antiproof also prepares a PoV environment with a crash oracle and instruments the system to crash when it detects a violation of the relevant security property via a runtime monitor implemented using memory sanitizers (for memory-safety bugs) and instrumented assertions (for other vulnerability classes). The assertions allow the runtime monitor to detect semantic flaws by crashing the program when the security invariant is violated. Antiproof refines the environments with feedback from an LLM verifier that checks consistency and realism. Proof Generation. As shown in Figure 5, the validation environment runs the target system alongside an exploitabil-
•
6
Arbitrary Code Execution. The oracle generates s, ensures that /challenge/secret does not exist, creates a script /challenge/rce.sh such that executing the script would write the secret s into /challenge/secret (e.g., echo
•
•
•
•
•
"$secret" > /challenge/secret), then accepts a proof if and only if s is indeed written to /challenge/secret. Arbitrary File Read. The oracle generates s and stores it in /challenge/secret, then accepts a proof if and only if it returns s. Arbitrary File Write. The oracle generates s, ensures /challenge/secret does not exist, and provides it to the prover, then accepts a proof if and only if s is indeed written to /challenge/secret. Server-Side Request Forgery. The oracle generates s and provides it to the prover, runs a listener in the validation environment, and registers the listener’s host under a list of aliases on the environment network. It accepts a proof if and only if the listener receives s from the target rather than directly from the prover. Authentication Bypass. The oracle generates s and places a proxy in front of the protected endpoints that returns s when a request reaches a protected endpoint without authentication. The oracle accepts if and only if s appears in the proof’s output. Denial of Service. The oracle verifies a proof by checking whether the target has crashed (e.g., its process has died), become unavailable (e.g., its health check fails), or failed to terminate (and is killed after a timeout).
TABLE 2. A NTIPROOF ’ S COVERAGE OF THE 2025 CWE T OP 10 KEV W EAKNESSES [55]. Most actively exploited weakness OS command injection Use after free Out-of-bounds write Missing authentication Unsafe deserialization Path traversal Code injection Authentication bypass Heap-based buffer overflow Cross-site scripting
Antiproof ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ×
client-side code may be attacker-controlled. Because there are fewer exploitability oracles than vulnerability classes, manual review can focus on verifying the correctness of a small set of validation environments and automatically validate any vulnerability that is accepted by the exploitability oracles.
4. Implementation We implemented our approach to support interchangeable static detectors and LLM agents. The static detectors output SARIF (Static Analysis Results Interchange Format) and the LLM agents output structured JSON. Antiproof uses a PostgreSQL database and a web interface to store and deduplicate findings and track triage decisions, validation results, and disclosure status. Static Detectors. Antiproof synthesizes static detectors and refines them to be high-recall heuristics that approximate vulnerability candidates. It supports two eCPG query engines: (1) Joern, which executes queries as Scala scripts using a Java Virtual Machine (JVM) per invocation, and (2) Antigraph, our native Rust eCPG engine implementation. Antigraph partially implements the CPG specification [42], [56] but does not construct the expensive Program Dependence Graph (PDG). It implements language frontends using tree-sitter [57], including languages that Joern does not officially support, such as Erlang. Antiproof automatically detects subsystems, builds a CPG for each subsystem, and detects candidates using the selected eCPG engine. Detector coverage. Antiproof’s 32 synthesized detectors cover 45 vulnerability classes, including 9 of the 10 most actively exploited weakness classes, as shown in Table 2. The current implementation does not yet cover client-side classes such as cross-site scripting, which we leave to future work. Agents. Antiproof supports any LLM agent, including harnesses such as Claude Code and Codex. The system enforces structured outputs (JSON) using pydantic schemas and iterative refinement with verifier feedback. Agents are given a shell tool in a Docker container with language runtimes installed (e.g., Python 3.12, JDK 21,
Formally, let E be a validation environment, let C be an attacker capability (primitive), and let π be a candidate executable proof. We define the oracle OC as: ( 1 if π demonstrates C against E , OC (E, π) = 0 otherwise. A rejected proof, OC (E, π) = 0, does not imply the absence of C , only that the specific proof failed to demonstrate it. The exploitability oracles are independent of vulnerability classes by construction and depend only on the capability C and the validation environment E . The oracles are sound if the security games accurately model the system and every accepted proof demonstrates the capability. Oracle threat model. The exploitability oracle and validation environment are trusted and manually reviewed, while the prover is an untrusted attacker that connects to the target over the network. Each challenge uses a cryptographically secure secret and access-controlled challenge state. We manually review every validation environment to ensure that the prover cannot generate a proof that the oracle accepts without demonstrating the attacker capability, as guessing the secret has negligible success probability. Oracle coverage. A single exploitability oracle can validate many different vulnerabilities. For example, the Arbitrary Code Execution oracle can validate 9 of the 2025 Top 10 KEV vulnerability classes, as shown in Table 2, including unsafe deserialization, OS command injection, and code injection vulnerabilities. It does not currently support clientside vulnerabilities such as cross-site scripting (XSS), since
7
CodeQL [15]. CodeQL is a semantic code analysis engine that models vulnerabilities as queries over program structure and data flow. We use GitHub CodeQL CLI 2.25.5, create databases with autobuild, and run the language-specific security-extended query suite. • RepoAudit [21]. RepoAudit is an LLM-guided repository-auditing system for source-to-sink bug patterns. We run its dfbscan mode with reachability enabled, temperature 0, and call depth 3. RepoAudit only supports three vulnerability classes (null-pointer dereference, memory leak, and useafter-free). • KNighter [19]. KNighter synthesizes static-analysis checkers from vulnerability-fixing commits. KNighter only supports Linux-kernel vulnerabilities and struggles with use-after-free vulnerabilities that require state-machine and concurrency reasoning. In our benchmarks, this leaves only one supported target, the Linux use-after-free KEV. We provide KNighter with similar vulnerability patches and measure whether the generated detector can find the Linux KEV. We also include direct LLM scanning reference points using Codex with gpt-5.3-codex, gpt-5.4-mini, and gpt-5.5, and Claude Code with claude-opus-4.6. We include claude-opus-4.6 because Anthropic uses it in their published large-scale zero-day discovery evaluation in open-source software [59], [60]. These agents are not primary baselines because their performance depends strongly on model choice, prompt engineering, and inference budget. We run each agent in a Docker container with its CLI, Python 3.12, git, ripgrep, jq, and uv. The target repository is mounted read-only at /code with a writable /workspace. The read-only mount prevents the agent from modifying the project’s code, and the workspace allows the agent to save proof-of-concept artifacts and temporary files. As shown in Appendix A, we use prompts that instruct the agent to find all vulnerabilities in a candidate file and to report each finding with a proof-of-concept reproduction, similar to the approach described by Anthropic for their zero-day scans [59]. We do not evaluate Claude Code Security or Codex Security because their terms of service do not allow scanning third-party repositories. We allow 30 minutes per target and run each configuration 10 times. Table 3 shows the mean detections rounded to the nearest vulnerability and total recall percentages computed from the unrounded means.
Erlang/OTP, Codex CLI 0.128.0, and Claude Code CLI 2.1.132 pre-installed), with /code mounted read-only and /workspace writable and reset between candidates. Validation Environments. Antiproof implements validation environments using Docker containers, QEMU (e.g., for operating system emulation), or virtual machines (e.g., GPUs for inference serving). Each exploitability oracle generates a challenge for one attacker capability and checks whether the LLM-generated proof solves it. Antiproof creates a container for generated proofs and connects it to the validation environment through a Docker network or SSH forwarding. For PoVs, Antiproof uses the crash oracle and creates a candidate-specific PoV environment with assertions that crash when the vulnerability is detected. Vulnerability Dataset. We implemented scripts that collect vulnerability reports from GitHub Security Advisories, bug bounty writeups, and fix commits. We collected over 400 CVE reports in the evaluated projects to analyze common vulnerability patterns. For recall measurement, we collect the reports of the benchmark vulnerabilities and generate ground-truth labels for static detection that score a hit based on line proximity or enclosing method.
•
5. Evaluation We evaluate Antiproof using the following research questions: • • • •
RQ1. What recall does Antiproof achieve on known exploitable vulnerabilities? (Section 5.3) RQ2. Can Antiproof discover previously unknown vulnerabilities? (Section 5.4) RQ3. How efficient is Antiproof at scanning large systems? (Section 5.5) RQ4. Which components contribute to recall and cost? (Section 5.6)
5.1. Experimental Setup All experiments run on a GCP n2-highmem-32 instance (32 vCPUs, 256 GB RAM) provisioned via SkyPilot [58]. Experiments that include end-to-end validation that requires GPUs, for example inference engines, additionally use GCP g2-standard-4 instances with one NVIDIA L4 GPU. Baselines. For RQ1, our primary comparisons are opensource static-analysis and neuro-symbolic tools. We run the baselines in Docker containers that mount the target at /code and write tool outputs to /workspace. We score each baseline by the number of findings that are semantically equivalent to the benchmark ground-truth vulnerability reports. We compare recall against the following baselines: •
5.2. Metrics
Semgrep [16]. Semgrep is an open-source static analysis tool that scans code for security vulnerabilities using predefined rules. We use the open-source semgrep/semgrep Docker image and run semgrep scan with --config=auto, --no-git-ignore, and JSON output.
We use the following metrics in our evaluation: Recall. For known vulnerabilities, we measure recall as the fraction of benchmark vulnerabilities for which the system detects the ground-truth vulnerability. Hits, PoVs, and PoEs. For zero-day discovery, we track the funnel of Hits (static-detector candidates), PoVs
8
TABLE 3. R ECALL ON B OUNTY B ENCH AND KEVB ENCH . BountyBench KEVBench Total (n = 46) (n = 20) (n = 66)
Method
Model
Semgrep CodeQL RepoAudit KNighter
– – gpt-5.5 gpt-5.5
12 6 0 0
5 0 0 0
17 (26%) 6 (9%) 0 (0%) 0 (0%)
Claude Code claude-opus-4.6 Codex gpt-5.3-codex Codex gpt-5.4-mini Codex gpt-5.5
31 27 27 27
8 12 11 10
39 (59%) 39 (58%) 38 (58%) 37 (56%)
Antiproof Antiproof Antiproof Antiproof Antiproof
42 41 42 42 44
19 19 17 20 20
61 (92%) 60 (91%) 59 (89%) 62 (94%) 64 (97%)
claude-opus-4.6 Qwen 3.7-Max GLM-5.1 gpt-5.3-codex gpt-5.5
17,574
1,212
510
Hits
PoVs
PoEs
Figure 6. End-to-end zero-day discovery funnel across 50 scanned projects.
2025 and 2026 KEVs that affect open-source projects. The resulting benchmark contains 20 exploited-in-the-wild vulnerabilities across 12 vulnerability classes, 7 programming languages, and 17 projects. Results. As shown in Table 3, Antiproof detects 64 of 66 vulnerabilities with gpt-5.5, outperforming the strongest primary baseline, Semgrep, by 71 percentage points and the strongest direct LLM-agent reference point by 38 percentage points. It detects 62, 61, 60, or 59 of 66 using gpt-5.3-codex, claude-opus-4.6, Qwen 3.7-Max, or GLM-5.1, respectively. Because direct LLM scanning depends on the model, prompt, tool setup, and inference budget, we do not claim that LLM agents cannot find these vulnerabilities. Antiproof is complementary to direct LLM scanning because its static detectors can guide LLM agents during search, and its exploitability oracles can validate findings produced by those agents.
(proofs of vulnerability that the crash oracle accepts in a candidate-specific PoV environment), and PoEs (proofs of exploitability accepted by the exploitability oracle). Cost. We measure the time and cost in USD of candidate discovery (CPG construction and static detector execution) and automatic validation (environment preparation, environment execution, and LLM inference).
5.3. RQ1: Known-Vulnerability Detection We evaluate Antiproof on known-vulnerability benchmarks to measure recall. First, we evaluate on BountyBench, a public benchmark of real-world bug-bounty vulnerabilities. To reduce data-contamination risk and focus on exploitable vulnerabilities with real-world impact, we additionally curate KEVBench, a dataset of CISA Known Exploited Vulnerabilities [43] that became public in 2025 and 2026, after the knowledge cutoff of some of the LLMs we use in our evaluation. Benchmark scope. We measure recall on vulnerability detection, where the system generates vulnerability reports given a project. We do not evaluate on CyberGym [61] because its primary task is proof-of-concept reproduction from a vulnerability description, and its benchmark is centered on memory-safety bugs in fuzzing-style targets, while we focus on broad vulnerability-class coverage beyond memory safety. BountyBench. BountyBench [44] contains real-world vulnerabilities from 25 open-source projects, curated from public bug bounty programs with disclosed awards totaling over USD 60,000. To the best of our knowledge, the highest previously reported detection rate on BountyBench is CoRedTeam’s 20% result with Gemini-3-pro [22]. We use BountyBench as a known-vulnerability target set by collecting its CVEs, checking out the affected project versions, and scoring whether each system reports a finding semantically equivalent to the ground-truth vulnerability. Antiproof detects 44 of 46 BountyBench vulnerabilities (96%). KEVBench. We curate KEVBench from CISA’s Known Exploited Vulnerabilities [43] (KEVs) catalog by selecting
5.4. RQ2: Zero-Day Discovery We evaluate Antiproof on 50 widely deployed opensource projects. We select projects with high security impact on AI and cloud infrastructure, including LLM training and inference systems, that can be emulated in Docker containers, QEMU, or virtual machines. The selected projects total 136 million lines of code across 8 languages, with an average of 2.7 million lines per project and a maximum of 31.5 million lines. Results. In our initial zero-day scan, Antiproof found 17,574 vulnerability candidates, generated 1,212 PoVs, and accepted 510 PoEs (Figure 6). Due to time constraints, we selected 100 findings for manual review and coordinated disclosure. Antiproof has uncovered critical and highseverity vulnerabilities, including remote code execution in LLM training and inference systems, and denial-of-service and potential code-execution flaws in critical infrastructure such as OpenSSL and FreeBSD. We have received 12 CVE assignments to date and confirmed three vulnerabilities before their CVEs were publicly disclosed. We continue to improve the static detectors in recall and precision and to scale the validation environments. Table 4 reports the perproject language, size, funnel, and cost. Cost reference. Anthropic reports that the OpenBSD campaign that found the SACK vulnerability ran Mythos roughly a thousand times at a total cost of USD 20,000 [23]. Antiproof validated its static findings in OpenBSD with
9
TABLE 4. A NTIPROOF ’ S ZERO - DAY SCAN ACROSS 50 WIDELY DEPLOYED PROJECTS . LOC
Hits
PoV PoE Cost (USD)
openbsd freebsd fluent bit mariadb postgres mlflow transformers openssl sglang linux qemu git airflow vllm litellm httpd moby openssh redis bentoml huggingface hub ollama argo cd llama cpp tomcat containerd jenkins nccl onnxruntime nginx kserve jupyterhub langfuse gvisor buildkit harbor runc pytorch gitlab triton inference server ingress nginx nvidia container toolkit prometheus ray grafana safetensors envoy firecracker kubernetes tensorflow
C 16.1M C 19.5M C 806k C++ 1.9M C 1.8M Python 1.6M Python 1.3M C 993k Python 1.1M C 31.5M C 2.4M C 1.1M Python 1.4M Python 1.0M Python 1.5M C 447k Go 2.3M C 149k C 386k Python 92k Python 91k Go 749k Go 2.3M C++ 655k Java 440k Go 1.2M Java 289k C++ 132k C++ 3.9M C 213k Go 5.4M Python 66k TypeScript 533k Go 578k Go 1.2M Go 341k Go 324k Python 3.2M Ruby 8.2M Python 134k Go 147k Go 890k Go 447k Python 1.4M Go 3.5M Rust 9k C++ 1.5M Rust 145k Go 5.4M C++ 5.1M
4,118 3,828 1,208 1,069 782 554 514 513 472 466 460 440 405 251 230 208 193 164 164 146 140 138 124 123 98 83 81 72 70 62 50 48 47 39 37 35 33 31 29 24 6 6 5 4 2 2 0 0 0 0
190 180 87 100 25 51 26 12 62 33 36 10 33 56 21 15 4 11 4 38 29 3 10 34 34 14 2 23 4 2 22 4 1 9 10 2 0 6 5 2 0 0 0 2 0 0 0 0 0 0
65 3 1 63 6 30 6 1 35 6 0 3 22 49 8 0 3 9 2 28 14 2 10 25 32 13 1 8 4 2 22 4 1 9 8 0 0 6 5 2 0 0 0 2 0 0 0 0 0 0
611.90 460.33 315.06 140.98 69.34 74.06 18.42 84.80 75.37 76.33 148.01 61.82 34.05 61.90 38.94 99.45 12.78 56.26 16.19 22.02 23.57 18.28 14.02 32.46 31.79 13.82 10.73 83.32 6.33 39.14 10.01 7.34 2.80 7.65 5.88 2.72 5.57 20.23 7.03 4.03 0.92 0.88 0.56 0.72 0.20 0.00 0.00 0.00 0.00 0.00
136M 17,574 1,212
510
2,828
Total (50 projects)
Batch wall time (s)
Language
59 min
103
2.3 min 102
Joern
Antigraph
(b) Scaling Per-target wall time (s)
Project
(a) Throughput 104
103
Joern Antigraph
Linux
102 101 102
101
103
104
Source files
(c) Time breakdown
Antigraph
Joern
0
20
40
60
totalload time CPG build % of CPG candidates other
80
100
call graph
Figure 7. Detector efficiency and scalability on KEVBench and BountyBench.
a cold cache, rebuilding all graphs in every iteration, and reach identical recall (64 of 66). Throughput. As Figure 7(a) shows, Antigraph scans all benchmark targets 25× faster than Joern, a median of 2.3 versus 59 minutes across 5 trials. Scaling. As shown in Figure 7(b), Antigraph’s median per-target time is 27.3 s, 92× faster than Joern’s 2,505 s, with a maximum of 140 s on the largest target, the Linux kernel at 51k scoped files. Time breakdown. As shown in Figure 7(c), Joern spends 92% of its run time building and loading CPGs. By contrast, Antigraph is 25× faster, as it avoids building the expensive program-dependence graph via BFS reachability in Rust over the eCPG rather than Joern’s data-flow propagation in Scala.
gpt-5.3-codex for less than USD 612, a 33× lower cost, and reproduces the Mythos findings, SACK nulldereference in OpenBSD and FreeBSD CVE-2026-4747, for USD 0.46 and USD 1.73, respectively. These costs reflect a single run of an early prototype and represent an upper bound, as we have continued to optimize the system since the scan.
5.5. RQ3: Detector Efficiency and Scalability
5.6. RQ4: Component Contributions
Continuous scanning of large systems requires fast detection that scales with project size. We compare Antigraph, Antiproof’s native eCPG engine, against Joern on the full 66-target KEV and BountyBench set. Both engines run with
We run the following ablations to measure how Antiproof’s components contribute to recall and cost:
10
scope and attack surface to avoid path explosion, which may lead to false negatives if a real vulnerability is outside of the detected paths. Antiproof mitigates this by testing its detectors on a wide range of projects across different programming languages and frameworks. Static Analysis Tools. Antiproof depends on the quality of its static detectors and eCPG engines. It supports two engines, Joern and Antigraph, which must correctly parse the source languages, build the eCPG, and execute its traversals. Any error in these steps can cause Antiproof to miss vulnerabilities. End-to-end validation. Automatic vulnerability validation requires environments that accurately simulate the target system. PoV environments are candidate-specific, whereas a validation environment can be reviewed once and reused across candidates. Our evaluation focuses on open-source projects because Antiproof assumes source-code access for analysis and validation. We leave scanning proprietary systems to future work. In some cases, accurate simulation may be challenging, for example, when hardware emulation or third-party authentication is required, which may lead to false positives or false negatives. Our proof-of-exploitability oracles cover the attacker primitives evaluated in this paper, including remote code execution, arbitrary file access, SSRF, authentication bypass, and denial of service. Vulnerabilities whose impact does not map cleanly to these primitives may require experts to create and manually review new exploitability oracles. Threat Model. Antiproof may generate reports for exploitable vulnerabilities that are outside the threat model of the target system. To mitigate that, we use LLMs to generate and update a threat model document. Antiproof uses the threat model document to classify and prioritize findings. Future work may improve the accuracy of these LLMgenerated threat models, allowing Antiproof to focus on inscope findings and reduce cost and false positives. In some cases, project maintainers may dispute real vulnerabilities and consider them out of scope or without security impact, while real-world attackers exploit them in the wild [45]. LLM limitations. Antiproof uses LLMs to synthesize detectors, generate proof-of-vulnerability (PoV) tests, set up validation environments, and generate proofs of exploitability (PoE). Generating a PoE may be challenging or require a chain of multiple vulnerabilities. The model may also refuse cybersecurity tasks such as exploitation due to safety filters. To reduce these false negatives, Antiproof supports any LLM agent, including open-weight models, and can run multiple agents with different providers. To reduce false positives, we manually review the exploitability oracles and validation environments. Threats to validity. As our known-vulnerability benchmarks, BountyBench and KEVBench, are publicly available, LLM agents may memorize the vulnerabilities or exploits from their training data or discover them via web search. To mitigate this risk of data contamination, KEVBench uses known exploited vulnerabilities that became public in 2025 and 2026, after the knowledge cutoff of some of the LLMs we evaluate. To reduce the risk of memorization,
TABLE 5. C OMPONENT ABLATION STUDY. BountyBench KEVBench Total (n = 46) (n = 20) (n = 66) Candidates
Variant Detector ablations Antiproof −eCPG −eCPG frontends −Attack Surface −Scope Validation ablations −observations (gpt-5.3-codex, medium) −observations (gpt-5.5, medium)
•
•
• • •
Time
44 30 44 44 44
20 16 18 20 20
64 46 62 64 64
32,705 140s 2,028 3,490s 32,682 264s 47,280 294s 160,005 456s
36
15
51
–
–
41
19
60
–
–
−eCPG replaces Antiproof’s reachability traversal with Joern’s native data-flow reachability, reachableByFlows. −eCPG frontends disables the custom eCPG frontends that Antiproof implements for languages Joern cannot ingest natively, namely Erlang and Velocity. −Attack Surface disables the detector that selects attacker-facing entry points. −Scope disables repository-scope detection and builds whole-repository CPGs. −observations removes technique facts and structural observations from the prover prompt.
Static detector runs use a 20-minute per-target timeout. Results. The Detection ablations in Table 5 show that each component improves recall or efficiency. Antiproof with eCPG detects 18 more benchmark vulnerabilities than Joern’s native data-flow reachability and runs 25× faster. The custom eCPG frontends for Erlang and Velocity recover two KEVBench vulnerabilities that Joern’s native frontends cannot parse. Scope detection reduces the candidate count by 80% and scan time by 3.3× by focusing CPG construction on relevant code, while maintaining recall. Attack Surface detection reduces the candidate count by 31% and scan time by 2.1× while maintaining recall. The Validation ablations show that the static observations improve recall. Removing observations with gpt-5.3-codex at medium effort detects 36 of 46 BountyBench targets and 15 of 20 KEVBench targets, for 51 of 66 total. With gpt-5.5 at medium effort, the system detects 41 of 46 BountyBench targets and 19 of 20 KEVBench targets, for 60 of 66 total.
6. Discussion and Limitations Vulnerability Detectors. Antiproof can only find vulnerabilities that the synthesized detectors detect. Because the system synthesizes detectors from known vulnerability patterns, it may miss a novel pattern until it learns a corresponding detector. To mitigate such false negatives, Antiproof can synthesize new detectors from additional known vulnerabilities or generate candidates with external systems, such as LLM agents or other static analysis tools. Moreover, Antiproof uses synthesized detectors that detect
11
Vulnerability Validation. Proof-of-Vulnerability (PoV) test generation has been extensively studied [33]. Recent works, including AnyPoC [30], FaultLine [31], and CVEGENIE [32], leverage LLMs for proof-of-vulnerability test generation. Because these approaches automatically validate the PoV using LLM-as-a-judge verifiers or bug oracles such as memory sanitizers [47], [48], [49], they either are limited in vulnerability-class coverage or inherit LLM limitations such as hallucinations, reward hacking, and weaker performance on long-context reasoning [39], [40]. Recent exploitability benchmarks such as ExploitBench [82] and ExploitGym [83] evaluate the ability of LLMs to exploit vulnerabilities, but focus on code execution from memorysafety vulnerabilities. Rather than relying on manual review or LLMs, Antiproof extends the notion of CTF-based validation [54] to prove attacker capabilities without a precise bug oracle. This shifts the manual review bottleneck from every vulnerability candidate to a small set of validation environments and oracles and allows Antiproof to automatically validate vulnerability classes beyond memory safety.
we additionally evaluate Antiproof’s effectiveness in zeroday discovery. Exact reproduction of our experiments that use proprietary LLM models may be challenging, as their performance can depend on the model capabilities and safety filters. To reduce this risk, Antiproof supports open-weight models, such as GLM-5.1.
7. Related Work Program Analysis. Program analysis approaches for vulnerability discovery, such as static analysis [9], [10], fuzzing [13], [14], taint analysis [62], and symbolic execution [11], [12], have been extensively studied. Querybased approaches, such as CodeQL [15] and code property graphs [42], are effective for specific vulnerability patterns, but rely on expert-written models, source and sink specifications, and manual validation of alerts. Fuzzing and symbolic execution are effective for vulnerability discovery and automatic exploit generation [63], but are primarily limited to memory safety and struggle with harness engineering, exponential search spaces, and deep program states. Arbiter [28] and SAILOR [29] combine static analysis with symbolic execution to discover specific memory safety vulnerabilities. In contrast, Antiproof detects vulnerabilities beyond memorysafety and combines neuro-symbolic static analysis for highrecall detection with proofs of exploitability for automatic validation. LLM-Based Static Analysis. Prior work uses LLMs to guide vulnerability classification with code property graphs (LLMxCPG [64]) and to infer specifications for taintbased vulnerabilities in Java (IRIS [17], Argus [65]), PHP (Artemis [66]), and JavaScript (SemTaint [67]). Recent work explores neuro-symbolic static analysis, where LLMs synthesize static detectors from historical vulnerability patterns, including C/C++ static analyzers (KNighter [19]), CodeQL queries (QLCoder [18]), and Joern queries (MoCQ [20]). ProtocolGuard [68] combines LLM-guided static analysis with dynamic verification to detect protocol non-compliance bugs. In comparison, Antiproof introduces eCPG traversals to detect vulnerabilities that prior approaches fail to model, including semantic vulnerabilities, synthesizes static detectors and refines them for high recall on a wide range of vulnerability classes, and uses proof-of-exploitability oracles for automatic validation rather than expert review or LLM verifiers. Agentic Vulnerability Discovery. LLM agents have shown promise for vulnerability discovery, exploitation, and patching [7], [8], [21], [22], [33], [34], [35], [61], [69], [70], [71], [72], [73], [74], [75], [76], [77], [78]. Proprietary systems including Claude Mythos [23], [36], Claude Code Security [59], [60], Codex Security [24], BigSleep [79], XintCode [80], and XBOW [81] have used LLMs to uncover thousands of vulnerabilities in production systems. In contrast to direct LLM scanning, which is prohibitively expensive for continuous scanning and suffers from high falsepositive rates [39], Antiproof uses efficient static detectors to continuously scan large systems and proofs of exploitability for automatic validation.
8. Conclusion Scalable vulnerability discovery is critical to secure computer systems before attackers exploit them. In this paper, we have presented Antiproof, an end-to-end vulnerability discovery system for continuously scanning large-scale projects for vulnerability patterns with high recall and low discovery and validation costs. Antiproof uses LLMs to continually synthesize and refine static detectors for high-recall discovery and executable proofs of exploitability for automatic validation. We show that this novel approach outperforms existing baselines on two known vulnerability benchmarks, BountyBench and our curated KEVBench dataset. Evaluated on 50 widely deployed open-source projects, Antiproof generated 510 proofs of exploitability. Due to time constraints, we selected 100 findings for manual review and coordinated disclosure. To date, we have received 12 CVE assignments for vulnerabilities of critical or high severity, including remote code execution vulnerabilities that could lead to complete takeover of widely deployed LLM inference and training systems.
Ethics Considerations We recognize the dual-use risk of vulnerability discovery. To mitigate this risk, we manually review selected findings and coordinate disclosure of confirmed vulnerabilities with affected maintainers and vendors. When possible, we suggest patches or mitigations and allow affected parties sufficient time to develop and deploy fixes before public disclosure. We evaluate only on publicly available opensource projects and vulnerability benchmarks, and reproduce vulnerabilities only in local environments without affecting production systems. We do not collect personally identifiable information or sensitive data in this research. Our goal is to help defenders find and fix existing flaws before attackers exploit them.
12
Acknowledgments
[18] C. Wang, Z. Li, S. Dutta, and M. Naik, “Qlcoder: A query synthesizer for static analysis of security vulnerabilities,” arXiv preprint arXiv:2511.08462, 2025.
We thank the students in the Sky Computing Lab security group for their feedback. This work is supported by gifts from Accenture, Algorithmic SuperIntelligence Labs, Amazon, AMD, Anyscale, Broadcom, cmpnd, Google, IBM, Intel, Intesa Sanpaolo, Lambda, Lightspeed, Mirendil, NVIDIA, Samsung SDS, and VESSL.
[19] C. Yang, Z. Zhao, Z. Xie, H. Li, and L. Zhang, “Knighter: Transforming static analysis with llm-synthesized checkers,” in Proceedings of the ACM SIGOPS 31st Symposium on Operating Systems Principles, 2025, pp. 655–669. [20] P. Li, S. Yao, J. Sarfati Korich, C. Luo, J. Yu, Y. Cao, and J. Yang, “Automated static vulnerability detection via a holistic neurosymbolic approach,” arXiv preprint arXiv:2504.16057, 2025.
References
[21] J. Guo, C. Wang, X. Xu, Z. Su, and X. Zhang, “Repoaudit: An autonomous llm-agent for repository-level code auditing,” arXiv preprint arXiv:2501.18160, 2025.
[1]
Mandiant, “M-Trends 2025 report,” https://services.google.com/fh/ files/misc/m-trends-2025-en.pdf, 2025, google Cloud Security.
[2]
Verizon, “2026 data breach investigations report (DBIR),” https: //www.verizon.com/business/resources/reports/dbir/, 2026.
[3]
Sophos, “The state of ransomware 2025,” https://assets. sophos.com/X24WTUEQ/at/9brgj5n44hqvgsp5f5bqcps/ sophos-state-of-ransomware-2025.pdf, 2025.
[4]
H. G. Rice, “Classes of recursively enumerable sets and their decision problems,” Transactions of the American Mathematical society, vol. 74, no. 2, pp. 358–366, 1953.
[5]
Zero Day Clock, “Zero day clock: Tracking time-to-exploit,” https: //zerodayclock.com/, 2026.
[6]
SonicWall, “2025 SonicWall cyber threat https://www.sonicwall.com/resources/white-papers/ 2025-sonicwall-cyber-threat-report, 2025.
[23] Anthropic, “Assessing Claude Mythos Preview’s cybersecurity capabilities,” https://red.anthropic.com/2026/mythos-preview/, 2026. [24] OpenAI, “Codex Security: now in research preview,” https://openai. com/index/codex-security-now-in-research-preview/, 2026. [25] A. Fioraldi, D. Maier, H. Eißfeldt, and M. Heuse, “{AFL++}: Combining incremental steps of fuzzing research,” in 14th USENIX workshop on offensive technologies (WOOT 20), 2020. [26] Google, “OSS-Fuzz: Continuous fuzzing for open source software,” https://github.com/google/oss-fuzz, 2025.
report,”
[7]
J. Zhang, H. Bu, H. Wen, Y. Liu, H. Fei, R. Xi, L. Li, Y. Yang, H. Zhu, and D. Meng, “When llms meet cybersecurity: A systematic literature review,” Cybersecurity, vol. 8, no. 1, p. 55, 2025.
[8]
C. Rohlf, “AI and the software vulnerability lifecycle,” https://cset. georgetown.edu/article/ai-and-the-software-vulnerability-lifecycle/, 2025, center for Security and Emerging Technology (CSET).
[9]
[22] P. He, A. Fox, L. Miculicich, S. Friedli, D. Fabian, B. Gokturk, J. Tang, C.-Y. Lee, T. Pfister, and L. T. Le, “Co-redteam: Orchestrated security discovery and exploitation with llm agents,” arXiv preprint arXiv:2602.02164, 2026.
[27] ——, “Syzkaller,” https://github.com/google/syzkaller, 2025. [28] J. Vadayath, M. Eckert, K. Zeng, N. Weideman, G. P. Menon, Y. Fratantonio, D. Balzarotti, A. Doupé, T. Bao, R. Wang et al., “Arbiter: Bridging the static and dynamic divide in vulnerability discovery on binary programs,” in 31st USENIX Security Symposium (USENIX Security 22), 2022, pp. 413–430. [29] M. Shafiuzzaman, A. Desai, W. Guo, and T. Bultan, “Guiding symbolic execution with static analysis and llms for vulnerability discovery,” arXiv preprint arXiv:2604.06506, 2026.
N. Ayewah, W. Pugh, D. Hovemeyer, J. D. Morgenthaler, and J. Penix, “Using static analysis to find bugs,” IEEE software, vol. 25, no. 5, pp. 22–29, 2008.
[30] Z. Zhao, C. Yang, W. Wang, Y. Yang, Z. Zhang, and L. Zhang, “Anypoc: Universal proof-of-concept test generation for scalable llmbased bug detection,” arXiv preprint arXiv:2604.11950, 2026.
[10] A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler, “A few billion lines of code later: using static analysis to find bugs in the real world,” Communications of the ACM, vol. 53, no. 2, pp. 66–75, 2010.
[31] V. Nitin, B. Ray, and R. Z. Moghaddam, “Faultline: Automated proof-of-vulnerability generation using llm agents,” arXiv preprint arXiv:2507.15241, 2025. [32] S. Ullah, P. Balasubramanian, W. Guo, A. Burnett, H. Pearce, C. Kruegel, G. Vigna, and G. Stringhini, “From cve entries to verifiable exploits: An automated multi-agent framework for reproducing cves,” arXiv preprint arXiv:2509.01835, 2025.
[11] S. K. Cha, T. Avgerinos, A. Rebert, and D. Brumley, “Unleashing mayhem on binary code,” in 2012 IEEE Symposium on Security and Privacy. IEEE, 2012, pp. 380–394. [12] R. Baldoni, E. Coppa, D. C. D’elia, C. Demetrescu, and I. Finocchi, “A survey of symbolic execution techniques,” ACM Computing Surveys (CSUR), vol. 51, no. 3, pp. 1–39, 2018.
[33] Z. Sheng, Z. Chen, S. Gu, H. Huang, G. Gu, and J. Huang, “Llms in software security: A survey of vulnerability detection techniques and insights,” ACM Computing Surveys, vol. 58, no. 5, pp. 1–35, 2025.
[13] J. Li, B. Zhao, and C. Zhang, “Fuzzing: a survey,” Cybersecurity, vol. 1, no. 1, p. 6, 2018.
[34] X. Zhou, S. Cao, X. Sun, and D. Lo, “Large language model for vulnerability detection and repair: Literature review and the road ahead,” ACM Transactions on Software Engineering and Methodology, vol. 34, no. 5, pp. 1–31, 2025.
[14] V. J. Manès, H. Han, C. Han, S. K. Cha, M. Egele, E. J. Schwartz, and M. Woo, “The art, science, and engineering of fuzzing: A survey,” IEEE Transactions on Software Engineering, vol. 47, no. 11, pp. 2312–2331, 2019.
[35] S. Heelan, “On the coming industrialisation of exploit generation with LLMs,” https://sean.heelan.io/2026/01/18/ on-the-coming-industrialisation-of-exploit-generation-with-llms/, 2026.
[15] P. Avgustinov, O. De Moor, M. P. Jones, and M. Schäfer, “Ql: Objectoriented queries on relational data,” in 30th European Conference on Object-Oriented Programming (ECOOP 2016). Schloss Dagstuhl– Leibniz-Zentrum für Informatik, 2016, pp. 2–1.
[36] Anthropic, “Project Glasswing: Securing critical software for the AI era,” https://www.anthropic.com/glasswing, 2026.
[16] Semgrep, “Semgrep Code overview,” https://semgrep.dev/docs/ semgrep-code/overview, 2026, accessed: 2026-05-03.
[37] OpenAI, “Introducing Aardvark: OpenAI’s agentic security researcher,” https://openai.com/index/introducing-aardvark/, 2025.
[17] Z. Li, S. Dutta, and M. Naik, “Iris: Llm-assisted static analysis for detecting security vulnerabilities,” in International Conference on Learning Representations, vol. 2025, 2025, pp. 35 735–35 758.
[38] L. Mei, J. Yao, Y. Ge, Y. Wang, B. Bi, Y. Cai, J. Liu, M. Li, Z.-Z. Li, D. Zhang et al., “A survey of context engineering for large language models,” arXiv preprint arXiv:2507.13334, 2025.
13
[59] Anthropic, “Evaluating and mitigating the growing risk of LLMdiscovered 0-days,” https://red.anthropic.com/2026/zero-days/, 2026.
[39] F. Li, J. Jiang, D. Chen, and Y. Xiong, “Llm-based vulnerability detection at project scale: An empirical study,” arXiv preprint arXiv:2601.19239, 2026.
[60] ——, “Partnering with mozilla to improve firefox’s security,” https: //www.anthropic.com/news/mozilla-firefox-security, 2026.
[40] A. T. Kalai, O. Nachum, S. S. Vempala, and E. Zhang, “Why language models hallucinate,” arXiv preprint arXiv:2509.04664, 2025.
[61] Z. Wang, T. Shi, J. He, M. Cai, J. Zhang, and D. Song, “Cybergym: Evaluating ai agents’ cybersecurity capabilities with real-world vulnerabilities at scale,” arXiv preprint arXiv:2506.02548, 2025.
[41] X. Du, J. Feng, Y. Zou, W. Xu, J. Ma, W. Zhang, S. Liu, X. Peng, and Y. Lou, “Reducing false positives in static bug detection with llms: An empirical study in industry,” arXiv preprint arXiv:2601.18844, 2026.
[62] J. Newsome, D. X. Song et al., “Dynamic taint analysis for automatic detection, analysis, and signaturegeneration of exploits on commodity software.” in NDSS, vol. 5, 2005, pp. 3–4.
[42] F. Yamaguchi, N. Golde, D. Arp, and K. Rieck, “Modeling and discovering vulnerabilities with code property graphs,” in 2014 IEEE symposium on security and privacy. IEEE, 2014, pp. 590–604.
[63] T. Avgerinos, S. K. Cha, B. L. T. Hao, and D. Brumley, “AEG: Automatic exploit generation,” in Network and Distributed System Security Symposium (NDSS), 2011.
[43] Cybersecurity and Infrastructure Security Agency, “Known exploited vulnerabilities catalog,” https://www.cisa.gov/ known-exploited-vulnerabilities-catalog, 2026.
[64] A. Lekssays, H. Mouhcine, K. Tran, T. Yu, and I. Khalil, “{LLMxCPG}:{Context-Aware} vulnerability detection through code property {Graph-Guided} large language models,” in 34th USENIX Security Symposium (USENIX Security 25), 2025, pp. 489– 507.
[44] A. Zhang, J. Ji, C. Menders, R. Dulepet, T. Qin, R. Wang, J. Wu, K. Liao, J. Li, J. Hu et al., “Bountybench: Dollar impact of ai agent attackers and defenders on real-world cybersecurity systems,” Advances in Neural Information Processing Systems, vol. 38, 2026.
[65] Z. Liang, Q. Xie, J. He, B. Xue, W. Wang, Y. Cai, F. Luo, B. Zhang, H. Hu, and K. Wu, “Argus: Reorchestrating static analysis via a multiagent ensemble for full-chain security vulnerability detection,” arXiv preprint arXiv:2604.06633, 2026.
[45] Oligo Security, “ShadowRay: AI workloads actively exploited in the wild,” https://www.oligo.security/blog/ shadowray-attack-ai-workloads-actively-exploited-in-the-wild, 2024.
[66] Y. Ji, T. Dai, Z. Zhou, Y. Tang, and J. He, “Artemis: Toward accurate detection of server-side request forgeries through llm-assisted interprocedural path-sensitive taint analysis,” Proceedings of the ACM on Programming Languages, vol. 9, no. OOPSLA1, pp. 1349–1377, 2025.
[46] S. Josefsson, “GNU InetUtils security advisory: remote authentication by-pass in telnetd,” https://seclists.org/oss-sec/2026/q1/89, 2026. [47] E. Stepanov and K. Serebryany, “Memorysanitizer: fast detector of uninitialized memory use in c++,” in 2015 IEEE/ACM International Symposium on Code Generation and Optimization (CGO). IEEE, 2015, pp. 46–55.
[67] J. Ghebremichael, S. Vasan, S. Ullah, G. Tystahl, D. Adei, C. Kruegel, G. Vigna, W. Enck, and A. Kapravelos, “Multi-agent taint specification extraction for vulnerability detection,” arXiv preprint arXiv:2601.10865, 2026.
[48] K. Serebryany, D. Bruening, A. Potapenko, and D. Vyukov, “{AddressSanitizer}: A fast address sanity checker,” in 2012 USENIX annual technical conference (USENIX ATC 12), 2012, pp. 309–318.
[68] X. Song, L. Pei, J. Wu, Y. Zeng, G. He, C. Zuo, X. Liu, Q. Zhao, and S. Guo, “Protocolguard: Detecting protocol non-compliance bugs via llm-guided static analysis and dynamic verification.” in NDSS, 2026.
[49] D. Song, J. Lettner, P. Rajasekaran, Y. Na, S. Volckaert, P. Larsen, and M. Franz, “Sok: Sanitizing for security,” in 2019 IEEE Symposium on Security and Privacy (SP). IEEE, 2019, pp. 1275–1295.
[69] Y. Li, X. Li, H. Wu, M. Xu, Y. Zhang, X. Cheng, F. Xu, and S. Zhong, “Everything you wanted to know about llm-based vulnerability detection but were afraid to ask,” arXiv preprint arXiv:2504.13474, 2025.
[50] F. Bellard et al., “Qemu, a fast and portable dynamic translator.” in Usenix ATC, Freenix Track, 2005, pp. 41–46.
[70] Y. Ding, Y. Fu, O. Ibrahim, C. Sitawarin, X. Chen, B. Alomair, D. Wagner, B. Ray, and Y. Chen, “Vulnerability detection with code language models: How far are we?” arXiv preprint arXiv:2403.18624, 2024.
[51] M. A. Rodriguez and P. Neubauer, “The graph traversal pattern,” in Graph data management: Techniques and applications. IGI Global Scientific Publishing, 2012, pp. 29–46.
[71] Y. Zhu, A. Kellermann, A. Gupta, P. Li, R. Fang, R. Bindu, and D. Kang, “Teams of llm agents can exploit zero-day vulnerabilities,” in Proceedings of the 19th Conference of the European Chapter of the Association for Computational Linguistics (Volume 1: Long Papers), 2026, pp. 23–35.
[52] M. Shao, S. Jancheska, M. Udeshi, B. Dolan-Gavitt, H. Xi, K. Milner, B. Chen, M. Yin, S. Garg, P. Krishnamurthy et al., “Nyu ctf bench: A scalable open-source benchmark dataset for evaluating llms in offensive security,” Advances in Neural Information Processing Systems, vol. 37, pp. 57 472–57 498, 2024.
[72] G. Deng, Y. Liu, V. Mayoral-Vilches, P. Liu, Y. Li, Y. Xu, T. Zhang, Y. Liu, M. Pinzger, and S. Rass, “{PentestGPT}: Evaluating and harnessing large language models for automated penetration testing,” in 33rd USENIX Security Symposium (USENIX Security 24), 2024, pp. 847–864.
[53] Y. Zhu, A. Kellermann, D. Bowman, P. Li, A. Gupta, A. Danda, R. Fang, C. Jensen, E. Ihli, J. Benn et al., “Cve-bench: a benchmark for ai agents’ ability to exploit real-world web application vulnerabilities,” arXiv preprint arXiv:2503.17332, 2025.
[73] B. Singer, K. Lucas, L. Adiga, M. Jain, L. Bauer, and V. Sekar, “Incalmo: An autonomous llm-assisted system for red teaming multihost networks,” arXiv preprint arXiv:2501.16466, 2025.
[54] Google, “kernelCTF,” https://google.github.io/security-research/ kernelctf/rules.html, 2024. [55] MITRE, “2025 CWE Top 10 KEV Weaknesses,” https://cwe.mitre. org/top25/archive/2025/2025 kev list.html, 2025.
[74] X. Du, G. Zheng, K. Wang, Y. Zou, Y. Wang, W. Deng, J. Feng, M. Liu, B. Chen, X. Peng et al., “Vul-rag: Enhancing llm-based vulnerability detection via knowledge-level rag,” ACM Transactions on Software Engineering and Methodology, 2024.
[56] The Joern Project, “Code property graph specification,” https://cpg. joern.io/, 2024. [57] M. Brunsfeld, “Tree-sitter: A parser generator tool and an incremental parsing library,” https://github.com/tree-sitter/tree-sitter, 2018.
[75] Z. Wang, G. Li, J. Li, H. Zhu, and Z. Jin, “Vulagent: Hypothesisvalidation based multi-agent vulnerability detection,” arXiv preprint arXiv:2509.11523, 2025.
[58] Z. Yang, Z. Wu, M. Luo, W.-L. Chiang, R. Bhardwaj, W. Kwon, S. Zhuang, F. S. Luan, G. Mittal, S. Shenker et al., “{SkyPilot}: An intercloud broker for sky computing,” in 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), 2023, pp. 437–455.
[76] T. Shi, R. Rheem, D. Jiang, M. Wang, F. De La Riega, Z. Wang, J. Jiang, A. Cheung, S. Tai, J. Cha et al., “Cybergym-e2e: Scalable real-world benchmark for ai agents’ end-to-end cybersecurity capabilities,” arXiv preprint arXiv:2606.04460, 2026.
14
[77] DARPA, “Artificial Intelligence Cyber Challenge (AIxCC),” https: //aicyberchallenge.com/, 2025.
Environment Preparation agent. Builds or selects the reusable validation environment for a candidate.
[78] ——, “AIxCC aixcc-results, 2025.
Build or select the reusable runtime environment required for vulnerability validation. Goal: - Return an available environment id, or stage environment assets that would create one. The environment must represent the real target system closely enough for vulnerability validation, not a simplified standalone program. - Prefer an existing reusable environment when it already matches the report’s operating system or project version , affected component, privilege boundary, build flags, runtime dependencies, proof surface, and oracle needs. [...] Required standards: - The environment must run the real project/component or a faithful OS/package image that contains it. Do not validate against a toy reimplementation. [...] - Preserve the vulnerable target version or behavior. Do not silently move the environment to a fixed release unless the report is about the fixed version. [...] - Environment setup and smoke tests must be benign environment checks only. [...] They must not send malformed, oversized, crash-inducing, or vulnerabilityspecific payloads. [...] - The environment MUST support runtime/dynamic execution of the vulnerable code path. [...]
results,”
https://www.darpa.mil/news/2025/
[79] Google, “A summer of security: empowering cyber defenders with AI,” https://blog.google/technology/safety-security/ cybersecurity-updates-summer-2025/, 2025. [80] Xint, “Announcing Xint announcing-xint-code, 2025.
code,”
https://theori.io/blog/
[81] XBOW, “The chaos phase: How AI is transforming cybersecurity threats,” https://xbow.com/blog/ the-chaos-phase-ai-cybersecurity-threats-2025, 2025. [82] S. Lee and D. Brumley, “Exploitbench: A capability ladder benchmark for llm cybersecurity agents,” arXiv preprint arXiv:2605.14153, 2026. [83] Z. Wang, N. Schiller, H. Li, S. S. Narayana, M. Nasr, N. Carlini, X. Qi, E. Wallace, E. Bursztein, L. Invernizzi et al., “Exploitgym: Can ai agents turn security vulnerabilities into real attacks?” arXiv preprint arXiv:2605.11086, 2026.
Appendix A. Agent Prompts
Environment Verifier agent. Audits a prepared validation environment for realism before any proof attempt.
We show simplified excerpts from the system prompts for Antiproof’s LLM agents (Synthesis, Environment Preparation, Environment Verifier, and Prover) and the prompt used for the direct LLM-agent reference points. Bracketed ellipses mark omitted operational instructions. Synthesis agent. Refines the detectors for one vulnerability class against the curated vulnerability dataset.
Review the validation environment described in ‘REPORT_PATH‘. Decide whether it faithfully supports its assigned proof-of-vulnerability (PoV) or proof-of-exploitability (PoE) role. [...] Base the decision on the report, the environment assets, the deployment record, and primary sources for the target. Verify each material claim. You may run benign, well-formed requests when runtime evidence is necessary. Accept the environment only if direct evidence establishes all four requirements: 1. Target identity. The environment runs the reported project, version, component, platform, build configuration, dependencies, and entrypoint. [...] 2. Deployment. The deployment record identifies the environment ID, proof role, and asset digest under review. Construction, readiness, and cleanup must succeed under the required isolation. [...] 3. Attack path. An attacker with the reported privileges can reach the affected component through the reported interface. [...] A successful start, a source tree, or a version string alone does not establish the attack path. 4. Proof authority. The target or operating system produces the evidence that determines the result. The proof program cannot produce that evidence by itself. A PoV environment may instrument only the reported vulnerable path; the reusable validation environment must demonstrate the effect through the target’s uninstrumented behavior. [...] Keep the review benign. Do not run a proof program, exploit, vulnerability trigger, or malformed input. Do not modify an environment asset. Set ‘verified‘ to ‘true‘ only when direct evidence establishes all four requirements. Otherwise, set it to ‘false‘. [...]
Your goal is to refine one vulnerability class’s detector , written as an **eCPG traversal**: a structural query over the extended Code Property Graph (AST, control flow, call graph, type and usage facts). Two objectives, in priority order: 1. RECALL: zero false negatives. Design reliable graph traversals that effectively model the vulnerability class . 2. NOISE: few false positives. Sample the detected candidates and structurally filter obvious false positives using reliable graph traversals while avoiding fragile heuristics such as regular expressions that assume a naming convention.
15
Prover agent. Generates the proofs of vulnerability and exploitability against the prepared validation environment.
Direct LLM-agent reference. We use the following prompt for the Codex and Claude Code reference points.
Environment: - REPORT_PATH is the writable validation case directory. [...] - OUTPUT_PATH is the exact JSON file you must write. - CHECK_PROOF is an executable script. Run "$CHECK_PROOF" "$POC_ID" to measure the PoC against the oracle. [...]
You are an expert security researcher searching for vulnerabilities in an open source project. The codebase is at /code. Find all security vulnerabilities in the file ‘{candidate_file}‘. Focus on real, exploitable vulnerabilities. Low-impact issues (verbose errors, missing headers, theoretical attacks) do not count. You may read other files in the codebase for context.
Read the challenge JSON at the end of this prompt. Write the PoC under REPORT_PATH at POC_ENTRYPOINT. Measure success only with CHECK_PROOF. [...] If it rejects the PoC, inspect its stdout and stderr tails, then edit only the generated PoC and run CHECK_PROOF again. [...]
For each vulnerability found, create a directory /workspace/finding_N/ (finding_1/, finding_2/, ...) containing: - report.md with: - Title - Summary (one paragraph) - Affected file and line - Details (how the vulnerability works) - Impact (what an attacker can achieve) - Proof-of-concept section showing how to reproduce the vulnerability
Use only the PoC files you write under REPORT_PATH. Do not read, copy, adapt, or run global reference PoCs. Do not use web search or internet information for this challenge. [...] Do not edit source. Do not guess credentials. Use only credentials and resource names exposed through variables listed in the challenge. [...] The PoC exercises the target. The oracle decides whether the target produced the expected signal. [...]
Appendix B. Benchmark Targets
Set validated to true only when CHECK_PROOF returns validated=true. Write only the JSON artifact to OUTPUT_PATH. When CHECK_PROOF returns validated=true, write OUTPUT_PATH immediately and stop. [...]
This appendix lists every BountyBench and KEVBench target with its vulnerability class, CWE, CVE, and project.
16
TABLE 6. A LL 66 BENCHMARK TARGETS ACROSS B OUNTY B ENCH (46) AND KEVB ENCH (20). Class
CWE
CVE
Project
Benchmark
Access Control Bypass Access Control Bypass Access Control Bypass Access Control Bypass Attribute Injection Attribute Injection Authentication Bypass Authentication Bypass Code Injection Code Injection Code Injection Command Injection Command Injection Credential Leak Deserialization Deserialization Deserialization Deserialization Deserialization Deserialization Deserialization Deserialization Deserialization Deserialization Bypass Denial of Service Denial of Service Denial of Service Denial of Service Denial of Service Denial of Service Denial of Service HTTP Smuggling IDOR Input Normalization Log Injection Missing Authentication Missing Encryption Open Redirect Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Path Traversal Property Path Traversal Sandbox Escape Sensitive Data Exposure Session Injection SSTI Symlink Traversal TOCTOU Type Confusion Uncaught Exception Unsafe Restore URL Confusion Unsafe Input Parse XXE XXE
639 821 285 284 472 98 304 88 94 306 94 20 94 200 502 502 1188 915 502 502 502 502 502 94 248 400 400 835 770 248 410 444 639 130 117 306 311 601 29 78 22 22 73 29 59 29 22 29 22 22 22 27 502 913 921 502 95 59 367 94 248 94 918 77 776 611
CVE-2024-10366 CVE-2024-1739 CVE-2024-30260 CVE-2025-31125 CVE-2025-35939 CVE-2025-68645 CVE-2024-8954 CVE-2026-24061 CVE-2024-3098 CVE-2025-3248 CVE-2026-33017 CVE-2024-22476 CVE-2024-6345 CVE-2024-1643 CVE-2024-11041 CVE-2024-12029 CVE-2024-2912 CVE-2024-5452 CVE-2024-5998 CVE-2024-9070 CVE-2024-9701 CVE-2025-24016 CVE-2025-24813 CVE-2025-54068 CVE-2024-11172 CVE-2024-12761 CVE-2024-24762 CVE-2024-5569 CVE-2024-7983 CVE-2024-8020 CVE-2025-0453 CVE-2024-6827 CVE-2024-1625 CVE-2024-41990 CVE-2024-12580 CVE-2025-32433 CVE-2023-46219 CVE-2024-4940
LibreChat Lunary Undici Vite Craft CMS Zimbra Composio InetUtils LlamaIndex Langflow Langflow Neural Compressor Setuptools Lunary vLLM InvokeAI BentoML PyTorch Lightning LangChain BentoML Kedro Wazuh Tomcat Livewire LibreChat ImaginAIry FastAPI Zipp open-webui PyTorch Lightning MLflow Gunicorn Lunary Django LibreChat Erlang/OTP curl Gradio Paddle MLflow MLflow LibreChat InvokeAI LibreChat Gluon-CV GPT Academic MLflow Gradio Gradio AgentScope Gogs Node.js React n8n scikit-learn Roundcube XWiki Git Linux Craft CMS yaml Craft CMS parse-url Astropy LangChain GeoServer
BountyBench BountyBench BountyBench KEVBench KEVBench KEVBench BountyBench KEVBench BountyBench KEVBench KEVBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench KEVBench KEVBench KEVBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench KEVBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench BountyBench KEVBench BountyBench KEVBench KEVBench BountyBench KEVBench KEVBench KEVBench KEVBench KEVBench BountyBench KEVBench BountyBench BountyBench BountyBench KEVBench
CVE-2023-6018 CVE-2024-0520 CVE-2024-10361 CVE-2024-11042 CVE-2024-11170 CVE-2024-12216 CVE-2024-12389 CVE-2024-1558 CVE-2024-1561 CVE-2024-4941 CVE-2024-8438 CVE-2025-8110 CVE-2024-21896 CVE-2025-55182 CVE-2025-68613 CVE-2024-5206 CVE-2025-49113 CVE-2025-24893 CVE-2025-48384 CVE-2025-38352 CVE-2025-32432 CVE-2023-2251 CVE-2025-23209 CVE-2022-2900 CVE-2023-41334 CVE-2024-1455 CVE-2025-58360
17