即使是成熟且经过大量测试的软件也存在缺陷，而大型语言模型（LLM）在发现这些漏洞方面也越来越熟练。Linux内核——目前测试最充分的软件之一，部署在全球数十亿台设备上——最近披露了超过1000个漏洞。随着前沿模型越来越能将看似无害的漏洞串联到关键漏洞利用中，我们需要能够在这些漏洞被实际利用之前检测并修复它们的技术。 理想情况下，这些技术能够发现并修补所有漏洞，并提供证据证明已经没有更多漏洞存在。形式验证是一种实现这一点的方法。在形式验证中，开发者将代码转换为数学模型，然后尝试证明它始终遵循一套定义的安…