形式规范和验证
使用可证正确安全模型开发协议的主要优势在于它提供了对抗能力的保证限制。对于一份是合约，只要其协议遵循并且证明是正确的，那么对手就不能违反所声明的安全属性
更深刻的反省使得先前的断言更加显着。对手可以是任意智能和有能力的。说他们仅通过数学模型被打败是非同寻常的。当然，这不完全是真的。
现实引发了阻止纯安全的乌托邦和现有的正确行为的因素和情况。实施可能是错误的。硬件可以诱发以前未经考虑的攻击向量。安全模式可能不足，并且不符合现实生活中的使用。
对于协议需要多少规范、多严格和怎么检查的判断是需要的。例如，像SeL4 Microkernel项目这样的努力是一个很好的例子，全面的歧义需要近20万行的Isabelle代码来验证少于10万行的C代码。然而，操作系统内核是关键的基础设施，如果没有正确实施，可能是严重的安全漏洞。
所有加密软件是否都需要相同的艰巨努力？还是可以选择一个没有那么吃力的途径，以产生相当的结果？如果协议是完美实现的，那么如果它运行的环境是非常脆弱的，如Windows XP，那有没有关系？
对于卡尔达诺而言，我们选择了以下的妥协。首先，由于密码学和分布式计算领域的复杂性，证据往往是非常微妙、漫长、复杂和有时需要相当的技术性。这意味着人为的检查可能是乏味且容易出错的。因此，我们认为，为了涵盖核心基础设施而编写的白皮书中，提出的每一个重要证据都需要进行机器检查。
第二，为了验证Haskell代码是否正确对应于我们的白皮书，我们可以选择两种流行的选项：通过LiquidHaskell与SMT验证器进行接口并使用Isabelle / HOL。
可满足的模理论（SMT: satisfiability modulo theories）求解器处理满足方程式或不等式的功能参数的问题，或者说可以不存在这样的参数。如De Moura和Bjørner所讨论的，SMT的用例是多样的，但关键是这些技术都是强大的，并且可以大幅减少瑕疵和语义错误。
另一方面，Isabelle / HOL是一种更具表现力和多样性的工具，可用于指定和验证实施。 Isabelle是一个通用的定理解算器，可以处理高阶逻辑结构，能够表示集合和其它用于证明的数学对象。 Isabelle本身与Z3 SMT认证工具集成，以处理涉及此类限制的问题。
这两种方法都有价值，因此我们决定分阶段地含括这两种方法。人造书面证明将在Isabelle编码，以检查其正确性，从而满足我们的机器检查要求。我们打算逐渐将Liquid Haskell加入到卡尔达诺在2017年和2018年实施的所有生产代码。
最后一点，形式验证只能与可用工具集验证的规范相比。选择的Haskell的主要原因之一是，它提供了实用性和理论的平衡。从白皮书衍生出来的规范看起来很像Haskell的代码，连接这两个代码比用命令式语言更容易。
在获取适当的规范和更新规范时，仍然存在着巨大的困难，如升级，瑕疵修复和其他关注事项等需要做出更改;然而，这种现实并不能减弱总体价值如果在建立可证安全的基础上遇到麻烦，那么应该实施纸面提案。