vibecheck 黑客松亮点：带运行时注入投票验证的 Catan 克隆

spikedoanz · x · 2026-11-03

作者 spikedoanz 分享了周末担任 vibecheck 黑客松评审的经历，最欣赏的项目是一个品味不俗的 Catan(卡坦岛)克隆游戏——其投票系统带可证明的强制约束，且是在运行时注入实现的，项目已开源在 GitHub(parthavshergill/charter)。

引用的推文补充了活动全貌：60 多名极客用一个周末学习形式化方法(FM)，收获包括「C 的 int 不等于 Lean 的 int」「证明 vibe 翻译正确对原代码意义有限」「全称量化定理在前提不可满足时没用」等实操教训，完整结果即将公布。配图为四款风格各异的多主题棋盘游戏画面，展示该引擎可换皮肤生成不同 Catan 变体。