「Lean 洗 slop」成圈内膜：形式化验证创业被讽为 VC 骗局

ludwigABAP · x · 2026-10-22

这是 X 上一段围绕 autoformalization（自动形式化）与「Lean slop」的圈内吐槽串。有开发者直言：借着形式化验证的噱头，可以轻松说服不懂「验证需要验证基准」的 VC 融到千万美元级别的钱，然后套现离场。楼主回应称自己确实有过相关项目构想并获得了融资兴趣，但最大的问题是这类课题的核心困难在「人」而非技术，本质上是按设计就解不开的问题。整段对话是对当前形式化验证 + LLM 融资热潮的辛辣讽刺。