数值函数形式化验证：中间语言与验证平台选型

基于 [[数值函数形式化验证-想法与约束.md]] 中 PureLibm-rs 五级验证体系，探索 Rust 之外的验证平台选择，评估中间语言作为"一次证明、多语言分发"中枢的可行性。

整理日期：2026年6月

〇、核心问题

在 PureLibm-rs 的五级验证体系中，L3（Gappa 多项式误差证明）和 L4（Coq/Flocq 完整正确舍入证明）是语言无关的——证明的是算法而非特定实现。这引出一个架构问题：

是否存在一个中间语言，可以在其中完成算法验证，然后提取到多语言（C/Rust/Julia），通过差分测试对齐？

即"一次证明、多语言分发"的模式：

验证平台 (单一语言) ──→ 机器可检查的证明
       │
  AI 翻译 / 提取 ↓
┌──────┼──────┐
C     Rust   Julia
│      │      │
└──┬───┴───┬──┘
   ↓
差分测试对齐 (穷举/随机 + oracle)

本文档系统评估了五个中间验证语言/平台（Why3、Boogie、Viper、Dafny、CakeML）和四个验证平台（SPARK/Ada、C+Frama-C、Coq/Flocq、VST+CompCert），给出针对此场景的选型建议。

一、评估维度

维度	含义
IEEE 754 形式化完备性	语言/工具是否内置 IEEE 754 浮点的形式化语义模型
浮点精度证明能力	能否自动或半自动证明舍入误差 bound（如多项式逼近误差 ≤ N ULP）
代码提取目标	能否从验证语言生成可执行代码，支持哪些目标语言
多语言前端	能否从 Rust/C/Ada 等语言的代码翻译到该平台做验证
Coq 后端	能否生成 Coq 验证条件，以进行 L4 级完全形式化证明
TCB 大小	信任基（Trusted Computing Base）的大小——需要信任多少未经验证的代码
AI 辅助友好度	语言/工具的训练数据丰富程度，AI 生成代码和标注的质量预期
浮点验证成熟度	是否有已完成的 libm 级浮点函数验证案例

二、中间验证语言对比

2.1 Why3/WhyML（Inria）

目前唯一满足"IEEE 754 形式化 + C 提取 + 多语言前端 + Coq 后端"完整链条的 IVL。

架构:
  Rust ──→ Creusot ──→ WhyML ←── SPARK/GNATprove ←── Ada
                        │
  C ──────→ Frama-C WP ─┤
                        ↓
                  Why3 调度
                    ├── SMT (Z3, CVC4, Alt-Ergo)
                    ├── Gappa (浮点舍入误差)
                    └── Coq (手动证明)
                        ↓
                  提取到 C / OCaml

IEEE 754 标准库（ieee_float.why）：

type float32 = <float 8 24>   (* binary32 *)
type float64 = <float 11 53>  (* binary64 *)

type mode = RNE | RNA | RTP | RTN | RTZ

val add: mode -> float32 -> float32 -> float32
val sub: mode -> float32 -> float32 -> float32
val mul: mode -> float32 -> float32 -> float32
val div: mode -> float32 -> float32 -> float32
val fma:  mode -> float32 -> float32 -> float32 -> float32
val sqrt: mode -> float32 -> float32

val to_real: float32 -> real          (* 浮点→实数 *)
val of_real: mode -> real -> float32  (* 实数→浮点，带舍入 *)

val is_finite: float32 -> bool
val is_nan: float32 -> bool
val is_infinite: float32 -> bool
val is_normal: float32 -> bool
val is_subnormal: float32 -> bool
val is_positive: float32 -> bool
val is_negative: float32 -> bool

"unbounded float"方法论：

Inria 团队在验证 log-sum-exp（LSE）和 SLSE 时引入的核心技巧 —— 将精度证明和溢出证明分离：

(* 步骤 1: 在 unbounded float 中证明精度——不考虑溢出 *)
lemma accuracy_bound: 
  ∀ x: ub_float32, 
  abs (to_real (compute x) - exact_value x) ≤ ε * abs (exact_value x)

