Show HN：Statespace 用构建小型带检查语言来学习形式化方法

Statespace 是一个用 Claude 生成的形式化方法课程，面向有系统经验的后端工程师，通过构建一门用 z3 找 bug 的带检查应用语言来学习。课程还涵盖在 Lean 中做证明、用 TLA+ 建模并发与分布式系统行为，并连接 Postgres，以静态站点形式托管在 GitHub Pages 上。作者自述缺乏该领域经验，主要希望获得专家反馈与建议。