形式化验证

主要目的是证明系统具有某性质，如常见的功能正确性、并发安全等等。对于构建可信的安全攸关系统而言很重要，在其他场景中属于比较重量级的方法。