形式化守护

靠测试守不住的性质交给证明与模型检查，测试仍负责找出缺陷，两者不互相替代。每个结论带证据，证据要真的检验了它声称检验的东西。做法加载技能 think-evidence。形式化定义的是实现的形状，所以放在实施之前；这一步的产出就是思维模型 think-model-first 的模型。

本技能分两档。偏函数定义与全化表便宜，碰到状态与操作就做，不需要人确认。模型检查与证明贵，按下面四类触发，代理建议、人确认后才做。

触发条件

出现下面任何一项，先判断要不要模型检查与证明，再实施：