Ironclad 中的形式化验证是指我们让内核代码经历的一系列流程和检查，以确保 不存在运行时错误 (AoRTE)，并且确保其组件的正确性。我们用于此目的的主要工具是 SPARK，这是一种可验证的 Ada 子集。
Ironclad 的目标是拥有尽可能形式化验证的内核，这是一个我们不断努力实现的目标，同时尽量不影响项目的特性增长。
验证是一个昂贵且耗时的过程，其复杂性随着需要验证的代码量而增加。由于我们有一个小团队在 Ironclad 上工作，因此我们平衡这种巨大成本的方法是在关注新功能的同 时，一旦这些功能正常运行并稳定，我们就会对其进行验证。这导致 Ironclad 具有比其他情况更少的已验证代码，如果验证是首要任务的话，但我们相信这种方法使 Ironclad “值得进行验证”。验证一个无法运行任何软件的内核有什么用，因为它的功能还不完善！归根结底，我们有限的人力资源使我们不得不仔细选择要处理的任务，并且 完全适合 Ironclad 目前所处的预 alpha 阶段。
因此，Ironclad 并非 100% 都是经过验证的代码。其大部分与架构无关的代码都位于 SPARK 的范围内，其中大部分处于较低级别的验证阶段，而更具安全性和用户导向 的部分则经过了更高等级的 SPARK 验证。架构代码的验证程度要低得多。
SPARK 是一种形式化的可验证的 Ada 子集，它使我们能够轻松且方便地验证 Ada 代码库中的部分内容，同时使其与未经过验证的部分互操作。SPARK 在航空航天、国防和交 通运输行业中拥有悠久的使用历史，最重要的是，它具有出色的 FOSS 检查器选项，例如 GNATProve，这是我们与 Ironclad 配合使用的检查器。
SPARK 本质上由对现有 Ada 代码编写的契约和约束组成，这些契约和约束与 SPARK 对代码本身的要求一起，形成了一种代码行为的规范，该规范经过数学检查。GNATProve 使用各种演绎框架来执行此检查，例如 Why3、CVC4 和 Z3。由于这些契约和条件本身就构成了规范，因此不需要作为 SPARK 的一部分提供单独的规范。
这些契约的示例包括：
procedure Increment (X : in out Integer)
with Pre => X < Integer'Last; -- 确保递增操作不会溢出。
subtype Prime is Integer range 2 .. Integer’Last
with Dynamic_Predicate => (not (for some N in 2 .. Prime - 1 => Prime mod N = 0));
-- 确保只能将素数分配给这种类型。
procedure Swap_Bad_Depends (X, Y : in out Integer)
with Depends => (X => Y, Y => X),
Post => X = Y'Old and Y = X'Old
-- 确保 X 和 Y 的状态仅受彼此影响，并且确实发生了正确的交换。
经过分析后，SPARK 代码被分为 5 个级别，这些级别相互构建，具体取决于其验证的质 量、正在验证的内容以及使用此验证所做的保证，这些级别从低到高依次为：
| 级别 | 含义 |
|---|---|
| Stone | 有效的 SPARK，作为采用过程中的中间级别，并允许代码与其他的 SPARK 代码进行接口 |
| Bronze | 正确的数据初始化和流程，但没有关于健全性和 AoRTE 的保证 |
| Silver | 完整的 AoRTE，这意味着不会发生任何不正确的数据状态、内存泄漏或其他情况，但没有关于逻辑健全性的保证 |
| Gold | 建立在 Silver 之上，使用 GNATProve 检查规范和关键逻辑属性 |
| Platinum | 对逻辑规范进行完全验证，完全由开发人员自行决定。 |
Ironclad 分为不同的子系统，这在源代码中可以看作是子目录和 Ada 包。以下是项目的概述：
| 子系统 | SPARK 的 Stone 级别进度 | SPARK 的 Silver/Gold 级别进度 | 验证质量 |
|---|---|---|---|
| arch | 已完成 | 待定架构端口 | 待定架构端口 |
| arch/riscv64-limine | 未开始 | 待定 Stone 级别 | 待定 Stone 级别 |
| arch/x86_64-limine | 未开始 | 待定 Stone 级别 | 待定 Stone 级别 |
| cryptography | 已完成 | 已完成 | 完整的 AoRTE |
| devices | 已完成 | 大部分已完成 | 偶尔存在小错误 |
| ipc | 已完成 | 大部分已完成 | 选择性地进行完整的 AoRTE |
| lib | 已完成 | 已完成 | 完整的 AoRTE |
| memory | 已完成 | 未开始 | 待定 Gold 级别 |
| networking | 已完成 | 已完成 | 完整的 AoRTE |
| userland | 已完成 | 大部分已完成 | 系统调用未验证 |
| vfs | 已完成 | 部分 | 在某些地方进行完整的 AoRTE |
如果您想自己分析形式化验证状态和信息，可以使用 gnatprove 在本地对 Ironclad 进行检查。有关更多说明，请参见项目的 README。