技术路线的巧思
AI 写代码的根本焦虑是「看起来对」和「真的对」之间的鸿沟，人类审查填不满这个坑。Leanstral 的路线是借形式化方法的死板：关键逻辑用 Lean 这类证明助手描述规格，AI 生成的实现必须连同证明一起通过机器检查，错一步都过不了关。AI 恰好补上了形式化方法几十年的短板（写证明太费人力），形式化又恰好补上 AI 的短板（产出不可信），两个互相嫌弃的领域意外咬合。
落地的现实半径
先泼冷水：形式化验证的适用半径有限，规格本身写错了证明也救不了，UI 和业务逻辑这类「对错靠人定义」的领域基本无缘。但在它的主场，密码学实现、协议栈、金融核心、安全关键系统，这套组合的价值是实打实的，那些领域本来就在用形式化方法，只是贵到只有少数组织用得起，AI 把价格打下来就是把市场打开。「AI 生成、机器验证」可能是高保证软件的下一个标准姿势，Leanstral 是这条路上值得记名字的早期探索。
via: Hacker News