Show HN：Statespace 通过构建一门小型可校验语言来学习形式化方法

一位有系统经验的后端工程师用 Claude 为自己定制了一门形式化方法课程，核心是构建一门用 z3 找 bug 的可校验应用语言，在 Lean 中做证明、用 TLA+ 建模并发与分布式系统行为，并接入 PostgreSQL。课程以静态站点形式托管在 GitHub Pages 上，作者自认缺乏该领域经验，发布主要为了向专家征求反馈和建议。