WEBVTT

1
00:00:01.300 --> 00:00:10.440
This is Anthropic, Read Aloud. Today: L L Ms are making formal software verification feasible at a much larger scale.

2
00:00:11.740 --> 00:00:17.282
L L Ms are making formal software verification feasible at a much larger scale.

3
00:00:17.732 --> 00:00:28.924
Claude formally proved security properties in the compiled code of 123 open-source libraries. Along the way, it found bugs that had eluded detection for years.

4
00:00:29.374 --> 00:00:50.359
From Anthropic Research, published October 22, 2026. By Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich Nicholas Carlini, Rajashree Agrawal, and Jason Gross.

5
00:00:51.359 --> 00:01:13.823
Most software is riddled with bugs, which A I 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. Formal software verification could provide this guarantee, but it has historically required years of expert effort, making it impractical for most real-world projects.

6
00:01:13.943 --> 00:01:36.642
In a collaboration with Theorem, however, we show this is no longer the case: L L Ms can now produce formal proofs at large scale, enabling new software development workflows that include proven security guarantees. Using Claude, we proved security properties at the assembly code level (RISC-V) in over 100 real-world open-source software libraries.

7
00:01:36.762 --> 00:01:53.935
To our knowledge, this represents the first large-scale effort to use A I to apply formal verification to production software at the assembly code level. While writing the proofs, Claude also discovered bugs that had eluded detection for years, despite trillions of test runs.

8
00:01:54.055 --> 00:02:02.147
As model capabilities continue to improve, we expect formal verification to become an essential part of secure software development.

9
00:02:02.947 --> 00:02:03.791
Introduction.

10
00:02:04.241 --> 00:02:22.650
Even mature, heavily tested software contains bugs, and L L Ms are increasingly adept at finding them. The Linux kernel, one of the most well-tested pieces of software today, deployed on billions of devices worldwide, recently had over 1000 vulnerabilities disclosed.

11
00:02:22.770 --> 00:02:34.220
With frontier models becoming more capable of chaining seemingly benign bugs into critical exploits, we need techniques that can detect and fix these bugs before they can be exploited in the wild.

12
00:02:34.670 --> 00:02:54.574
Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found. Formal verification is one way to do this. In formal verification, developers translate their code into a mathematical model, then try to prove that it always follows some defined set of security rules.

13
00:02:54.694 --> 00:03:13.148
If they fail to prove this, that means there could be a bug in the code that would violate a rule, and the nature of the failure implies what the bug might be. Repeating this process (after eliminating the cause of failure each time) will ultimately yield proof that the code is devoid of any bug that would violate those rules.

14
00:03:13.598 --> 00:03:33.267
However, formal verification isn’t easy. Proofs can be many times larger than the original code, and writing them requires significant effort and a niche, highly specialized skill set. For instance, it took two person-years to implement the seL4 operating system kernel, but 20 person-years to formally verify it.

15
00:03:33.387 --> 00:03:41.524
Accordingly, formal verification has been practical only in truly mission-critical applications, such as Airbus’s avionics code.

16
00:03:41.974 --> 00:04:03.988
But L L Ms are making it far easier. Frontier models can now produce correctness proofs for real-world software fully autonomously. To demonstrate this, we asked Claude to prove useful security properties across 123 open-source libraries, including showing that some of their executable artifacts can never crash under certain conditions.

17
00:04:04.108 --> 00:04:20.410
Specifically, Claude proved that these programs will always exit normally without triggering memory-safety errors or failing assertions, for every input less than 64 megabytes and every modeled Linux operating system (OS) response and memory layout,

18
00:04:20.530 --> 00:04:31.196
under certain assumptions (namely that the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V 1 C P U using Linux OS).

19
00:04:31.316 --> 00:04:39.392
This is still far away from fixing all possible bugs, but it does get us much closer than before and provides a roadmap toward that end.

20
00:04:39.842 --> 00:05:00.592
We’re publishing a subset of these proofs so that anyone can verify and reuse them, along with the RISC-V and OS semantics. Theorem, our collaborator on this project, is also offering to run the same pipeline for other open-source projects, and is publishing a Claude skill to help developers get started with verifying their own code.

