大型代码库形式化验证变得实用

针对极大型代码库的形式化证明如今已具备可行性，过亿行代码的形式化证明不再荒谬。作者认为，形式化验证应成为设计高可靠性与安全性的新型安全系统时的关键考虑步骤。