Antiproof: Synthesizing Vulnerability Detectors and Proofs of Exploitability

Image generated by AI

TLDR

• What: Antiproof combines LLM-synthesized static code analysis queries (using an extended Code Property Graph) with automated, sandboxed proof-of-exploitability oracles to achieve both high-recall vulnerability detection and zero-false-positive automatic validation.
• Who's at risk: Large-scale deployed infrastructure and machine learning systems (including Ray, SGLang, vLLM, and LiteLLM) whose complexity makes traditional taint analysis and manual code review impractical.
• Key number: Antiproof detected 64 out of 66 vulnerabilities (97% recall) in benchmark tests, outperforming static-analysis baselines like Semgrep (26% recall) and CodeQL (9% recall) while automatically verifying exploits to eliminate false positives.

Finding critical software bugs before bad actors do has historically been a zero-sum game between scalability and precision. Static analysis tools scale easily but suffer from high false-positive rates and struggle with semantic, non-memory-safety flaws. Conversely, raw LLM-based agents can find deep logical flaws but are prohibitively expensive for continuous integration (CI) environments—for example, Anthropic reported running Claude Mythos roughly a thousand times on OpenBSD at a total cost of USD 20,000 just to find a single zero-day, still requiring manual human validation afterward.

Presented in July 2026, Antiproof is an end-to-end vulnerability discovery system designed to solve this cost-accuracy tradeoff. By combining neuro-symbolic detector synthesis with sandboxed proof-of-exploitability (PoE) oracles, Antiproof achieves near-perfect recall (97%) while generating deterministic, executable proofs of concepts (PoCs) to entirely automate triage. The tool has already uncovered several hundred zero-days in production software, yielding 12 CVE assignments across critical AI infrastructure platforms, including Ray, SGLang, vLLM, and LiteLLM.

Threat Model

Antiproof evaluates target repositories under a realistic network-attacker threat model:

Background & Problem Setup

Existing systems trade off cost, recall, and precision. In Figure 2, the authors illustrate a motivating example (CVE-2026-24061 in GNU InetUtils telnetd) where traditional static analysis fails. Because the application uses a custom memory allocator (obstack_grow), standard taint-tracking tools like CodeQL or Joern lose the data-flow path between the source (getenv("USER")) and the sink (execv).

To place Antiproof in context, Table 1 compares existing vulnerability discovery paradigms across key dimensions (using ●, ◐, and ○ to denote full, partial, and no support, respectively):

Methodology

Antiproof operates through three decoupled subsystems, illustrated in Figure 3: Synthesis, Detection, and Validation.

+-------------------------------------------------------+
|                       SYNTHESIS                       |
|  [Vulnerability Dataset] -> (LLM Synthesis Agent)     |
|                                    |                  |
|                                    v                  |
|                         [Synthesized Detectors]       |
+-------------------------------------------------------+
                                     |
                                     v
+-------------------------------------------------------+
|                       DETECTION                       |
|  [Target Codebase] ------> (Antigraph Engine)         |
|                                    |                  |
|                                    v                  |
|                          [Candidate Violations]       |
+-------------------------------------------------------+
                                     |
                                     v
+-------------------------------------------------------+
|                      VALIDATION                       |
|  [Candidates] -----------> (Prover Agent)              |
|                                    |                  |
|                                    v                  |
|                        [Challenge-Response Oracle]    |
|                                    |                  |
|                                    v                  |
|                           (Verified Bug/PoE)          |
+-------------------------------------------------------+

1. Synthesis (The Offline Loop)

Instead of forcing an LLM to scan a massive codebase line-by-line, Antiproof uses an LLM offline to synthesize reusable, high-recall static detectors. These detectors query an Extended Code Property Graph (eCPG). The eCPG extends standard CPGs (which map ASTs, control flow, and data dependencies) by dynamically inserting virtual nodes and virtual edges.

For instance, as shown in Figure 4, when evaluating a configuration file reader/writer discrepancy (e.g., KEV CVE-2025-48384 in Git), the synthesis agent injects a virtual node representing the shared .git/config resource. This connects the writer (write_pair) and the reader (parse_value), allowing a simple graph traversal query to flag the semantic parser discrepancy.

2. Detection (The Fast Scanner)

Rather than executing slow data-flow analysis or resolving Program Dependence Graphs (PDGs), Antiproof's custom Rust-based scanning engine, Antigraph, runs optimized Breadth-First Search (BFS) reachability over the eCPG. To scale to codebases with millions of lines of code, the system applies two specific filters:

• Scope Detection: Decomposes repositories into smaller, independently analyzable subsystems.
• Attack Surface Filter: Identifies attacker-reachable entry points (e.g., HTTP handlers, gRPC endpoints) and trims non-reachable code paths from the traversal search space.

3. Validation (The Triage Oracle)

Every flagged candidate is sent to a deterministic, sandboxed validation environment (Docker or QEMU). Instead of relying on an "LLM-as-a-judge" (which is highly prone to hallucination and reward hacking), Antiproof uses Proof-of-Exploitability (PoE) Oracles. These run as a deterministic challenge-response protocol.

For example, to validate an Arbitrary Code Execution (RCE) candidate:

1. The oracle generates a cryptographically secure random secret $s$.
2. It ensures /challenge/secret does not exist in the sandbox.
3. It mounts a script template /challenge/rce.sh such that executing the script would write the secret $s$ into /challenge/secret.
4. The Prover Agent (an LLM) is given access to the sandbox network and must generate an exploit payload that successfully forces the target application to run /challenge/rce.sh.
5. The oracle checks the sandbox state. If and only if the secret $s$ is correctly written, the exploit is validated.