21
00:05:01.042 --> 00:05:04.967
Formal verification is a broad field with many methodologies.

22
00:05:05.087 --> 00:05:26.770
Below, we also describe our initial explorations using other formal verification methods to accelerate other security or software development tasks, such as assessing the security of the zlib compression algorithm, proving behavioral equivalence of a Python interpreter written in Rust, and rooting out long-standing bugs in critical software.

23
00:05:27.220 --> 00:05:47.485
The road ahead for formal verification is promising. The cost of writing proofs is falling as models become more intelligent. Moreover, as more code is formalized and methods of achieving security guarantees become more standardized, the ability to reuse or modify proofs across codebases will amortize the cost.

24
00:05:47.605 --> 00:05:57.979
We encourage all developers to explore formal verification with L L Ms, especially those who previously tried it with less capable models and found it didn’t work.

25
00:05:58.429 --> 00:06:03.530
In the rest of this post, we cover our formal verification experiments in more detail.

26
00:06:04.330 --> 00:06:05.746
Turning tests into proofs.

27
00:06:06.196 --> 00:06:29.875
To prove that a piece of software is correct, we must first state what “correct” even means. Correctness is defined by the specification (spec). In some programs, there is a clear way to formally specify the program’s intended behavior. For example, a PNG decoder takes a sequence of bytes and (following RFC 2083 ) decodes these bytes into the corresponding image.

28
00:06:29.995 --> 00:06:46.148
But for most programs, things aren’t so straightforward. What would it mean for a text editor or a web browser to be “correct”? The difficulty of obtaining a comprehensive and unambiguous spec is a significant obstacle to verifying software at a larger scale.

29
00:06:46.598 --> 00:07:06.326
To address this for the code in the open-source libraries that we sought to prove, we take the approach of automatically converting their preexisting compilable test suites into a spec by encoding the rule “this test suite always passes,” using a general model of what it means to execute any RISC-V-compiled binary on Linux.

30
00:07:06.446 --> 00:07:25.610
Historically, proving such specs was intractable, given the inherent complexity of writing a proof that can encompass and make an argument over all possible behaviors and interactions of tens of thousands of assembly instructions over any input (and the fact that proofs tend to be extremely large as a result).

31
00:07:25.730 --> 00:07:36.731
This is where today’s L L Ms come in: churning through millions of lines of code in pursuit of a well-defined goal is a task that L L Ms are extremely well suited for.

32
00:07:37.181 --> 00:07:59.517
For this project, we started with fuzz tests. In these tests, developers write an entry point 2 into their code that takes inputs, such that any input that causes a crash is a bug the authors care about. Then the fuzzer, a testing engine, generates enormous numbers of semirandom and mutated inputs at the entry point to try to find a bug (visualized in Figure 1).

33
00:07:59.637 --> 00:08:12.296
The longer a fuzzer runs, the more bugs it can find. But this is inherently a brute-force process, with no guarantee of exercising every possible code path, regardless of how many inputs you try.

34
00:08:12.746 --> 00:08:23.805
Fuzzing works by running huge numbers of generated inputs through one entry point to find the inputs that cause a crash. There are infinite inputs, so the search can never be complete.

35
00:08:24.255 --> 00:08:46.750
To find all the bugs that would’ve been surfaced by a fuzz test, we turned the fuzz test into a spec defined over the compiled RISC-V instructions. The spec says that the fuzz test won’t crash for any input less than 64 megabytes. 3 If Claude can prove this spec, the fuzz test on RISC-V becomes superfluous: fuzzing that entry point will never find any bugs.

36
00:08:47.200 --> 00:09:06.218
We did this for hundreds of projects in Google’s O S S-Fuzz initiative, which provides continuous fuzz testing for qualifying open-source projects. O S S-Fuzz contains thousands of developer-authored entry points that look for broken code properties by crashing (for example, on a failed assertion).

37
00:09:06.338 --> 00:09:26.004
O S S-Fuzz automatically instruments C and C++ programs with AddressSanitizer 4 (ASan), causing them to crash whenever memory is accessed improperly (which is a leading cause of software vulnerabilities ). Broad-spectrum specifications like memory safety apply to almost all software.

