Yes, I ran @opentaint, our static taint analyzer, on a mid-sized Java project (~100K lines, ~0.65 MB of bytecode), checking for the absence of path-traversal data flows. The numbers come from that run, though the estimates for AI and formal verification are speculative. The problem with formally proving dataflow properties across a whole project is that you need abstract dataflow semantics for every method. AI can generate those, sure, but without proving them sound, you're just trusting whatever it came up with. So let's assume we do it properly: embed JVM bytecode into a formal verifier, have AI generate field- and context-sensitive (but path-insensitive, for a fair comparison) semantics for each method, prove them sound, and then prove or disprove the security property. We can even assume the external library models and security rules are already there, so we don't count their cost. For this one project and one property, the taint analyzer produced ~440 MB of dataflow summaries and fixpoint artifacts. Based on that, I estimate ~28.5B input tokens and ~145M output tokens for a cold AI-based formal verification run. That's around $11,500 at Opus 5.5 API prices. And this isn't just a one-time cost: at least some of that information would need to be recomputed whenever the codebase changes, though unchanged proofs could be reused. Since these estimates are based on the bytecode size, method summaries, and fixpoint data from the taint analysis, actual costs could differ significantly depending on how much work the proof engine handles itself and how much can be reused. But the more work you offload to the proof engine, the closer you get to having it perform the static analysis itself. Anyway, take the numbers with a grain of salt. Meanwhile, static taint analysis computes the same dataflow properties in minutes on a CPU, without any API token costs. That's why, before rewriting a codebase in another language or spending tokens on AI agents proving dataflow properties, I'd suggest trying static taint analysis first. It has its own problems, of course. Performance can vary widely between projects, and what works well in one can struggle in another. To me, a much more interesting direction is making these analyzers flexible and interactive enough that AI agents can tune them for a particular project, identify bottlenecks, and work around them, rather than pushing agents to do the whole analysis themselves

New on our Frontier Red Team blog: using Claude to formally verify software at large scale. Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time). With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks. Read our research in full here: anthropic.com/research/forma…

Speculative prediction: Over the next 12-24 months the need to formally verify everything will turbocharge demand for frontier AI the way the y2k bug turbocharged IT spending in the late 90s. Then like y2k, after the bug is mostly fixed theres likely a market hangover.

👀 @hillelogram 📎 Formal Verification of LLM-Generated Code ssvlab.github.io/lucasccorde…

Lean Verified Transformers (srush.github.io/lean-transfo…) In which we prove a bunch of Transformer invariants from scratch in Lean, and speculate about how hard it would be to do that for the rest of the world's code.

OpenTaint (@opentaint) leads recall. JVM-only, but that may be exactly the scope you need. A good reminder that language breadth and finding real flows are separate strengths.

Which taint analyzer would you trust to check you code? We tested eight across 852 frozen cases in 13 languages. Nobody swept the board: speed, precision, recall, and coverage pull in different directions. Here.s the breakdown: blog.brokk.ai/the-taint-anal…

$20,000 spent across 1,000 security reviews. One found something. All expired. That's what it costs when every review starts from scratch. The reviewer learns your trust boundaries, finds the vulnerability patterns, writes the report. Next sprint, new code ships. Different reviewer. Learns everything again. Finds the same categories of bugs. Maybe misses the ones the last reviewer caught. Meanwhile, 44% of AI-generated code contains known security flaws. Vulnerability exploitation just became the #1 breach entry point for the first time in 19 years. And LLM-only security reviews reproduce only 14% of their findings across five runs on the same code. The tools exist. The security knowledge doesn't stick. OpenTaint just changed that math. It's an open source taint analysis engine that turns one-off security reviews into unlimited reusable scans. The key: it combines the flexibility of model reasoning with the consistency of formal program analysis. Here's the loop: - Discover: An AI agent reviews your code. Learns trust boundaries and vulnerability patterns. Captures them as an informal specification in plain language. - Enact: Converts that informal spec into formal taint rules and dependency models. Machine-readable. Deterministic. Repeatable. - Scan: Runs formal program analysis across the ENTIRE project. Not just the files the agent looked at. Everything. In seconds. - Triage: Confirms real findings. Tunes away false alarms. Every refinement improves the next scan. Each cycle adds reusable knowledge. The first review costs $20. Every scan after that is essentially free. That's a 1,000x cost reduction on the same security coverage. It already found CVE-2026-58138. A 182-step taint trace from an unauthenticated HTTP endpoint to remote code execution via GraalJS. Real vulnerability. Real CVE. Real production impact. In head-to-head comparisons across five analysis depth levels (direct return, local dataflow, inter-procedural, field sensitivity, virtual dispatch), OpenTaint detected vulnerabilities at every level. Semgrep's pattern matching missed four of five. Even the taint engines of Semgrep and CodeQL fell short on the two deepest levels. Supports Java, Kotlin, and Spring (deep framework support). Go in alpha. Python, C#, JavaScript, and TypeScript on the roadmap. Fully open source. Apache 2.0 engine. MIT CLI. No vendor lock-in. Install in one line: npm install -g @seqra/opentaint @seqradev

Next time you get access to Mythos/Fable — you know what to do: opentaint.org/blog/appsec-ag…