This completely shifts the manual review bottleneck. Security engineers no longer triage thousands of noisy static analysis alerts; they only audit the small, deterministic set of validation environments and capabilities.

Key Results

1. Known Vulnerability Benchmark Performance

Antiproof was evaluated against BountyBench (46 real-world vulnerabilities) and a curated dataset named KEVBench (20 active, exploited-in-the-wild vulnerabilities from 2025/2026). As described in Section 5.3 and detailed in Table 3, the results are decisive:

Note: Baselines like RepoAudit and KNighter showed 0% recall because their specialized scopes (e.g., limited to only three vulnerability types or Linux-specific use-after-free templates) did not map to the broader benchmark sets.

2. Scanning Speed and Scaling

By avoiding expensive PDG construction and implementing BFS reachability in native Rust, Antiproof's Antigraph engine scales linearly. Figure 7 illustrates the efficiency comparison against Joern:

• Throughput: Antigraph scanned the entire benchmark suite in a median of 2.3 minutes—a 25x speedup compared to Joern's 59 minutes (Figure 7a).
• Peak Scaling: On the massive Linux kernel codebase (51,000 scoped files), Antigraph completed its scan in under 140 seconds (Figure 7b).

3. Real-World Zero-Day Discovery

Across 50 widely deployed systems (representing 136 million lines of code), Antiproof generated 17,574 candidate hits, which were automatically triaged down to 1,212 Proofs of Vulnerability (PoVs), ultimately yielding 510 fully validated Proofs of Exploitability (PoEs) (Figure 6).

The execution cost was remarkably low. While proprietary LLM searches often run into tens of thousands of dollars, Antiproof reproduced the OpenBSD SACK null-pointer dereference for a mere USD 0.46 in API tokens, and a FreeBSD vulnerability (CVE-2026-4747) for USD 1.73.

Limitations & Open Questions

While Antiproof's results are impressive, several elements require critical skepticism:

1. Vulnerability Class Blindspots: Table 2 shows that Antiproof currently fails to cover Cross-site scripting (XSS). Because client-side code execution runs in the victim's browser rather than the server sandbox, it is incredibly difficult to validate using a straightforward back-end challenge-response oracle.
2. Oracle Design Bottleneck: Although validating individual bugs is automated, defining the capability-based oracle environments still requires expert human oversight. If an attacker's exploit path relies on a chain of multiple distinct logical errors that do not cleanly map to existing primitives (such as simple File Read or RCE), the validation step will fail to prove exploitability.
3. Data Contamination: Because the evaluated models (gpt-5.5, claude-opus-4.6) are highly advanced, there is an inherent risk that they memorized historical BountyBench and KEVBench bug reports during pre-training, artificially inflating recall. The authors attempted to counter this by scanning post-cutoff 2025/2026 KEVs, but complete isolation is difficult to guarantee.

What Practitioners Should Do

To defend codebases against automated discovery engines like Antiproof, security teams should implement the following controls:

1. Build Local Capability-Based Oracles in CI: Do not rely on basic static analysis. Implement automated, sandboxed testing environments (e.g., using Docker or lightweight microVMs like Firecracker) that explicitly test for security boundaries. Write end-to-end integration tests that try to trigger remote code execution or unauthorized database reads, using randomized secrets to verify that isolation models are structurally sound.
2. Audit eCPG Attacker Reachability: Map your applications' true attack surfaces. Use AST parsers (such as tree-sitter) to flag any public-facing API routes, RPC endpoints, or deserialization routines that accept untrusted input, and ensure they are bound by strict schemas (e.g., strict Pydantic parsing or Protocol Buffers) before reaching internal functions.
3. Incorporate State-Machine Verification: Antiproof's success in finding logic errors (like authentication bypasses) highlights the weakness of stateless firewalls. Implement stateful verification within your API gateways, ensuring that a state-based challenge (such as session-validity tokens) is cryptographically bound to all downstream internal system requests.

The Takeaway

Antiproof demonstrates a fundamental shift in vulnerability research. By abandoning the slow and expensive approach of letting LLMs read entire codebases, and instead using LLMs to compile fast, structural eCPG queries, we can scan enterprise-scale systems at negligible cost. When these hybrid scanners are combined with deterministic, capability-based test sandboxes, false positives disappear—providing defenders with a highly scalable, automated pipeline to find and patch zero-days before attackers can exploit them.

Den's Take

What excites me about Antiproof is that it tackles the absolute bane of automated vulnerability discovery: the crushing triage tax of false positives. Traditional static analysis tools like CodeQL or Semgrep are notoriously brittle when they hit customized data flows—such as the custom allocator issue in the telnetd example, which CodeQL misses entirely, while its overall benchmark recall stands at a mere 9%. Antiproof's neuro-symbolic approach, which uses LLMs to synthesize Code Property Graph queries and validates them with a sandboxed proof-of-exploitability (PoE) oracle, is the right way forward. Achieving a 97% recall (detecting 64 out of 66 benchmark vulnerabilities) while uncovering 12 real-world CVEs in critical AI infrastructure like vLLM, LiteLLM, and Ray is highly impressive.

This hybrid design of combining static query generation with automated execution loops mirrors the core philosophy of self-evolving agentic operating systems for web exploitation, where LLMs must operate within tight, deterministic feedback environments to successfully navigate and exploit complex software targets. My main concern is that Antiproof's reliance on sandboxed execution means its recall will still be fundamentally limited by how representative the sandbox setup is of production state. Nonetheless, eliminating the manual triage bottleneck for massive codebases proves that neuro-symbolic synthesis has officially graduated from academic toy to practical security tool.