(* 步骤 2: 单独证明原始程序不溢出 *)
lemma no_overflow: 
  ∀ x: float32, is_finite x → is_finite (compute x)

已验证案例： LSE（log-sum-exp）和 SLSE（mutual information）——误差 bound 参数化于底层 exp/log 实现的精度假设。

维度	评价	说明
IEEE 754 形式化	⭐⭐⭐⭐⭐	`ieee_float.why` 是除 Flocq 外最完整的形式化
浮点精度证明	⭐⭐⭐⭐	Gappa 集成，天然适合多项式误差 bound
代码提取	⭐⭐⭐½	C ✅ OCaml ✅ Rust ❌（Creusot 只有反向）
多语言前端	⭐⭐⭐⭐⭐	C, Ada, Rust, Java, Solidity
Coq 后端	⭐⭐⭐⭐	生成 VCs 供 Coq/Flocq 证明
TCB 大小	⭐⭐⭐½	Why3 框架本身 + SMT solvers（Gappa 已验证）
AI 友好度	⭐⭐½	WhyML 训练数据少
浮点验证成熟度	⭐⭐⭐⭐	LSE/SLSE 案例，Frama-C 工业案例

2.2 Boogie（Microsoft Research）

最简洁的 IVL。不提取代码，不做浮点精度验证。

Dafny / VCC / SDV ──→ Boogie ──→ Z3 (SMT)

维度	评价	说明
IEEE 754 形式化	⭐⭐	无原生浮点类型，通过 SMT 浮点理论模拟
浮点精度证明	⭐	没有 Gappa 集成，舍入误差 bound 的证明极不自然
代码提取	❌	不提取代码
多语言前端	⭐⭐⭐	Dafny, C# (Spec#), C (VCC/SMACK)
Coq 后端	❌	无
TCB 大小	⭐⭐⭐½	Boogie + Z3

结论：不适合此场景。 Boogie 的哲学是"把验证问题翻译成 SMT 公式"——它没有 IEEE 754 的形式化模型，没有 Gappa 用于误差 bound，不提取代码。

2.3 Viper（ETH Zurich）

分离逻辑最强。面向内存安全和并发，不为数值精度设计。

Prusti (Rust) / Nagini (Python) / Gobra (Go) ──→ Viper ──→ Z3

维度	评价	说明
IEEE 754 形式化	⭐	无原生支持
浮点精度证明	⭐	不在设计目标中
代码提取	❌	不提取
多语言前端	⭐⭐⭐⭐	Rust, Python, Go, Java (VerCors)
Coq 后端	❌	无
浮点验证成熟度	❌	无 libm 级案例

结论：不适合此场景。 Viper 的核心优势在权限推理——如果你未来需要验证"多线程数值计算"中的内存安全，它是首选。但对于数学函数的精度验证，它没有任何专用能力。

2.4 Dafny

SMT 自动验证语言。Rust 提取是最大亮点，但 IEEE 754 形式化深度不足。

架构:
  Dafny 源码 (.dfy)
      ├──→ Boogie → Z3 (验证)
      └──→ 直接编译到 C#/JS/Java/Go/Python/Rust

维度	评价	说明
IEEE 754 形式化	⭐⭐½	`fp32`/`fp64` 类型在集成中，无不依赖 SMT 的显式形式化
浮点精度证明	⭐⭐½	无 Gappa，依赖 SMT 浮点理论（功能弱于专用工具）
代码提取	⭐⭐⭐⭐	C# ✅ JS ✅ Java ✅ Go ✅ Python ✅ Rust ✅ (AWS, POPL 2025)
多语言前端	❌	只有 Dafny 自身
Coq 后端	❌	无
AI 友好度	⭐⭐⭐⭐	语法接近主流语言，LLM 支持好
浮点验证成熟度	⭐⭐	统计库（Mean, Variance），无 sin/cos/exp

