形式化验证

形式化验证关注的是：怎样把对程序或系统的要求写成足够精确的命题，并让机器检查“实现满足要求”的论证。

这个专题暂时不急着写成一篇总论。先把过去关于类型系统、Software Foundations、Functional Programming in Lean 和 TLA+ 的学习放到同一张地图上，再从具体问题长出文章。

一条从日常编程到机器证明的连续谱

这些方法不是简单的“形式化 / 不形式化”二分，而是在表达能力、自动化程度和成本之间取不同位置：

1. 让非法状态无法表示

- tagged type、newtype、ADT、phantom type

- 编译器能够排除一部分类型错误，但通常不能证明任意业务性质

- 已有文章：tagged-types-for-ids、strong-vs-dynamic-types-ai-codegen

2. 在边界检查更细的约束

- schema、refinement type、运行时 validator

- 适合字符串格式、数值范围、跨字段约束和外部输入

- 已有笔记：java refined type

3. 用测试搜索反例

- example-based testing、property-based testing、fuzzing

- 找不到反例不等于已经证明，但可以用较低成本覆盖大量情况

4. 穷举有限状态空间

- SAT、SMT、model checking

- 特别适合协议、并发状态机和系统设计

- 已有材料：@Specifying systems%3A the TLA+ language and tools for hardware and software engineers、@Specifying systems

5. 构造并检查证明

- Coq、Lean 等 proof assistant

- 人负责选择定义、定理和证明思路，kernel 检查证明项

- 已有读书笔记：software foundations volume 1%3A logical foundations

把 Software Foundations 和 Lean 4 结合起来

两者可以围绕同一批概念组织，而不是写成两套互不相干的软件教程：

当前实际进度是：Software Foundations 读到第 3 章；Functional Programming in Lean 已经读完；Theorem Proving in Lean 4 还没有开始。当前 vault 中保留了部分 Software Foundations 笔记，但还没有找到 Functional Programming in Lean 的读书笔记。上面的表格只是以后可能使用的对照维度，不代表已经决定的下一步。

后续要继续证明助手、转向 model checking，还是从具体工程问题出发，目前还没有想清楚。先如实保留这个开放状态，不把候选想法写成 roadmap。

知乎旧文在专题里的位置

tagged-types-for-ids 解决的是一个很具体的问题：不要让 UserId 和 PortfolioId 因为底层都是 String 就能互相误用。

它与形式化验证的联系在于：把原本只存在于注释和程序员脑中的约束，编码进机器能够检查的形式系统。

但它只能证明“这里传入了带 PortfolioId 标记的值”，不能自动证明：

- 底层字符串确实对应数据库中的 Portfolio；

- 创建 tagged value 时没有滥用 cast；

- 整个业务流程满足更高层的不变量。

所以它很适合作为专题第一层：先看类型能免费排除什么，再追问剩余性质应该由 validator、测试、model checker 还是 proof assistant 保证。

可以逐步长出的文章

暂未确定。等新的具体问题或写作动机出现后，再从已有阅读和笔记中长出文章。

待整理

- [ ] 后续方向尚未想清楚；等具体问题出现后再补 roadmap