Reaches

On May 21, Sonar acquired Gitar. Sonar already had SonarQube — static analysis across 40+ languages, deterministic verification of syntax, data flows, control flows, known vulnerability patterns. Same answer every run. Seventy-five percent of the Fortune 100 depend on it. Teams that use it are 44% less likely to experience outages from AI-generated code.

So why buy a second engine?

Because static analysis can't catch logical inconsistencies, functional verification problems, or design flaws — the things Sonar's own press release calls "tough to codify mathematically." Gitar uses LLM-based reasoning to find those. It reasons like a developer, evaluating code from first principles rather than predefined rules.

One company now ships two verification systems. One is deterministic. One is probabilistic. One can be pointed at an auditor. One cannot.

The Boundary

The split isn't temporary. Deterministic verification works because it reduces problems to formal specifications — that's what makes it deterministic. VeriCodeGen achieves 82% success rates in Dafny, 27% in Lean, but only for individual function correctness. Not architectural coherence. Not intent alignment. Not security invariants across composition. Pramaana, the formal verification startup with $27M from Khosla, isn't even doing code verification — it's doing domain reasoning verification for law and drug discovery, where the formal structure exists. Each vertical requires manual domain formalization by experts. Their Hardy prover showed that math-specific proof strategies don't transfer across domains.

The problems that matter most in software resist formalization. That's not a gap that closes with more investment. It's a property of the problems themselves — the same property that makes them hard, that makes them the things humans review.

$2.5 Billion Toward Reaching

The market knows which side of the boundary the problems are on. CodeRabbit raised $143M at a $1.5 billion valuation in August, runs 2 million LLM-based code reviews per week, serves 17,000 customers including Nvidia and Adyen. Qodo raised $120M total to build agentic verification tooling. The capital overwhelmingly flows to the probabilistic side — because that's where the problems are.

This is rational. The deterministic layer covers what it covers. It cannot expand to cover architectural coherence any more than a spell checker can evaluate an argument. Organizations need something that reaches the problems that matter. The probabilistic layer reaches them.

But reaching and verifying are different actions.

ACM TOSEM 2026 evaluated Copilot's LLM-based code review against realistic multi-file codebases. The system "frequently fails to detect critical vulnerabilities including SQL injection, cross-site scripting, and insecure deserialization." The failures concentrated in cases where the taint crossed file boundaries — the same cases the original generation missed. The reviewer has the same blind spot as the generator. The probabilistic layer reaches the problem and then fails at it in the same way the system it's supposed to check does.

Pricing the Boundary

The Sauce Labs Enterprise AI Code Verification Crisis report surveyed 400 U.S. executives. Ninety-two percent are not confident their safeguards would catch an AI-driven failure before users. Eighty-nine percent report positive ROI from AI testing tools. Qodo's 2026 report — 500 developers, 300 engineering leaders, separate questionnaires — found 89% had experienced an AI-related production incident, and only 3.7% say their existing processes are sufficient.

These aren't contradictions. They're the market pricing the formalizability boundary without naming it. The ROI is real — partial coverage is better than none, the deterministic layer genuinely catches things, the probabilistic layer catches some things. The doubt is also real — neither layer can verify what matters most. Both are true simultaneously.

I wrote about this recursion eighteen months ago: every layer of automated verification creates a new unverified layer. What I didn't anticipate was the market building that recursion into a $2.5 billion product category at 30-40% annual growth. The Verifier isn't a theoretical risk anymore. It has a valuation.