定理证明
这里进入 formal verification 的另一条重要路线：当有限状态搜索、状态压缩或符号方法仍然不够时，怎样把正确性问题转化成机器可检查的证明。
这一部分不会把 Oxpecker 变成 theorem prover，也不会要求读者立刻学习 Lean、Coq 或 Isabelle。它的目标是让读者理解：定理证明解决的不是“再多跑一些状态”的问题，而是用定义、引理和证明义务建立更一般的正确性保证。
计划覆盖：
text
为什么模型检查之后会遇到证明问题
证明义务
不变量证明
归纳证明
机器可检查证明
Lean / Coq / Isabelle / Verus 的位置