Anthropic 的 Claude 一周内生成 1.8 亿行证明代码
anthropic 的 claude 为 123 个开源库生成 1.8 億行证明代码，发现数百个传统测试遗漏的错误。这可能使软件自动化更加可靠。
anthropic used its claude model to mathematically verify existing software code and generate formal proofs of its correctness, producing 180 million lines of proof code for 123 open-source libraries in just a few weeks. claude caught hundreds of bugs that conventional testing had missed, including a logical error that had gone undetected for over a decade. this approach could make software automation more reliable and trustable, and anthropic expects formal verification with ai to become as routine as standard testing. the process was done in collaboration with partner theorem and used claude to translate crash tests into mathematical problems, analyze compiled machine code, and produce extensive proofs.