核心问题

能不能在写代码前证明流程没有洞？

工程困境

订单、支付、退款、访问权组合起来后，状态空间很大。靠脑补很容易漏。

思想模型

TLA+、Alloy 这类工具的核心不是语法，而是思想：

定义状态
定义操作
定义不变量
让机器搜索反例

你不一定要精通形式化验证，但要学会形式化地问问题。

工程落地

用轻量方式也可以：

  • 画状态表
  • 列不变量
  • 列非法状态
  • 写 property-based tests
  • 写并发场景测试

Atlas Action

对一个复杂流程写：

State:
Actions:
Invariant:
Forbidden:

然后找一个能破坏它的反例。

小结

形式化验证的核心价值，是逼你把“应该没问题”变成“找不到反例”。