形式化验证只保证代码满足规约，不保证规约忠实于自然语言需求，因此一个比需求更窄的属性的机器证明可能毫无价值却能通过所有检查。