38
00:09:26.454 --> 00:09:47.594
The open-source library and its existing fuzz test are compiled to a RISC-V executable. This executable, along with Theorem’s RISC-V and OS formal semantics and the desired no-crash property, mechanically yield a specification the proof must satisfy. Claude writes the proof; the Rocq kernel checks it against the specification.

39
00:09:47.714 --> 00:09:52.237
Green marks what’s proven, conditional on the trusted components being correct.

40
00:09:52.687 --> 00:10:08.260
Over the span of a few weeks, Claude successfully patched the bugs it found and then proved that there are no crashes on any input (up to 64 megabytes) for 239 entry points across 123 different O S S-Fuzz libraries.

41
00:10:08.380 --> 00:10:28.623
These proofs operate on the compiled RISC-V instructions (that is, executable binaries), and they comprise about 180 million lines of Rocq, with a typical proof running to about 600000 lines to provide security guarantees on binaries with a median length of 18000 RISC-V instructions.

42
00:10:28.743 --> 00:10:49.022
These proofs are built by translating the RISC-V assembly code to a mathematical model using Theorem’s RISC-V instruction and Linux process semantics. This means these proofs currently assume that the program runs as a single-threaded static binary with a fixed memory budget on a RISC-V C P U using Linux OS.

43
00:10:49.142 --> 00:11:02.372
Expanding the scope of these proofs is well within reach, as it would involve standardizing semantics for more assembly architectures and other operating system processes. See an expert’s take on the proofs Claude wrote.

44
00:11:02.822 --> 00:11:16.007
A formal no-crash proof over all inputs rules out all crashes along any path reachable from the entry point. While iterating on its proof, Claude can also find and fix any remaining reachable crash-producing bug.

45
00:11:16.457 --> 00:11:31.670
While this is an enormous volume of proof code, virtually none of it needs to be manually reviewed. The Rocq proof checker ensures that the spec is correctly satisfied by the proof. As a result, the only artifacts that a developer needs to trust are:

46
00:11:32.120 --> 00:11:35.402
The formal models of RISC-V and of Linux processes.

47
00:11:35.642 --> 00:11:37.915
The exact theorem statements that were proved.

48
00:11:38.155 --> 00:11:40.515
The Rocq proof checker itself. 5.

49
00:11:40.965 --> 00:11:52.762
This doesn’t mean these libraries contain no bugs. Instead, it means that any remaining bugs either are to be found within the artifacts listed above or are outside the scope of Claude’s proof.

50
00:11:52.882 --> 00:12:13.917
Hardening those still-possibly-buggy trusted components (Rocq, RISC-V, and Linux semantics) is not insignificant, but it’s a far more tractable task than debugging every line of code the scaled-out proofs cover, especially as this approach can secure an arbitrary number of projects without increasing the size of the trusted components.

51
00:12:14.367 --> 00:12:35.017
We welcome independent verification of our proofs and encourage refinement of our approach. To that end, we are publishing the trusted components (above) made for this project that are not already public; Claude’s complete Rocq proofs for fuzz tests that did not require patching; and specifications for other fuzz tests we were not able to prove.

52
00:12:35.817 --> 00:12:37.345
Finding and fixing bugs.

53
00:12:37.795 --> 00:12:55.885
Above, we showed that you can turn many open-source libraries’ developer-written tests (fuzz tests) into specs that Claude can prove will always pass, sometimes after patching the remaining bugs it found. For this reason, the process of attempting to prove these specs discovered hundreds of bugs.

54
00:12:56.335 --> 00:13:15.700
Lots of bugs showed up during Claude’s attempts to prove hundreds of entry points. To ensure that Claude didn’t have to stop for a human every time this happened, we let Claude fix the bugs it found: it patched the code, which caused the spec to be regenerated with that patched code, and then Claude proceeded to prove that new spec. 6

55
00:13:16.150 --> 00:13:29.206
Many of the bugs we found are ones that a fuzzer would be unlikely to ever find. Fuzzers mutate small inputs, typically capped at 1 megabytes, and typically rely on code coverage to guide them toward bugs.

