形式化验证是一种使用数学方法证明代码正确性的技术，尽管历史悠久，但一直局限于研究领域，因为编写证明极其困难和耗时。作者Martin Kleppmann预测，基于大语言模型（LLM）的AI助手将彻底改变这一现状。AI现在能帮助自动化编写证明脚本，使形式化验证变得便宜和高效。这将使验证更可行，同时AI生成的代码也需要形式化验证来确保正确性，替代人工审查。未来，开发者只需指定所需属性，AI即可生成代码和证明，类似编译器的工作方式。这一转变将使形式化验证成为软件开发的主流实践，尽管挑战将转向正确定义规范。AI的精确性还能弥补大语言模型的不确定性，提升整体可靠性。这一变革预示着软件工程的新时代，文化适应将是关键。