Dafny-to-Rust 编译器（AWS + UC Berkeley, POPL 2025）：

9/10 benchmark 性能≤手写 Rust 的 1.22×
2/10 达到性能平价
解决了类型系统差异、内存管理、跨语言互操作

CakeML 后端（Dafny 2025）：

Dafny IR → CakeML → 验证的编译链
减少 Dafny 的 TCB（不再信任 C#/Rust 编译器）

结论：Dafny 有潜力但浮点验证不成熟。 适合"快速得到一个可用的验证+Rust代码"。对于"不可质疑的正确性规格"，Why3 > Dafny。

2.5 Gillian（Imperial College）

符号执行 + 分离逻辑。研究阶段，不适用。

维度	评价	说明
代码提取	❌	不提取
浮点支持	❌	不在设计目标中
C 前端	✅	Gillian-C 基于 CompCert 语义（比 Why3 的 C 前端 TCB 更小）

优势在 Gillian-C 使用 CompCert 语义——长期看，如果 Gillian 将来支持浮点，这条路径的 TCB 比 Frama-C 更小。但目前不适用。

三、验证语言/平台对比

3.1 C + Frama-C/ACSL + Gappa

当前工业级浮点验证最成熟的 C 路径。

工作流:
  CORE-MATH C 代码 + ACSL 标注
    → Frama-C WP 插件 → WhyML VCs
    → Gappa (舍入误差) + SMT (程序逻辑) + Coq (超越函数)

维度	评价	说明
IEEE 754 形式化	⭐⭐⭐⭐½	ACSL 支持 Full IEEE 754 模型（含 NaN/Inf/signed zero）
Gappa 集成	✅	天然适合多项式逼近误差证明
C 语言形式化语义	⭐⭐	不基于 CompCert，C 语义在 Frama-C 中非形式化定义
UB 风险	⚠️	验证假设"无 UB"，需 value analysis 辅助排除
工业验证案例	✅	Safran 惯性导航（四元数浮点运算）
CORE-MATH 对接	✅	直接在 CORE-MATH C 代码上加标注，零翻译
AI 标注能力	⚠️	ACSL 训练数据少，AI 写 ACSL 标注质量存疑

关键优势： CORE-MATH 本身是 C，验证对象无需翻译。Gappa 是其多项式误差证明的设计场景。

关键劣势： C 的 UB 是结构性问题——验证的是"假设没有 UB"下的正确性。

3.2 SPARK/Ada

工业级最高内置保证。浮点数学库验证正在发展中。

维度	评价	说明
IEEE 754 支持	⭐⭐⭐⭐	语言内置 `Float'Pred`/`Float'Succ`、range types
浮点精度证明	⭐⭐⭐⭐	PropaFP 已验证 Taylor sin + Heron sqrt
形式化验证级别	Gold	完全功能证明（spark_math 部分函数）
libm 级验证	⚠️	spark_math 以定点为主，超越函数在 roadmap
AI 友好度	⭐⭐	Ada 训练数据极低，AI 翻译到其他语言质量差
生态大小	⭐⭐	社区小，库少

核心矛盾： 证明能力强，但作为"AI 翻译源语言"不适合——AI 从 Ada 翻译到 Rust/C/Julia 的质量，会因训练数据极度匮乏而远低于从 C 翻译。

3.3 Coq/Flocq

最高级别的形式化保证。IEEE 754 本身在 Coq 中形式化并证明了性质。

为什么 Coq/Flocq 是"最高级"的证明：

层级	证明对象	TCB 包含
SMT/Kani	具体输入上的程序行为	SMT solver（Z3 ~50万行C++）
Gappa	多项式在区间上的误差界	Gappa 本身（已验证）
SPARK Gold	Ada 代码满足标注	GNAT 语义 + SMT solver
Frama-C + Gappa	C 代码 + 浮点误差 bound	Frama-C 前端 + Gappa + SMT
VST + CompCert	C 程序的 CompCert 语义	Coq 内核（~2万行OCaml）
Coq/Flocq	浮点运算的形式化模型本身	Coq 内核

