正式验证
在硬件和软件系统的背景下，正式验证是使用正式的数学方法证明或反驳系统相对于某些正式规范或属性的正确性的行为。正式验证是对系统形式规范的关键激励措施，并且是正式方法的核心。它代表了电子设计自动化中分析和验证的重要维度，并且是软件验证的一种方法。正式验证的使用使得计算机安全认证的常见标准框架中具有最高的评估保证水平（ EAL7 ）。
正式验证可能有助于证明系统的正确性，例如：加密协议，组合电路，具有内部内存的数字电路以及以编程语言表示为源代码的软件。经过验证的软件系统的突出示例包括经过验证的C编译器和SEL4高保证操作系统内核。
这些系统的验证是通过确保存在系统数学模型的形式证明来完成的。用于建模系统的数学对象的示例是：有限状态机器，标记的过渡系统，喇叭从句，培养皿网，矢量加法系统，定时自动机，混合自动机，过程代数，编程语言的正式语言，例如操作语言，语言语言，语言语言学语言，公理语义和Hoare逻辑。
方法
一种方法和形成是模型检查，该模型由系统详尽的数学模型组成（对于有限模型来说，这是可能的，而且对于某些无限模型，无限的状态集可以通过抽像或利用优势有限地代表对称）。通常，这包括通过使用智能和域特异性抽象技术来探索模型中的所有状态和过渡，以在单个操作中考虑整个状态并减少计算时间。实施技术包括状态空间枚举，符号状态空间枚举，抽象解释，符号模拟，精炼。要验证的属性通常在时间逻辑中描述，例如线性时间逻辑（LTL），属性规范语言（PSL）， SystemVerilog断言（SVA）或计算树逻辑（CTL）。模型检查的最大优势是它通常是完全自动的。它的主要缺点是它不适合大型系统。符号模型通常仅限于几百个状态，而显式状态枚举要求探索状态空间相对较小。
另一种方法是演绎验证。它包括从系统中产生及其规格（以及可能其他注释）的数学证明义务集合，其真相暗示系统符合系统的规格，并使用任何一个证明助手（交互式定理抛弃）（互动定理）（交互式定理）（例如HOL ， ACL2 ， ISABELLE ， COQ或PVS ）或自动定理抛弃，包括特别是可满足的模型理论（SMT）求解器。这种方法的缺点是，它可能要求用户详细了解系统为什么正常工作，并将此信息传达给验证系统，要幺以一系列定理的形式进行证明，要幺以规格的形式证明（系统组件（例如功能或过程）以及子组件（例如循环或数据结构）的系统组件（例如功能或过程）的不变，前提，后结构）。
软体
对软件程序的正式验证涉及证明程序满足其行为的形式规范。正式验证的亚地区包括演绎验证（请参见上文），抽象解释，自动定理证明，类型系统和轻量级正式方法。一种有希望的基于类型的验证方法是依赖键入的编程，其中函数类型包括（至少一部分）这些函数的规范，并且对代码进行类型检查可以根据这些规格建立其正确性。完全具有依赖类型的语言支持演绎验证作为特殊情况。
另一种互补方法是程序推导，其中通过一系列正确性提供的步骤从功能规范中产生有效的代码。这种方法的一个例子是鸟类 - 大型形式主义，这种方法可以看作是构造的另一种正确性形式。
这些技术可以是合理的，这意味着可以从逻辑上从语义上推导的验证属性，也可以是不合适的，这意味着没有这种保证。声音技术只有一旦涵盖了整个可能性的空间就能产生结果。不健全技术的一个示例是仅涵盖了可能性的一个子集，例如，整数只能达到一定数字，并给出“良好的结果”结果。技术也可以是可决定的，这意味着其算法实现可以保证以答案或不可决定的终止，这意味着它们可能永远不会终止。通过界定可能性的范围，当没有可确定的声音技术可用时，可以构建可决定的不健全技术。
验证和验证
验证是测试产品适合目的的一个方面。验证是互补方面。通常一个人将整体检查过程称为V＆V。
- 验证：“我们是否试图做正确的事？”，即，该产品是否指定为用户的实际需求？
- 验证：“我们制造了我们要制作的东西吗？”，即产品是否符合规格？
验证过程包括静态/结构和动态/行为方面。例如，对于软件产品，可以检查源代码（静态）并与特定的测试用例（动态）相对。验证通常只能动态地进行，即，通过将其通过典型和非典型用法放置（“它是否令人满意地满足所有用例？”）来测试产品。
自动化程序维修
程序维修是针对Oracle进行的，其中包括用于验证生成修复程序的程序的所需功能。一个简单的示例是测试套件 - 输入/输出对指定程序的功能。采用了多种技术，最著名的是使用可满足的模量理论（SMT）求解器以及基因编程，并使用进化计算来生成和评估解决方案的候选者。前一种方法是确定性的，而后者是随机的。
程序维修结合了正式验证和程序合成的技术。正式验证中的故障平局技术用于计算可能是可能由综合模块靶向的可能性错误位置的程序点。维修系统通常专注于一小部分预定的错误类，以减少搜索空间。由于现有技术的计算成本，工业用途受到限制。
行业使用
设计的复杂性增长增加了硬件行业正式验证技术的重要性。目前，大多数或所有领先的硬件公司都使用了正式验证，但是软件行业的使用仍在萎缩。这可能归因于硬件行业的更大需求，因为错误具有更大的商业意义。由于组件之间潜在的微妙相互作用，因此越来越难以通过仿真来行使一组现实的可能性。硬件设计的重要方面适合自动证明方法，从而使正式验证更容易引入和更有生产力。
截至2011年，已经正式验证了几个操作系统：Nicta的安全嵌入式L4微粒，以OK Labs为SEL4商业出售；东中国师范大学的基于Osek/VDX的实时操作系统Orientais； Green Hills软件的完整性操作系统；和Sysgo的Pikeos 。 2016年，由耶鲁大学的中肖领导的一支团队开发了一个名为Certikos的正式验证的操作系统内核。
截至2017年，已通过网络的数学模型以及作为新的网络技术类别（基于意图的网络）的一部分，将正式验证应用于大型计算机网络的设计。提供正式验证解决方案的网络软件供应商包括Cisco Forward Networks和Veriflow Systems。
Spark编程语言提供了一种工具集，该工具集可实现正式验证的软件开发，并用于多个高融合系统。
Compcert C编译器是实施ISOC的大多数C的正式验证的C编译器。