56
00:13:29.326 --> 00:13:42.873
While proving an entry point in one library, Claude found a counter underflow in its copy of a decompressor that led to an out-of-bounds write, but only on inputs of around 20 megabytes that had one rare, specific layout.

57
00:13:42.993 --> 00:14:07.235
Other bugs include an out-of-bounds read in an image decoder that needed a 64 megabytes input and over 2 gigabytes of memory, an out-of-bounds read in another library that needed a particular sequence of calls across two handles to the same file, and a rediscovery of CVE-2026 to 56132 in libexpat, which needed deeply nested input.

58
00:14:07.355 --> 00:14:20.894
Claude also found logic bugs that never crash at all. While proving that one library was memory-safe, for example, it noticed that a feature for restricting which files an application can load isn’t always enforced.

59
00:14:21.344 --> 00:14:41.078
The ultimate goal of this project was to achieve a proof that the RISC-V-compiled fuzz tests had no remaining crashes to find. However, bugs like the above show that the process has another benefit, regardless of whether that goal is achieved: even just attempting this process yields real bugs that need to be fixed.

60
00:14:41.878 --> 00:14:43.547
Proving more than memory safety.

61
00:14:43.997 --> 00:15:05.959
Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations.

62
00:15:06.079 --> 00:15:24.185
For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes, so proving the test never crashes is equivalent to proving the property itself.

63
00:15:24.635 --> 00:15:43.708
This can also occur even when the properties are not directly specified by the developer. For example, in order for Claude to complete its O S S-Fuzz proof for cpp-httplib, it was necessary to rule out the possibility of a stack overflow due to too much recursion in the std::set destructor.

64
00:15:43.828 --> 00:15:59.262
This recursion depth is bounded by the maximum depth of a tree, so Claude had to prove (on machine code!) that libc++’s red-black tree rebalancing algorithm is correctly optimized to keep the tree’s depth logarithmically bounded.

65
00:16:00.062 --> 00:16:02.288
Other formal verification case studies.

66
00:16:02.738 --> 00:16:16.634
Formal verification is an expansive domain. The fuzz-test-to-proof example above is one instance of L L Ms making formal verification more widely usable by directly applying proofs to machine code.

67
00:16:17.084 --> 00:16:39.072
We’ve also seen success using L L Ms with formal verification in other ways. For example, we asked Claude to write a formal spec of RFC 1950, the technical document that defines the zlib compression file format. Then, we had Claude prove that the zlib implementation in the Linux kernel correctly implements that spec.

68
00:16:39.192 --> 00:17:00.056
As with the examples above, Claude proved this property at the binary level, except instead of RISC-V, Claude directly proved the x86-compiled binary using Claude-generated (and heavily tested) formal semantics of the x86 ISA. 7 We then repeated this process for half a dozen other widely used libraries.

69
00:17:00.176 --> 00:17:21.957
Along the way, we found some minor (unexploitable) bugs in corner cases, which are in the process of being filed upstream. We draw two conclusions from this exercise: (1) these extremely well-tested codebases are already almost fully correct, and (2) it is possible to prove end-to-end correctness properties about real existing codebases.

70
00:17:22.407 --> 00:17:37.536
In another experiment, we asked Claude to develop an interpreter for a large subset of Python in Rust, and to prove (using Verus, a verification tool for Rust) that it adheres to the CPython semantics outlined in an academic paper.

71
00:17:37.656 --> 00:17:56.506
We then measured the adherence to CPython’s behavior empirically, running over 1.7 million randomly generated Python programs, finding identical behavior with CPython in 99.95 percent of tests, with remaining test differences as unsurprising known corner cases.

72
00:17:56.956 --> 00:18:20.182
We also found issues in several widely used and critical applications via formal verification attempts of simple security properties. In one of them, we discovered a previously unknown logic bug that had been latent for more than a decade. During an effort to verify a widely used P D F reader, we found as many security bugs in one week as are typically reported in a year.

73
00:18:20.632 --> 00:18:23.890
See the Appendix for more details on some of these efforts.

