1 Introduction↩︎

Exploitable vulnerabilities are the most common initial-access 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 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]–[14].

1.1pt

Large language models (LLMs) have shown strong code-reasoning capabilities that can help address this challenge by automating parts of vulnerability discovery, exploitation, and patching [7], [33]–[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]–[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-of-concept generation [30]–[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.

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 detector-specific 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. 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.

2. 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.

3. 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.

2 Background↩︎

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]–[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.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 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.3 Code Property Graphs↩︎

A code property graph (CPG) is a graph representation of code that combines the abstract syntax tree, control-flow 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 data-flow analysis tools, such as CodeQL and Joern. Antiproof uses LLMs to generate and refine eCPG queries that detect a wide range of vulnerability classes.

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]–[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, system-level mitigations may prevent exploitation, and some bugs are challenging to exploit on their own, such as an out-of-bounds read of a single byte).

We define a proof of exploitability (PoE) as an end-to-end 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.

2.5 Known Exploited Vulnerabilities (KEVs)↩︎

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.

3 Design↩︎

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:

• 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↩︎

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.

To scan large systems effectively, Antiproof refines the following three detectors:

1. 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.

2. 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.

3. 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.

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.

3.2 Detection↩︎

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 attacker-controlled 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, \(R_S\), as well as the set of methods that can be reached from attacker-controlled entry points \(R_E\), and adds the sink as a candidate if it is attacker-reachable, that is, \(R_S \cap R_E \ne \emptyset\). 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).

3.3 Validation↩︎

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.

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 proof-of-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 6, the validation environment runs the target system alongside an exploitability 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:

• 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).

Formally, let \(E\) be a validation environment, let \(C\) be an attacker capability (primitive), and let \(\pi\) be a candidate executable proof. We define the oracle \(O_C\) as: \[O_C(E, \pi) = \begin{cases} 1 & \text{if \pi demonstrates C against E,}\\ 0 & \text{otherwise.} \end{cases}\] A rejected proof, \(O_C(E, \pi) = 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 client-side vulnerabilities such as cross-site scripting (XSS), since 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.

6pt

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, 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 open-source 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:

• 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.

• 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 use-after-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 9, 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.

5.2 Metrics↩︎

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 (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).

2.0pt

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 Co-RedTeam’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 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.

5.4 RQ2: Zero-Day Discovery↩︎

We evaluate Antiproof on 50 widely deployed open-source 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 7). Due to time constraints, we selected 100 findings for manual review and coordinated disclosure. Antiproof has uncovered critical and high-severity 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 per-project 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 gpt-5.3-codex for less than USD 612, a \(33\times\) lower cost, and reproduces the Mythos findings, SACK null-dereference 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.

3pt

5.5 RQ3: Detector Efficiency and Scalability↩︎

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 a cold cache, rebuilding all graphs in every iteration, and reach identical recall (64 of 66).

Throughput. As Figure 8 (a) shows, Antigraph scans all benchmark targets 25\(\times\) faster than Joern, a median of 2.3 versus 59 minutes across 5 trials.

Scaling. As shown in Figure 8 (b), Antigraph’s median per-target time is 27.3 s, 92\(\times\) 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 8 (c), Joern spends 92% of its run time building and loading CPGs. By contrast, Antigraph is 25\(\times\) 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.

5.6 RQ4: Component Contributions↩︎

We run the following ablations to measure how Antiproof’s components contribute to recall and cost:

• \(-\)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.

2pt

Results. The Detection ablations in Table ¿tbl:tab:ablations? 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\(\times\) 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\(\times\) 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\(\times\) 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 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 LLM-generated threat models, allowing Antiproof to focus on in-scope 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, we additionally evaluate Antiproof’s effectiveness in zero-day 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. Query-based 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 memory-safety and combines neuro-symbolic static analysis for high-recall 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 taint-based 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]–[35], [61], [69]–[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 false-positive rates [39], Antiproof uses efficient static detectors to continuously scan large systems and proofs of exploitability for automatic validation.

Vulnerability Validation. Proof-of-Vulnerability (PoV) test generation has been extensively studied [33]. Recent works, including AnyPoC [30], FaultLine [31], and CVE-GENIE [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]–[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 memory-safety 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.

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 open-source 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.

Acknowledgments↩︎

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.

9 Agent Prompts↩︎

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.

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.

Environment Preparation agent. Builds or selects the reusable validation environment for a candidate.

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 vulnerability-specific payloads. [...]
- The environment MUST support runtime/dynamic execution of the vulnerable code path. [...]

Environment Verifier agent. Audits a prepared validation environment for realism before any proof attempt.

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`. [...]

Prover agent. Generates the proofs of vulnerability and exploitability against the prepared validation environment.

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. [...]

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. [...]

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. [...]

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. [...]

Direct LLM-agent reference. We use the following prompt for the Codex and Claude Code reference points.

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.

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

10 Benchmark Targets↩︎

This appendix lists every BountyBench and KEVBench target with its vulnerability class, CWE, CVE, and project.

References↩︎