SAST Is Dead, Long Live SAST!
AI agents have beaten SAST at finding bugs. So what's left for SAST to do? Quite a lot, as it turns out. Finding a bug and proving an entire class of bugs is absent are two very different problems. And when we put a price on the latter, SAST suddenly looked a lot less dead.
As a tool for finding bugs, SAST is dead. Give an AI agent a codebase today, and it can read the code like an experienced reviewer, follow a hunch across a dozen files, and even write an exploit to prove a bug is real. Pattern-matching SAST can’t keep up. It’s stuck trading false positives for false negatives, and no amount of rule tuning can solve that problem. Even advanced dataflow analysis has its limits: if a bug falls outside what the rules cover, it gets missed.
We saw exactly this with Conductor. CodeQL, Semgrep, and our own stock rules produced half a hundred findings between them, but not one caught the unauthenticated RCE. The reason was simple: none of the stock rule sets recognized the GraalVM script evaluator as a dangerous sink. Our agent, however, successfully found the vulnerability and wrote the rule needed to detect it.
-
POST /api/workflowThe request body can carry a whole workflow definition, script included.Stock rules: a known source -
evaluator.evaluate(…)An INLINE task hands the script from the definition to an evaluator. -
.allowHostAccess(ALL).option(…)The evaluator builds a GraalVM context with full access to the host JVM.Stock rules: no model of the builder. The agent wrote one. -
context.eval("js", script)The request's script runs inside that context.Stock rules: not a sink. The agent wrote the rule. - The script runs OS commands as the Conductor process.
So if the question is which tool finds the most bugs, the agent wins, and it isn’t even close. But defenders face a different, much harder question: how do you know an entire class of bugs is absent from your code?
Finding bugs isn’t proving they’re gone
Anthropic recently published research on making formal verification practical with LLMs, and it opens with a line that captures the problem well:
“Most software is riddled with bugs, which AI can now easily find and exploit. The standard defenses against cyberattacks are no longer sufficient: we need ways to prove that code is free of bugs.”
The logic is uncomfortable but simple. Attackers have access to the same agents you do, so finding bugs faster isn’t enough to keep you safe. You have to find every bug, while an attacker only needs to find the one you missed. What you really want is to be able to say something like “no request parameter in this codebase can ever reach a file-system call,” with stronger evidence to back it up than “an agent looked and didn’t find anything.”
Formal verification can give you exactly that kind of guarantee. For decades, though, it has been too expensive for most real-world projects. Anthropic’s research argues that AI is finally bringing the cost down. We like where this is heading, but it leaves us with two questions: how much does a formal proof actually cost today, and is there already a cheaper way to establish some of the properties defenders care about?
Cristiano Calcagno, one of the creators of Facebook’s Infer static analyzer, has already offered an answer to the second question:
“Part of formal verification can be replaced by more efficient static analysis, and part of static analysis by better programming language design.”
We agree. In the rest of this post, we’ll put some speculative numbers on what formal verification costs today, then show how static taint analysis can prove specific properties that matter to defenders at a fraction of the cost.
What a proof costs
We ran OpenTaint, our static taint analyzer, on a mid-sized Java project with 100K lines of code and 0.65 MB of bytecode. We checked a specific security property: no request-controlled data can reach a dangerous file-system call, or, to be precise, there are no path-traversal flows. OpenTaint finished in about a minute of CPU time, without spending a single API token.
But what would it cost to prove the same property using AI and a general-purpose formal verifier?
To make the comparison fair, let’s assume we do it properly. First, we embed the JVM bytecode into a formal verifier. Then we have AI write field- and context-sensitive dataflow semantics for every method, keeping the analysis path-insensitive, just like OpenTaint. We’d also need to prove those semantics are sound. Otherwise, we’re just trusting whatever the AI generated. Only then can we prove or disprove the security property itself. We’ll also assume the library models and security rules already exist, just as they do for OpenTaint, and leave their cost out of the estimate.
Most of the cost comes from writing the semantics and proving them sound, since every method needs both. For this one property, OpenTaint generated 440 MB of dataflow summaries and fixpoint data. That’s not a direct measure of proof complexity, but it gives us a rough idea of how much work is involved. Based on that, we estimate that an AI-driven verification run from scratch would require around 145 million output tokens and 28.5 billion input tokens. At Claude Opus 5.5 API prices, that works out to roughly $11,500.
How we got that number, and how much to trust it
- Output. At roughly 3 bytes per token, 440 MB of summaries and fixpoint data works out to about 145 million output tokens. This assumes the model writes every method’s semantics and the intermediate fixpoint state exactly once.
- Input. For everything the model writes, it needs context: the method’s bytecode, summaries of the methods it calls, and the surrounding proof state. At roughly 200 input tokens for every output token, that adds up to about 28.5 billion input tokens.
- Price. Opus 5.5 charges $4 per million input tokens, $20 per million output tokens, and $0.20 per million cached input tokens. That’s about $2,900 for output and $8,600 for input, assuming roughly 97% of input tokens are served from the prompt cache. Without caching, input alone would cost about $114,000, bringing the total to roughly $117,000.
These are ballpark numbers, and the actual cost could go either way.
- It could be lower if the model can express method semantics more compactly than the analyzer’s internal format, or if the proof engine handles more of the work. But the more work the proof engine takes on, the closer it gets to being a static analyzer itself.
- It could be higher because the estimate doesn’t account for failed proof attempts, retries, or the additional work needed to prove the semantics sound.
And this isn’t a one-time cost. Every code change can mean redoing part of the work, although proofs for unchanged code can be reused when their assumptions still hold.
The exact numbers matter less than the gap: a minute of CPU time versus thousands of dollars, for a single property in a single project. So before rewriting your codebase in another language (the second half of the quote) or paying AI agents to prove dataflow properties, it’s worth trying static taint analysis first.
Dataflow SAST is lightweight formal verification
How can an analyzer do in a minute what an AI-driven proof might cost thousands of dollars to do? Because we’re asking a much narrower question: whether data can flow from one part of the program to another. By focusing on dataflow properties, we can specialize both the specifications and the way we prove them, rather than building a general-purpose proof from scratch. The underlying ingredients are still the same. A formal proof needs three things: a specification, a model of the environment, and the semantics of the program. A taint analyzer works with the same three.
The first two are inputs: someone has to write the rules and build the models. The third is where most of the cost comes from in our estimate. But instead of having AI write and prove the dataflow semantics method by method, the analyzer computes them itself, along with the fixpoint for the whole project, without spending a single API token.
That speed comes with trade-offs. The analyzer approximates program behavior, and it isn’t fully sound. Expanding its coverage is a hard computational problem, especially when dealing with aliasing, reflection, and exceptions. Here’s what our analysis covers today and where its limits are:
- Flow
- Context
- Fields
- Dynamic dispatch
- Persistence
- External methods and frameworks as far as their models go
- Aliases
- Reflection
- Exceptions
Pushing those limits is one of our main goals. We want to prove more security properties automatically, without sacrificing the speed and practicality that make static analysis useful in the first place.
And there’s another direction we’re already exploring. For critical projects that need stronger guarantees, we could export the analyzer’s dataflow semantics and summaries into a general-purpose formal verifier, then let AI agents fill the remaining gaps in the proof. Instead of having AI build everything from scratch, static analysis would do most of the work, leaving agents to focus on what it can’t yet handle.
What dies and what survives
We’re not the only ones seeing verification as the future of SAST. At AI Engineer World’s Fair 2026, Sonar CEO Tariq Shaukat gave a talk titled In the Land of AI Agents, the Verifiers Are King. One of his slides makes a useful distinction: algorithmic verification handles things like dataflow and taint analysis, while agentic verification handles intent, business logic, and anomalies.
We agree. What survives is SAST as a prover. A tool that can say “this kind of flow cannot happen under these assumptions” gives you something a list of findings never could. And it can do that in minutes, consistently, on every commit, using the workflows teams already have: CI gates, SARIF reports, and pull-request checks. But to keep that role, analyzers need to expand what they can soundly cover and be explicit about their assumptions.
This also changes how we think about SAST’s oldest complaint: false positives. From a proof perspective, a false positive isn’t proof that a bug exists. It’s a case the analyzer couldn’t rule out. You address it much like a failed proof attempt: write code in ways the analyzer can reason about, and configure it to reflect your actual security assumptions, including known sanitizers and safe configurations. Following coding standards used to take real effort from developers. When agents write much of the code, that effort becomes much smaller.
Seen this way, agents and analyzers aren’t competing. They’re solving different parts of the same problem. The two inputs an analyzer can’t compute for itself, security rules and library models, are exactly the kind of work AI agents can help with. The rules are effectively formal security specifications, and our AppSec agent can write them, just as it wrote the missing Conductor rule. You pay for the agent’s work to create the rule once, and from then on, the analyzer checks every commit using CPU time.
That’s the future we see for SAST: agents help define what needs to be checked, and static analysis checks it continuously, cheaply, and with guarantees whose limits we can understand.
We want to take this further: make analyzers flexible and interactive enough that an agent can tune one for a specific project, find where it slows down, and work around the bottleneck, instead of trying to do the whole analysis itself.
Where to start
If SAST is going to have a second life as a prover, we believe that future should be open source. The rules, models, and assumptions behind its guarantees should be open to inspection, discussion, and improvement. That’s why we’re building OpenTaint in the open.
Install OpenTaint, ask your agent to write a rule for a security property you care about, and see what the analyzer can rule out in your own code. If you believe this is where SAST should be heading, give us a star on GitHub and help us build it.
SAST is dead, long live SAST!