Grok Bot 工程负责人 Lauren Tan 分享她 4 天前作为副业项目开始开发的游戏，落地约 1150 个 PR。每当发现代码问题就让 bot 加一条 lint 规则；大量使用 TLA+ 验证剧情、过场动画和游戏系统的状态机，每个主要系统各有一个形式化验证 skill。