Rocq1 篇实战文章

这周本来没什么动静，直到一篇 arXiv 预印本把我拽住了。8 月 13 日挂出来的，讲 LLM 写形式化规格到底行不行。 规格是什么级别的概念，不展开。写代码的人都知道，代码能跑和代码是对的，是两回事。形式化验证管的是后一件事。验证的前提，是你先把“什么算对”写成机器能检查的精确描述。那个东西就叫规格。