Current State of Verification As of late October 2026, AI systems can generate massive amounts of proof text, but no public result meets the strict whole-system criteria. Anthropic and Theorem’s recent release of about 180M lines of Rocq proofs covers 239 OSS-Fuzz entry points across 123 libraries LLMs are making formal software verification feasible at a ... Anthropic Says Claude Proved Security Properties Across ... LLMs are making formal software verification feasible at a .... However, these proofs only guarantee bounded crash-freedom (for inputs under 64 MB), target single-threaded static RISC-V binaries instead of the x86-64/ARM64 builds users actually run, and cover specific entry points rather than whole systems https://github.com/theorem-labs/oss-verify/blob/main/docs/what-gets-proven.md https://github.com/theorem-labs/oss-verify-proofs/blob/main/docs/trust.md Anthropic Says Claude Proved Security Properties Across .... Similarly, the proof of the Linux kernel's zlib binary covers just one component, not a whole kernel LLMs are making formal software verification feasible at a ... LLMs are making formal software verification feasible at a ....

The Likeliest Path to Resolution The most probable first qualifier will not be a massive project like Linux, GCC, or LLVM. Instead, a compact TLS library or database engine, such as OpenSSL/BoringSSL, rustls, or SQLite, is the prime candidate. Crucially, the criteria allow for proofs of memory safety and absence of undefined behavior for C/C++ code. This represents a vastly more tractable goal than establishing full functional correctness, making a whole-library memory-safety proof on x86-64 the most direct path to a qualifying public release.

Drivers for an Early Timeline Extremely rapid general AI capability gains—such as recent subexponential 3-SAT refutations and Tier 4 FrontierMath mastery—make a 2027 resolution plausible. There are also heavily resourced, targeted efforts: Theorem’s roadmap projects verifying 95% of nixpkgs machine code at the binary level on x86-64 by the end of 2027, conditional on continued scaling https://theorem.dev/blog/verified-software-stack/ https://theorem.dev/blog/verified-software-stack/ https://theorem.dev/blog/verified-software-stack/. They report proof efficiency doubling roughly every two months https://theorem.dev/blog/verified-software-stack/. Because Theorem’s bottom-up approach requires verifying shared libraries like glibc and OpenSSL first, their trajectory maps directly onto the memory-safety route for C code. These drivers support a 10% chance of a qualifying result by April 1, 2027, and a 25% chance by September 15, 2027, but theoretical breakthroughs alone do not establish that robust, end-to-end verification of deployed systems will follow immediately.

Bottlenecks and the "Complexity Wall" Despite raw generation speed, reaching the median on March 15, 2028, requires overcoming a "complexity wall." Current proofs are verbose and low-level, and scaling up to codebases of 100k+ lines requires modular abstractions that agents do not yet build well https://www-cdn.anthropic.com/files/4zrzovbb/website/6867eadf760258fa8b42a504600cd3c036d16358.pdf LLMs are making formal software verification feasible at a .... The recent AI-assisted xv6 verification highlights this gap: while agents generated a million lines of Rocq, humans still had to supply critical abstractions and specification designs Extending concurrent separation logic to the hardware ... Extending concurrent separation logic to the hardware level .... Set against related questions, the friction of integrating theoretical AI breakthroughs into robust, end-to-end applications for deployed systems warrants a modest lag between frontier capability gains and a qualifying public release. That integration burden makes March 2028 a more credible midpoint than treating rapid proof-generation gains as sufficient for a 2027 median.

Tail Risks and Obstacles A meaningful right tail extending into 2029 and beyond accounts for the difficult leap from simplified academic setups to exact production builds. Current frameworks struggle with dynamic linking and the multithreading inherent in production builds of OpenSSL and SQLite Anthropic Says Claude Proved Security Properties Across .... Furthermore, a qualifying proof requires independent expert approval of the specification and must definitively credit the AI with the central verification ideas. If agents struggle to master concurrency, optimized assembly, and specification design, resolving these architectural and attribution hurdles could push the qualifying date into the 2030s. I therefore put the probability of a qualifying result by April 15, 2029, at 75%, and by November 15, 2030, at 90%, leaving a substantial tail for persistent integration and approval obstacles.