Anthropic report: Claude generates 180 million lines of Rocq proofs, advancing formal verification to the assembly level

The screenshot is from the Anthropic official website.

AI is disrupting every aspect of the software industry, but in the security field, its performance has consistently been unsatisfactory. Especially when AI-generated code brings more hidden risks, and hackers are able to use AI to find and attack security vulnerabilities at large scale and low cost, the defending side is often exhausted and may even struggle to cope.

Since mid-October alone, major cybersecurity incidents have occurred frequently. First, the coding agent OpenCode was attacked and leaked users' third-party model keys. Then the PHP open-source programming language, used by nearly 70% of websites worldwide, was reported to have a major vulnerability, and many websites were shut down as a result. The latest Axios report also revealed that AI Agents are launching an "all-out attack" on the U.S. banking system, at a speed exceeding the response capacity of financial institutions and bringing major security risks. Mainstream institutions such as Morgan Stanley and Bank of America are handling it urgently.

On October 23, Anthropic and the Theorem Labs team released a report titled "LLMs are making formal software verification feasible at a much larger scale." Although the title appears somewhat specialized and academic, it was precisely when cybersecurity problems were becoming increasingly urgent that this report attracted widespread attention in the developer community.

From "finding vulnerabilities" to "proving security"

According to the report, Anthropic's Claude model generated about 180 million lines of Rocq proof code for 239 program entry points in 123 open-source software libraries, and in the process found and fixed hundreds of bugs. These included some vulnerabilities that had undergone trillions of tests but had still remained undiscovered over years of operation.

In addition to finding vulnerabilities faster and more accurately, the core breakthrough of this research lies in the fact that the research team advanced verification to the level of assembly instructions, carrying out proofs based on the RISC-V instruction set.

Some developers interpreted in discussions that the most important significance of the related research experiment is that, in the security field, AI was previously used more to "find bugs," but this only speeds up and improves the efficiency of the traditional software testing model. In essence, no matter how many times testing is performed, it is difficult to exhaust all possible cases, and it cannot avoid leaving vulnerabilities that give hackers an opportunity. Formal verification, by contrast, uses mathematical proof to confirm that a program satisfies specific security properties under given conditions.

In the past, this work relied heavily on professionals, was costly and time-consuming, and was difficult to apply on a large scale to ordinary software. But the research shows that, as the intelligence of large models continues to improve and Agents' ability to invoke and proactively execute tasks strengthens, this work has finally been able to scale.

Anthropic also pointed out that most software has vulnerabilities, and AI can now easily discover and exploit them. Today, mainstream cyber defense methods can no longer meet the requirements; what is more needed is a reliable method to prove that code has no vulnerabilities. The related research announced this time is the first large-scale use of AI to apply formal verification to production software at the assembly code level, finally turning what previously seemed an "impractical" requirement into reality.

Can the offense-defense situation be reversed?

Through continuously evolving AI capabilities and large-scale formal verification that can run in real-world settings, defenders in the cybersecurity field can discover defects that traditional testing finds difficult to reach. It is also conducive to moving security checks earlier into the development stage, discovering problems before code goes online, rather than waiting until vulnerabilities are exploited by attackers and then rushing to remedy them.

But for now, truly reversing the offense-defense situation is not so easy.

First, according to the report and related interpretations, formal verification does not mean it can prove that the entire software is "absolutely safe." It can only prove that a program satisfies preset properties under specific assumptions, constraints, and verification scope. If the specification itself has defects, or if vulnerabilities exist outside the verification scope, attackers may still find a breakthrough. For complex software systems, how to determine verification goals, handle third-party dependencies, and safely deploy fixes to production environments still requires a great deal of work.

A more realistic challenge is that the costs of using AI for attackers and defenders are not equal. An attacker only needs to find one exploitable vulnerability to possibly gain an intrusion opportunity; a defender must protect the entire system, not only discovering vulnerabilities but also assessing risks, verifying fixes, and avoiding introducing new problems during the repair process. Even if AI can greatly reduce the cost of vulnerability discovery and code verification, it does not mean defenders can immediately complete all this work.

In addition, some developers mentioned that formal verification may slow down development speed. With AI driving software development into a mode of continuous acceleration, whether it is possible to slow down for security may become a real dilemma. Some developers also worry that AI-generated proof strategies may "bypass the checkpoints" and produce lengthy proofs that are difficult for humans to review, ultimately escaping the scope of human monitoring and control and creating more serious problems.

Although the related research cannot immediately reverse the offense-defense situation, most discussions in the developer community still remain optimistic about the new progress, believing that change has already occurred and that a turning point may soon arrive.

Many developers posted that, as the related research becomes widespread in real-world scenarios, it may become an important part of shaping future software development models and changing the way the entire security system works. Pratham, a well-known AI and Web technology blogger, also said that this may be "one of the clearly underestimated achievements of AI so far," stating that as cybersecurity problems become more difficult, "we especially need more progress in this field." (This article was first published in TMTPost APP, written by Feixiang Tai Kong)