📖 AI 总结

Anthropic与合作伙伴Theorem利用Claude对现有软件代码进行数学验证，并自动生成形式化正确性证明。在数周内，Claude为谷歌OSS-Fuzz项目中的123个开源库生成了约1.8亿行证明代码，过程中发现数百个常规测试未能捕捉的漏洞，包括某PDF阅读器一周内发现的安全漏洞数量相当于该软件通常一年的报告量，以及一个隐藏十余年的逻辑错误。该流程由Rocq程序自动校验证明，几乎无需人工审核，但工具与形式化基础仍由人类构建。Anthropic承认，“形式化验证”不等于“无错误”，证明仅在特定条件下成立。此举的意义在于，若AI能同时编写代码并证明其正确，软件自动化有望迈出关键一步，Anthropic希望AI形式化验证能像常规测试一样普及。