使用可进行逻辑验证的模型和属性分析系统规范与设计的方法。
Hillel Wayne介绍了利用形式化方法在系统实现前发现设计缺陷的原则，重点关注性质的强度、状态空间探索以及环境假设。示例说明，对并发、故障和重试进行简化分析，如何及早暴露代价高昂的错误。