74
00:18:24.690 --> 00:18:26.150
This is just the beginning.

75
00:18:26.600 --> 00:18:47.058
One of the key limitations of L L M-assisted formal verification is that the proofs can take hundreds of millions of tokens to produce. Cost-efficiency is critical if our goal is to make these methods available to the entire software ecosystem. Fortunately, there are compelling reasons to expect efficiency to improve.

76
00:18:47.858 --> 00:18:49.835
Newer models need fewer tokens.

77
00:18:50.285 --> 00:19:07.555
We built 36 small verification tasks from real O S S-Fuzz code. Opus 5.5 proves half of them with about 40 percent fewer tokens than Opus 5. We expect this trend to continue as models are trained on long verification tasks.

78
00:19:08.005 --> 00:19:28.378
Figure 1: Opus 5.5 finishes proofs faster than earlier models. Share of 36 formal verification tasks proved by a single agent at a given token budget. Each task received three independent single-agent attempts at a 5 million-token budget, and counts as proven when the first attempt finishes.

79
00:19:28.498 --> 00:19:44.199
Image description: Line chart of the share of 36 verification tasks completed by token budget per agent for Opus 5.5, Fable 5.1, and Opus 5. Opus 5.5 finishes proofs with the fewest tokens.

80
00:19:44.999 --> 00:19:46.239
Proofs can be reused.

81
00:19:46.689 --> 00:20:05.497
When agents work separately, they often end up duplicating a lot of effort. Proofs, like software, are recursively built from smaller proofs, and the smaller the proofs are, the more reusable they tend to be. To measure the impact of this, we let agents copy each other’s proofs as they worked on proving their own targets.

82
00:20:05.617 --> 00:20:17.543
When given access to this shared workspace, agents needed 17 percent fewer tokens than when they worked alone, and some agents even succeeded after previously failing in a solo attempt.

83
00:20:17.993 --> 00:20:41.382
Figure 2: The 36 proofs from one shared workspace, in the order they finished. An arc joins any two proofs that share an unchanged file; bars show the tokens spent writing each proof, and black lines show the same task’s average cost for an agent working alone, which was higher in 30 of the 34 completed proofs (agents working alone were not able to complete two of the proofs).

84
00:20:41.502 --> 00:20:53.140
Image description: Chart of 36 proofs in finishing order, with arcs joining proofs that share a file and bars showing the tokens spent on each proof compared with an agent working alone.

85
00:20:53.590 --> 00:21:12.235
We observed the same phenomenon occurring at scale during our O S S-Fuzz proof effort. Most of a proof concerns code that every program contains (particularly initialization of the C runtime and AddressSanitizer), so very different programs can end up with significantly overlapping proofs.

86
00:21:12.355 --> 00:21:19.925
Agent teams took advantage of this by copying another team’s finished proof and then adapting it to their own program (Figure 6).

87
00:21:20.375 --> 00:21:42.460
Figure 3: Agents copied an existing proof and adapted it to each new program. Each column represents one program’s complete proof by share of bytes. Blocks are the parts of the proof and each block shows how much was kept identical, lightly edited (same file, size within 2 percent), edited more, or newly written. The shared parts gained almost no new code.

88
00:21:42.580 --> 00:21:52.191
Image description: Block chart of the proofs for libcups, freerdp, and libzmq, showing how much of each part was identical, lightly edited, edited more or new.

89
00:21:52.641 --> 00:22:07.565
This reusability of proofs is how Mathlib, a shared library of formal mathematics in Lean, grew to nearly 300000 theorems submitted by over 700 contributors: each new proof builds on the existing body of work.

90
00:22:07.685 --> 00:22:20.777
We accumulated a similar body of proofs in the course of our O S S-Fuzz effort, some of which we’re including in our release (we are not releasing proofs that may reveal an unpatched bug in the open-source software).

91
00:22:21.227 --> 00:22:41.920
As we graduate from these initial experiments, we need a strategy for verifying the enormous body of existing software, starting with the most critical dependencies. As we’ve shown, this can be achieved at scale by using generic specs and working at the binary level, sidestepping the need to rewrite entire codebases in another language.

