Claude Found the Bug 10 Million Tests Missed (in 36 Seconds)
Read the Portuguese translation →
Author: Hyperautomation Labs · Watch on YouTube
Video authored by the channel shown, not by IANIA; all rights belong to the creator. Transcript and summary generated automatically; the original-language content is preserved.
Original language: English
Original video: Claude Found the Bug 10 Million Tests Missed (in 36 Seconds) · Channel: Hyperautomation Labs · 07:17 · Watch on YouTube
Topics: AI agents, Cybersecurity and software security, Claude Code, Software engineering with AI
Summary
Section titled “Summary”The video explains how Claude used formal verification to prove that code meets specific safety promises, rather than relying on random testing that can miss rare bugs. In Anthropic and Theorem’s research, Claude generated proofs for open-source libraries and uncovered vulnerabilities that conventional tools had not found. The presenter demonstrates the approach with a small C function: a fuzzer found no crashes in 10 million tests, while CBMC produced a breaking input in about 36 seconds. The video also stresses that formal verification is not the same as proving software bug-free, since the results depend on assumptions about the hardware, model, and proof checker.
Key points
Section titled “Key points”- Random testing explores only some inputs, so it cannot establish that every possible input is safe.
- Formal proofs can verify a stated property, such as a program not crashing for inputs under 64 megabytes.
- Anthropic and Theorem reported that Claude proved properties for 239 entry points across 123 open-source libraries.
- A separate proof checker validates Claude’s generated proof line by line.
- The proof process uncovered bugs that testing tools missed, including bugs requiring large or unusual files.
- In the presenter’s demonstration, a fuzzer ran 10 million tests without a crash, but CBMC found a failing upload of about 63 megabytes in roughly 36 seconds.
- Formal verification has important limits: results depend on assumptions about the chip, execution setup, and the exact property being proved.
- The team addressed the risk of Claude making a proof pass by changing the program into one that does nothing, penalizing code changes and auditing them.
- The video suggests proofs could become a routine complement or alternative to testing, while emphasizing that some components still have to be trusted.
Chapters
Section titled “Chapters”| Start | Chapter | Summary |
|---|---|---|
| 00:00 | Testing versus proof | The video contrasts random testing with formal proof and introduces Anthropic and Theorem’s research into finding software bugs. |
| 01:03 | Why software proofs are difficult | The presenter explains the high historical cost of formal verification and how Claude applied proofs to existing open-source libraries. |
| 02:35 | Bugs missed by testing | Claude’s proof work exposed rare bugs, and the presenter tests a small program where CBMC finds a failure that millions of random tests missed. |
| 04:41 | Other results and limitations | The video describes Claude’s work on chip models and a Python interpreter, then discusses proof costs, assumptions, and safeguards against trivial code changes. |
| 06:15 | What proof-based software could mean | The presenter considers the prospect of software shipping with proofs and closes with a question for viewers and channel announcements. |
Quotes
Section titled “Quotes”It didn’t test it. It proved it. — 00:00
A proof is different. — 01:03
10 million random uploads, zero crashes. — 03:38
Formally verified does not mean bug-free. — 05:44
The chip and Linux model. The exact promise that was proved. And the proof checker itself. — 06:15
Concepts and entities
Section titled “Concepts and entities”Claude, Claude Code, Anthropic, Theorem, CBMC, SEL4, Linux kernel, libexpat, Opus 5.5, Prova formal, Fuzzing, Proof checker
Full transcript (original language)
Section titled “Full transcript (original language)”00:00 The apps on your phone run on code that’s been tested billions of times. It still has bugs nobody has found. Watch this. A testing machine is throwing random inputs at a program. One and a half billion tries. Four crashes found and the rest of the maze, nobody knows. Now watch what Claude did with the exact same maze. It didn’t test it. It proved it. Every path from that door checked and green. Anthropic published this research on
00:31 October 22nd together with a company called Theorem. And the first line is blunt. Most software is riddled with bugs which AI can now easily find and exploit. The Linux kernel runs on billions of devices and it recently had more than a thousand vulnerabilities disclosed. So finding bugs isn’t the hard part anymore. Proving there are none left is. Here’s the difference in plain words. Testing is like checking a building for gas leaks by walking into random rooms. Walk long enough and you’ll find some
01:03 leaks, but you can never say the building is safe. You only know about the rooms you walked into. A proof is different. It’s like having the plan of every single pipe and a guarantee that none of them leak. People have known how to do this for decades. Almost nobody does it because it is brutally expensive. How expensive? Here’s the famous example. An operating system kernel called SEL4. It took two person years to build it and
01:33 20 person years to prove it correct. 10 times more work to prove the code than to write it. That’s why proofs were only used where a bug could cost lives, like the software that flies Airbus planes. So Anthropic tried something new. They [snorts] took open source libraries, the building blocks hiding inside browsers, image viewers, and servers. And they took the tests the developers had already written. Each test became a promise. For every input under 64 megabytes, this program never
02:05 crashes. Claude’s job was to prove that promise. Over a few weeks, Claude proved it for 239 entry points across 123 libraries. That’s about 180 million lines of proof. A typical proof is around 600,000 lines. Nobody reads that. And here’s the clever part. You don’t have to. A separate program, called a proof checker, checks every single line. Here, it rejects
02:35 Claude’s proof because one case is still open. Claude fixes it. The checker accepts. Now that program, compiled for this kind of chip, is proven not to crash. Here’s the part I like most. To finish a proof, Claude has to deal with every bug in its way. So, it found bugs the testing machines had missed for years. One only happened on a file of about 20 megabytes with one rare layout. But testing tools usually stop at around 1 megabyte.
03:06 They’d never get there. Another needed a 64 megabyte image and 2 gigabytes of memory. It also rediscovered a known security hole in libexpat, a library used to read XML. And when the team tried this on a widely used PDF reader, they found as many security bugs in 1 week as usually get reported in a whole year. So, I tried a tiny version of this myself. I wrote a small C function that splits an upload into 1 megabyte blocks,
03:38 and I planted a bug in it. One that only shows up on big uploads, like the ones in the article. Then I ran a fuzzer capped at 1 megabyte, like the real ones. 10 million random uploads, zero crashes. By testing standards, this code looks perfect. So, I asked Claude code to stop testing and prove it instead with a free tool called CBMC. It took about 36 seconds. The proof failed and CBMC handed back the exact upload that breaks it, about 63
04:09 megabytes. Any upload over 16 megabytes writes past the end of a 16-slot array. My fuzzer never sent anything that big. So, it never stood a chance. Claude added one line and proved the fixed version. Verification successful. Every size from 0 to 64 megabytes with any contents, not a sample. All of them. It even flagged the trade-off. Big uploads now only get their first 16 blocks indexed. That’s the whole idea in 1 minute.
04:41 They didn’t stop at crashes. Claude wrote its own model of how Intel and AMD chips run instructions, good enough to boot Ubuntu. And while doing it, it found hundreds of mistakes in the official reference documentation. It also built a Python interpreter in Rust and proved it follows Python’s rules. On 1.7 million random programs, it matched real Python 99.95% of the time. So, what’s the catch?
05:11 Cost. Some of these proofs take hundreds of millions of tokens, but that’s dropping fast. On 36 test tasks, Claude Opus 5.5 proved half of them using about 40% fewer tokens than Opus 5. And when Claude agents were allowed to copy each other’s finished proofs, they used 17% fewer tokens. Proofs get reused the same way code does. Now, Anthropic is careful here and so should we be. Formally verified does not
05:44 mean bug-free. These proofs assume a RISC-V chip, one thread, and a particular setup. Most people run this code on Intel or ARM. There was also a cheating risk. Claude could make any proof pass just by rewriting the program into one that never does anything. So, the team penalized every code change Claude made and audited them. What you get isn’t perfection. It’s a much shorter list of things you have to trust. The chip and Linux model.
06:15 The exact promise that was proved. And the proof checker itself. So, what does this mean for you? Anthropic’s prediction is that proofs will soon be as normal as testing is today. Theorem is already offering to run this pipeline on other open source projects. And they published a Claude skill so developers can try it on their own code. If that happens, the software you use every day stops coming with a promise that it was tested and starts coming with a proof. So, here’s my question. Would you trust
06:46 code more if an AI proved it or less? Tell me in the comments. I read everyone. Real talk. 90% of you watching haven’t subscribed. On YouTube, hit join and become a member. Or just subscribe. It’s free and it tells the algorithm to send you more. On Facebook, subscribe is the supporter button. That’s what keeps the lights on here. Subscribe to support us. If you want a one-page summary with the
07:17 key numbers, the three things you still have to trust, and every link, comment maze, and I’ll send it to you. If you want the full playbooks, my paid guides are linked below. Follow along on Instagram and Facebook for bite-size AI. The deep dives live here on YouTube. See you in the next one.