形式验证利用数学模型和逻辑学推理，确立硬件或软件系统满足精确定义的规约。在计算机科学中，它既可以验证特定性质，例如内存访问的安全性，也可以验证有关功能行为的更广泛断言。其结论涵盖模型和假设所包含的全部行为，而不只是选定的若干次执行。验证可以通过机器检查的形式证明或穷尽式算法分析来确立某项断言；它并不能脱离规约来确立正确性。(cs.cmu.edu)
规约与模型
验证需要形式化地描述系统实际做什么，以及它应当做什么。模型可以表示程序执行、电路的状态变化或组件之间的交互。其精确程度取决于所选的抽象方式：高层协议模型可以省略实现细节，而代码级模型则必须考虑编程语言的相关特性，包括内存操作和算术行为。用于底层软件验证的工具会显式建模位向量和浮点运算等特性。(cs.cmu.edu)
性质可以描述单个状态，也可以描述完整的执行过程。安全性性质排除某种不期望发生的事件，例如数组越界访问。进展要求则关注某个事件最终是否会发生。时序逻辑提供了表达“始终”“最终”和“直到”等概念的算子，因此适合用来规定并发计算系统的行为。验证针对的是所声明的性质，这些性质不必构成涵盖系统所有特征的完整规约。(cprover.org)
证明模型正确，与确立模型忠实地反映了实际部署的系统，是两件必须区分的事。硬件行为、初始化过程、外部库和环境约束可能仍然只是证明所依赖的假设。例如，关于模型中信息通道的证明，并不会自动涵盖模型中未包含的时序通道。(sel4.systems)
演绎式程序验证
演绎式验证通过逻辑系统来确立程序的性质。霍尔逻辑用三元组表达基本的正确性判断：
其中， 是前置条件， 是命令， 是后置条件。按照部分正确性的解释，如果执行从满足 的状态开始并终止，那么其最终状态就满足 。完全正确性还要求执行必须终止。因此，仅证明后置条件，并不一定能说明程序会返回结果。(cs.cornell.edu)
赋值、顺序执行、条件分支和循环的推理规则，可以将较大的断言化归为较小的证明义务。循环不变量描述在各次迭代中保持成立的性质。证明需要确立：该性质在进入循环之前成立，经循环体执行后仍然成立，并且在循环退出时能够推出所要求的结果。终止性可以另行证明，方法是使用一个按良基序递减的量。(cs.cornell.edu)
证明助手支持构建和检查这些论证。用户提供定义和中间断言，自动化机制则可以完成部分证明义务。这种保证取决于推理系统的可靠性（逻辑学）及其证明检查机制的正确性。采用小型可信内核的证明助手，旨在减少必须直接信任的软件量。(sel4.systems)
模型检查与有界分析
模型检查通常通过分析状态迁移结构，判断系统模型是否满足某项性质。对于有限状态系统，算法可以检查所有相关的可达状态，而无需人工构建演绎证明。当某项性质不成立时，检查器通常可以给出反例，展示违反该性质的执行过程。这类执行轨迹使模型检查既可用于确立性质，也可用于诊断设计错误。(cs.cmu.edu)
有界模型检查检查不超过指定界限的执行过程。一种方法是将状态迁移步骤和可能的性质违反情况编码为布尔可满足性问题。一个满足赋值代表界限内的反例。不可满足的结果排除了编码所涵盖的搜索空间中的违反情况，但仅凭这一结果，不能排除更长执行过程中的违反情况。(cprover.org)
对于含有循环的程序，如果能证明所选的展开界限涵盖了所有相关迭代，就可以将有界分析的结论强化为针对所建模程序的穷尽性结果。CBMC 为此使用展开断言。如果覆盖范围不足，那么成功通过有界检查仍然只是一种有限范围的保证，而非不受界限限制的正确性证明。(github.com)
应用与实例
形式验证适用于硬件设计和软件组件。硬件模型检查可以检查电路行为，软件工具则可检查指针安全性、算术异常和用户指定的断言等性质。其范围可以小至单个函数，也可以扩展到操作系统中的选定组件。(cs.cmu.edu)
seL4 微内核展示了如何在多个抽象层次上进行验证。它的证明体系将实现与更高层的规约联系起来，涵盖功能正确性和安全性质。覆盖范围取决于架构和配置：并非每个变体都已证明所有性质。其假设文档列明了仍然存在的依赖，包括硬件行为和某些底层代码。(sel4.systems)
CompCert编译器是经验证编译的一个实例。其经过机器检查的正确性论证，将受支持的 C 程序的可观察行为与编译生成的汇编代码联系起来。这确立的是翻译过程的性质，而非应用程序是否实现了预期功能。要证明源程序满足其需求，仍需单独论证；编译器的保证也附带有关未定义行为和配套工具链的条件。(arxiv.org)
局限与保证
验证受到计算能力和建模方面的约束。状态空间可能迅速膨胀，而动态分配、并发、外部调用和复杂的语言特性也会增加软件验证的难度。抽象可以缩小问题规模，但抽象模型与实现之间的关系本身也必须得到论证。(cs.cmu.edu)
可信计算基由证明所依赖、却未被证明完整覆盖的组件构成。这些组件可能包括证明检查器、未经验证的工具链阶段、硬件模型或初始化代码。在这些边界处，测试和人工验证仍然重要：数学论证无法确立物理硬件的行为与假设完全一致。因此，关于验证保证的声明必须明确指出经过验证的对象、已证明的性质、覆盖的配置，以及将形式化结果与实际执行联系起来的假设。(arxiv.org)