Anthropic, in collaboration with Theorem Labs, has pushed Claude to eradicate software vulnerabilities down to the machine code level. They have sent Claude to the deepest levels, verifying formal proofs for a large number of production-level open-source code repositories using RISC-V assembly instructions—in just a few weeks, they completed verification on 123 open-source code repositories and 239 test entries, producing 180 million lines of verified Rocq mathematical proof code.
What’s truly chilling is what it uncovered. Those hidden vulnerabilities that failed to be found after trillions of fuzzing attempts, high-risk logical gaps that lurked for over a decade, as well as hardware defects at the x86 processor level and errors in official documentation—all of these were brought to light by Claude in one go. Traditional random testing is like sifting sand repeatedly to find holes; there are always some that escape the sieve. The strength of this method lies in converting the testing entry directly into mathematical propositions, and providing a coverage proof for all paths and inputs—once the proof gets stuck somewhere and cannot proceed, that often becomes a hiding spot for vulnerabilities. Moreover, Claude can easily fix the patch and continue verification, significantly reducing the false positive rate.
From a cost perspective, the significance of this task becomes clearer. The formal verification of machine code from the lower level to the actual code format used to be a highly labor-intensive task. Now, thanks to the capabilities of large models, the verification efficiency is increasing at a rate of about doubling every two months. Moreover, the proofs generated can be reused across different projects. Based on current trends, with an investment of approximately $134 million, it is expected that by the end of 2027, 95% of the machine code in the Nix ecosystem will be verified; the first batch of related proofs has already been published. As the cybersecurity situation becomes increasingly urgent, this approach of “using AI to turn code correctness into a mathematical theorem” provides the industry with a completely new defense line.