「氛围验证」引警示：AI 形式化证明近六成证错目标

本月一篇形式化验证研究显示，让 AI 同时编写形式化规格与证明时验证器可全部通过且无误报，但人类阅读规格后发现近 60% 的用例证明了并非作者本意的性质。博主据此提出「氛围验证」一词，警示 AI 写规格加 AI 写证明再加验证器放行的流程看似可靠，实则可能系统性偏离原意。