Flocq 证明的不是"这个程序对"——Flocq 证明的是"什么是 IEEE 754 舍入"以及"这个舍入模型具有什么数学性质"。

Flocq 的内容层次：

Core/RoundPred.v      — 舍入谓词的形式化定义（什么是合法的舍入方向）
Core/RoundNE.v        — round-to-nearest-even 的性质证明
Core/Ulp.v            — ULP 的形式化定义和性质
Core/FLT.v            — 浮点格式（任意尾数精度和指数范围）
IEEE754/Binary.v      — binary32/binary64 的完整 IEEE 754 语义
Calc/                 — 运算的具体实现和误差界证明
Prop/                 — 舍入误差的通用性质（如相对误差≤0.5ulp）

Flocq 实际能够处理的：

Hard-to-round cases 的完备性证明（不能靠穷举，因为 f64 有 2^64 个输入）
Range reduction（Payne-Hanek）的形式化——含条件分支和取模，超出 Gappa 区间分析范围
不同舍入模式的参数化证明
调用链的组合保证（已验证函数的规约可直接作为调用者的前提）

3.4 VST + VCFloat2（C + Coq）

C 程序的完整机器检查证明链，CompCert 语义 + Flocq 浮点模型。

VST (验证 C 程序满足功能规范)
  + VCFloat2 (浮点舍入误差分析)
  + CompCert (形式化验证的 C 语义)
  + Flocq (IEEE 754 形式化模型)
  → 全部归约到 Coq 内核

CPP 2024 已验证的应用： ODE Leapfrog 积分、Jacobi 迭代、稀疏矩阵转换。

与 Frama-C 的本质区别： Frama-C 的 C 语义是工具内部定义的非形式化语义。VST 的 C 语义是 CompCert 的——在 Coq 中形式化并证明了正确性的编译器。TCB 从"Frama-C + SMT solver"缩小到"Coq 内核"。

四、Why3 直接使用 vs Frama-C + Why3

4.1 两条路径的本质差异

维度	Why3 直接使用	Frama-C + Why3
出发语言	WhyML（手写）	C（CORE-MATH）
验证对象	算法本身	已有的 C 实现
核心产出	WhyML 规格 + 证明 + C 代码	被验证的 C 代码 + ACSL 标注
核心价值	"这个算法是正确的"	"这个 C 实现是正确的"
TCB	Why3 框架 + SMT	+ C 语言语义（非 CompCert）
CORE-MATH 对接	需手动翻译算法逻辑	直接在原始代码加标注
AI 翻译友好度	WhyML→C 由 Why3 保证	C→Rust/Julia AI 翻译

4.2 两条路径可以共存

                    WhyML (真理源)
                    /          \
     Frama-C + ACSL            Why3→C 提取
     CORE-MATH C 代码           可信任的 C 参考实现
           │                        │
           └────────┬───────────────┘
                    ↓
              交叉验证 (ACSL 标注 ↔ WhyML 规格)
                    ↓
              AI 翻译到 Rust
                    ↓
              差分测试对齐

交叉验证本身是最高强度的保证——同一算法的两个独立形式化互相验证。

五、CakeML：一个特殊的选项

5.1 CakeML 是什么

CakeML 不是 IVL——它是在 HOL4 定理证明器中形式化验证的编译器（Standard ML 子集 → 机器码）。

5.2 CakeML 的浮点能力

CakeML 有三个独立的浮点相关项目，形成完整链：

