Anthropic teamed up with Theorem Labs to harness the power of the Claude model for a thorough examination of low-level RISC-V assembly instructions. They carried out formal verification across a multitude of production-grade open-source code repositories. In a matter of weeks, they accomplished the verification of 239 test entry points spread across 123 open-source code repositories, resulting in the generation of a staggering 180 million lines of validated Rocq mathematical proof code.

During this meticulous process, they unearthed concealed vulnerabilities that had slipped past fuzz testing, as well as high-risk logical issues that had been lurking undetected for years. Their efforts even shed light on hardware defects in x86 processors and inaccuracies in official documentation.

By converting test entry points into mathematical propositions, this innovative approach achieved a comprehensive proof that covered all paths and inputs. Whenever the proofing process hit a snag, vulnerabilities were precisely identified, followed by automatic patching and subsequent verification, leading to a significant reduction in the miss rate.

Previously, formal verification projects that spanned from low-level to machine code were monumental tasks. However, with the advent of large models, verification efficiency has skyrocketed, with speeds roughly doubling every two months. Moreover, the proof content can be repurposed across different projects.

It is projected that with an investment of around $134 million, the verification of 95% of the machine code within the Nix ecosystem could be finalized by the close of 2027. At present, the first batch of related proofs has been made available to the public, presenting fresh solutions for the cybersecurity landscape.