即使是成熟且经过大量测试的软件也存在缺陷，而大型语言模型（LLM）在发现这些漏洞方面也越来越熟练。Linux内核——目前测试最充分的软件之一，部署在全球数十亿台设备上——最近披露了超过1000个漏洞。随着前沿模型越来越能将看似无害的漏洞串联到关键漏洞利用中，我们需要能够在这些漏洞被实际利用之前检测并修复它们的技术。 
理想情况下，这些技术能够发现并修补所有漏洞，并提供证据证明已经没有更多漏洞存在。形式验证是一种实现这一点的方法。在形式验证中，开发者将代码转换为数学模型，然后尝试证明它始终遵循一套定义的安全规则。如果他们无法证明这一点，意味着代码中可能存在会违反规则的漏洞，而故障的性质也暗示了该漏洞可能是什么。重复这个过程（每次都消除故障原因后），最终会得到代码没有任何会违反规则的错误的证据。 
然而，正式的核实并不容易。证明可能比原始代码大很多倍，写证明需要大量精力和高度专业化的技能。...