项目	功能
HOL4 IEEE 754 形式化	HOL4 中的 IEEE 754 浮点语义形式化
FloVer	舍入误差 bound 证书检查器——证明 `max
RealCake	扩展 CakeML 编译器支持 fast-math 优化（FMA 收缩等），同时证明优化后机器码与原始实数语义之间的误差 bound

FloVer 恰好覆盖 L3（多项式求值的误差证明）。 但只限直线代码——不处理 range reduction 等复杂控制流。

RealCake（ECOOP 2022）的三层语义：

标准 IEEE 754 语义（严格模式）
放松的浮点语义（允许 FMA 收缩等优化）
实数语义（ground truth）

编译器自动证明 I/O 行为在这三层之间的误差 refinement。JetEngine 内核在 Raspberry Pi 上加速 95%，误差 bound 被形式化证明。

5.3 CakeML 作为 Why3 的提取后端

当前:  Why3 → C 提取 → gcc/clang → 机器码 (信任 C 编译器)
改进:  Why3 → CakeML 提取 → CakeML 编译器 → 机器码 (编译器已验证)

注意：CakeML 替代的是 C 编译器（gcc/clang），不是 Coq。 它作为 Why3 的"第二个提取后端"，让编译阶段也有 Coq 级别的形式化保证，与 Coq 证明后端并列——一个保证证明正确，一个保证编译正确。

现状： WhyML→CakeML 在架构上可行，Dafny 2025 已有 Dafny→CakeML 先例。但没有人做过 WhyML→CakeML，需要自己实现翻译层。

六、对各语言的建议

6.1 Rust

地位： L0-L2 最佳实现语言，验证需借助 Why3/Creusot。

L0（类型系统+lint）：✅ 最佳
L1（穷举测试+oracle）：✅ proptest + MPFR FFI
L2（Kani 模型检查）：✅ 有限但够用
L3+（Gappa/Coq）：❌ 需要走出 Rust。LLVM 没有形式化浮点语义

6.2 TypeScript

不适合。 TS 的 number 是 IEEE 754 binary64，但：

无法控制舍入模式、检测浮点异常、做位编码操作
TS 验证工具（TheoremTS、Plumbproof）面向业务逻辑（金额守恒），不是数值分析（ULP 误差界）
脚本语言的浮点语义是"whatever the runtime does"——与形式化验证的"exactly what the spec says"结构性矛盾

6.3 Julia

适合作为算法原型 + oracle，不适合作为形式化验证平台。

IntervalArithmetic.jl（IEEE 1788-2015）：保证计算结果包含真值
ValidatedNumerics.jl：捆绑区间求根、全局优化、Taylor 模型
llvmcall + constrained intrinsics：比 Rust 更底层控制 LLVM 浮点语义

鸿沟： 区间算术给出 bound，但不是机器可检查的证明。Julia 社区在讨论生成 Lean/Coq certificate，但未实现。

6.4 Python

不适合。 Nagini 的浮点验证非常有限，重点在内存安全和引用计数，不在精度。

6.5 总结矩阵

浮点语义确定性
  ↑
  │  C + fenv       SPARK/Ada
  │
  │  Dafny
  │
  │  Rust           Julia
  │
  │  Python         TypeScript
  └──────────────────────────────→ 验证工具成熟度

七、推荐方案

7.1 核心架构

                    手写 WhyML
               (ieee_float + 算法 + 误差 bound 证明)
                         │
            ┌────────────┼────────────┐
            ↓            ↓            ↓
      Why3 验证通过   Why3→Coq VCs   (未来) Why3→CakeML
            │            ↓               ↓
            │       Coq/Flocq 证明   验证的机器码
            │       (L4: 完整正确舍入)
            ↓
      Why3 提取到 C
      (可信任的参考实现)
            │
   ┌────────┼────────┐
   ↓        ↓        ↓
AI→Rust  AI→Julia   保留 C
   │        │        │
   └───┬────┘────────┘
       ↓
  差分测试对齐
  (穷举 f32 + 随机 f64 + hard-to-round cases + CORE-MATH oracle)

7.2 Why3 直接使用 vs Frama-C + Why3 的选择

推荐分两步验证，而非二选一：

阶段	任务	时间
Pilot	Why3 直接使用——选 `cr_sqrtf` 在 WhyML 中完成全链路：IEEE 754 标注 → Gappa 误差 bound → SMT 程序逻辑 → 提取到 C → 和 CORE-MATH 交叉验证	2-4 周
决策点	基于 Pilot 结果决定后续路线	—

Pilot 结果决策矩阵：

Pilot 结果	建议
WhyML 流程顺畅	继续深化 Why3 路径，WhyML 成为真理源
WhyML 写起来太痛苦	转 Frama-C + ACSL，直接在 CORE-MATH C 代码上加标注
Gappa 对 range reduction 处理不了	已知局限，需 Coq 介入（不影响 Why3/C 的选择）
AI 翻译 C→Rust 质量好	Why3→C + AI 翻译路径可行，不需要 Dafny 的 Rust 提取

7.3 各验证层的归属

层级	保证内容	归属
L0（类型系统+lint）	降低 UB/panic 风险	每种目标语言自己做
L1（穷举测试+oracle）	f32 穷举 + f64 采样 + hard-to-round cases	语言相关，但 oracle 和测试集跨语言共享
L2（模型检查）	无 panic/越界/溢出	每种语言自己做（Kani/Creusot/Frama-C）
L3（Gappa 多项式误差）	逼近误差 bound	语言无关，一次证明，所有语言复用系数和误差 bound
L4（Coq/Flocq 完整证明）	正确舍入	语言无关，对关键函数做，作为 L3 最终保险

"银弹"的核心是 L3。L4 是"如果某个函数需要最高保证"的选项。

7.4 可移植的资产清单

无论选择哪个验证平台，以下资产是独立于语言和工具的：

Gappa 证明脚本（语言无关）——证明多项式误差
系数生成脚本（Sollya，语言无关）——魔术参数出处
测试向量集（f32 全部 + f64 采样）——差分测试基础
Hard-to-round cases 列表——边界保证
Oracle 参考输出（MPFR 高精度）——正确的标准
Coq/Flocq 证明（语言无关）——终极保证

AI 翻译到目标语言后，用 3-5 做差分测试。1-2 保证系数正确性跨语言复用。6 是终极保险。

八、风险与局限

风险	说明	缓解
WhyML 学习曲线	WhyML 不是主流语言，没有 Rust/C 的社区体量	Pilot 阶段快速验证可行性
超越函数需要公理化	`sin`/`cos`/`exp` 在 Why3 的 `real` 理论中是未解释符号	手写公理，或依靠 Coq/Flocq
Gappa 只擅长直线代码	Range reduction 含条件分支和取模，超出区间分析范围	需 Coq 手动介入
没有 Rust 提取	WhyML→Rust 不存在	AI 翻译 C→Rust + 差分测试弥补
CORE-MATH 只有部分函数有 Coq 证明	L4 的现实上限	你的 L4 作为文档和演进目标，不急
形式化验证 + 数学库两个深坑	需设边界防无限考古	Pilot 阶段设明确完成定义

〇、核心问题​

一、评估维度​

二、中间验证语言对比​

2.1 Why3/WhyML（Inria）​

2.2 Boogie（Microsoft Research）​

2.3 Viper（ETH Zurich）​

2.4 Dafny​

2.5 Gillian（Imperial College）​

三、验证语言/平台对比​

3.1 C + Frama-C/ACSL + Gappa​

3.2 SPARK/Ada​

3.3 Coq/Flocq​

3.4 VST + VCFloat2（C + Coq）​

四、Why3 直接使用 vs Frama-C + Why3​

4.1 两条路径的本质差异​

4.2 两条路径可以共存​

五、CakeML：一个特殊的选项​

5.1 CakeML 是什么​

5.2 CakeML 的浮点能力​

5.3 CakeML 作为 Why3 的提取后端​

六、对各语言的建议​

6.1 Rust​

6.2 TypeScript​

6.3 Julia​

6.4 Python​

6.5 总结矩阵​

七、推荐方案​

7.1 核心架构​

7.2 Why3 直接使用 vs Frama-C + Why3 的选择​

7.3 各验证层的归属​

7.4 可移植的资产清单​

八、风险与局限​

九、相关资源​