92
00:22:42.370 --> 00:23:00.343
This approach also facilitates the reuse of proofs at package-level granularity, which means that each dependency only needs to be verified once. Dependencies follow a power law: proving even a small set of shared libraries makes a huge swath of software feasible to prove.

93
00:23:00.463 --> 00:23:11.810
For more details, see Theorem’s roadmap for verifying the entirety of the Nix ecosystem, which includes critical infrastructure like glibc, OpenSSL, and cURL.

94
00:23:12.610 --> 00:23:13.598
Limitations.

95
00:23:14.048 --> 00:23:20.272
In practice, formal verification can sometimes prove less about the security of the code than we would like.

96
00:23:20.722 --> 00:23:38.329
“Formally verified” does not mean “bug-free.” Claude can write a proof showing that a compiled program’s behavior satisfies the requirements of a formal spec (which is verified by an external proof checker). However, a proof checker can’t tell you whether your spec matches reality.

97
00:23:38.449 --> 00:23:57.328
To match reality, the spec must correctly encompass and model everything about the real-world machine that the verified program runs on, including the C P U and operating system. When bugs show up in verified code, it’s because the spec, or the assumed semantics of the machine, differs from reality.

98
00:23:57.448 --> 00:24:12.119
Fortunately, this also means we know where to look for remaining bugs, and how to design a system where those still-possibly-buggy gaps are minimized. Below are the ways this applies to our proofs, and ideas for future work that would close those gaps.

99
00:24:12.569 --> 00:24:33.789
The real machine does something the model doesn’t describe. Our proofs are about single-threaded, static RISC-V binaries linked against musl libc. However, most people run these libraries on x86 or ARM and dynamically link them against glibc. To close this gap, we’d need system models that more closely resemble deployed systems.

100
00:24:33.909 --> 00:24:39.130
For example, a step toward this would be generating accurate semantics for x86.

101
00:24:39.580 --> 00:24:59.689
The claim may not cover everything we care about. We proved that a crash never triggers for any input under 64 megabytes on many fuzzing entry points in Google O S S-Fuzz, including ASan crashes. However, ASan doesn’t detect all memory safety bugs, and we didn’t verify all the entry points for each library.

102
00:24:59.809 --> 00:25:20.687
Even if we had, the whole library wouldn’t be covered by verifying all entry points (especially if there is dead code). Additionally, real programs might misuse the library, leading to memory corruption in the caller. To close that gap, we’d need to specify what callers must do for each public function, and callers would have to strictly adhere to it.

103
00:25:21.137 --> 00:25:35.911
We expect that as we learn more about leveraging L L Ms for formal methods, and as models continue to improve, these limitations will become tractable, and we’ll be able to verify a much larger percentage of the code we rely upon.

104
00:25:36.711 --> 00:25:37.524
Conclusion.

105
00:25:37.974 --> 00:25:52.758
The trajectory is clear: formal verification, which was historically practical only for bespoke expert-crafted guarantees in the most safety-critical code, will soon be as practical as fuzzing is today for almost all production software.

106
00:25:52.878 --> 00:26:07.726
Just like static types, testing frameworks, and other correctness tooling, verification will mature from “bolted-on” to “built-in,” driven not only by L L Ms but also by innovations in language design and development workflows.

107
00:26:08.176 --> 00:26:28.975
In today’s world, where L L Ms automatically scan for and find increasingly more code vulnerabilities, we must use processes that can guarantee code security properties. L L M-scaled formal verification is a promising approach toward securing these guarantees at a scope and scale that were previously unattainable.

108
00:26:29.095 --> 00:26:41.287
We encourage others to experiment so we can collectively build a world in which robust software has proliferated very widely and software bugs are a well-understood and quickly addressable rarity.

109
00:26:41.737 --> 00:26:43.065
Read the full appendix.

110
00:26:44.065 --> 00:27:04.269
That was L L Ms are making formal software verification feasible at a much larger scale, from Anthropic Research, published October 22, 2026. Read the original at anthropic dot com. This unofficial audio edition was generated automatically for the podcast Anthropic, Read Aloud.