使用LLM进行规约和证明驱动的程序开发

程序验证方法虽然能够为软件提供逻辑上的正确性保证，但是一直被认为是一种高成本的开发方式。主要原因有如下几个方面：

• 学习成本高。程序验证需要程序开发人员具有程序验证的知识。但是对于一个已经从事多年的开发人员，让其学习与当前工作看似毫无关系的数理逻辑，或者新的程序证明语言（例如Rocq），这无异于是对程序开发人员的苛求
• 维护成本高。现实的程序开发场景时刻面临着各种需求的改变。对于大多数公司的开发流程，需求的意味着改变原有的实现代码。新需求实现之后，再移交测试进行正确性验证。但是如果一个项目是证明驱动的，改变原有的代码之后意味着之前的证明全部都要重新进行，这是巨大的工程开销。
• 用于验证而编写的代码量远多于功能实现的代码量。参考Sel4，其用于证明的代码量是功能实现代码量的十倍以上。为了安全性而付出数十倍的代价，在多数场景下是低“性价比”的。

虽然程序验证方法在实际的落地中存在各种困难，但是从今年年初，随着Claude Opus 4.6推出，以及Claude Code，Cursor等LLM agent在功能上的反复迭代，这种落地中的困难可能在当下存在了一种解决的可能性。我实验了Cursor + Opus 4.6/Opus 4.7/GPT-5.5上在Rocq证明中的效果，结果都十分惊艳。在过去这证明无异于需要一个具有Rocq经验的人，工作几天完成。但是现在借助于LLM，只需要几个小时。从这点来看，貌似程序验证中维护成本高和证明工作量两个问题可以得到较好的解决。

对于学习成本，这是一个难以评估的点。当前LLM确实降低了当前编程的门槛，借助于LLM，即使一个完全没有接触过编程的人也能够获得一段可执行的，可完成当前任务的程序。但是随着功能的迭代，任务的复杂度上升，对安全/运行效率等存在了更多的需求之后，项目仍然需要具备相关专业知识的开发人员来开发和维护。越是规模庞大，复杂的项目，越是需要经验丰富的专业人员来进行管理与维护。但是不可否认的是，LLM确实提高了开发效率，降低了开发人员对于知识理解的门槛。对于程序验证而言，因为LLM能够解决一部分程序逻辑上理解困难的问题，开发人员并不需要成为一个形式化验证领域的专家，会一些基础的逻辑基础以及形式化验证的语言即可上手写出经过验证的代码。

基于此，我们尝试验证了使用大模型进行规约和证明驱动的程序开发（Specification- and Proof-Driven Development with LLM， SPDDwL）的可能性。其思路是，输入自然语言的需求，LLM将项目中不涉及side effects的部分全部使用Rocq进行编写，然后直接在Rocq中证明这部分代码需要满足的逻辑性质，最后再将所有通过证明的代码导出为项目中需要的编程语言实现，例如C++等。详细流程可以见我们的论文： https://arxiv.org/pdf/2605.26017 。通过初步实验，在30分钟内，我们自动生成了约1700行左右的Rocq功能实现与性质证明，同时导出了2k+行C++代码。导出的代码通过了样例测试以及12小时的模糊测试。

当前的结果给我们提供了一种程序开发的可能，通过编写Rocq等交互式定理证明语言，然后导出到对应的项目语言上，从而完成开发工作。这种规约和证明驱动的开发流程，极大程度保障了代码的安全性与可靠性。借助于LLM，也大大降低了代码与证明编写的成本。同时这种流程带来了另一种优势：虽然LLM存在幻觉，可能生成看似正确但是错误的代码。但是LLM即使生成了错误的Rocq实现，但是在证明时，错误的实现是无法通过逻辑证明的，所以幻觉并不会传导到导出代码中，从而避免了模型的幻觉。

从当前结果来看，程序验证方法存在了一种可能被更多人使用的，可以在项目中落地的方式。目前此工作仍然处在雏形之中，针对真实场景的各种需求，如何让真实需求与形式化结合，如何让LLM更好地与Rocq等交互式定理证明器结合等诸多问题，仍然是需要解决的难点。

— May 29, 2026