AI加速代码编写，但正确性验证成为瓶颈。文章介绍Go形式化验证工具Gobra及其底层Viper，通过前置条件、后置条件、循环不变量和权限模型，将程序性质转化为机器可检查的证明义务，并以求和算法演示。形式化验证不等于零缺陷，规范本身可能写错。AI Agent可生成候选规范、修复证明失败，但结论须由验证器给出，而非由另一个大模型判断。