01
四个领域，同一个标准
每个领域都按同一模式进行：不受信任的 C 驱动负责计算，Lean 检查器用精确有理数重新检查它的证书，一个成熟的程序在同一问题上作独立参照。点进各领域查看完整状态。
mini-DFT
一维周期约化 Hartree–Fock，平面波离散：基态、有限温度、展宽、k 点、能带与态密度，以及新加入的 LDA 交换。
mini-FEM
一维 Poisson 方程的 P1 线性元与梁方程的三次 Hermite 元，证书针对连续问题的真解。
mini-MD 新
一维 Lennard-Jones 原子链加 Velocity Verlet。每一步与真轨道的距离、守恒量与 Verlet 的结构性质都有证书。
mini-CALPHAD 新
读 TDB 数据库求二元相平衡、磁性相与相图。证书针对真正的全局平衡，而不只是求解器找到的那一个。
02
可信账本
项目的每一条命题都登记了等级、证据和所依赖的假设；运行报告的每一行都引用其中一条。等级的定义见纲领页，每条命题只标它实际达到的等级。
T4 命题是各个证书检查器的可靠性定理（检查器全程用精确有理数，不涉及浮点）与 C 可信内核无运行时错误的证明。尚未达到目标的 6 条：mini-DFT 5 条（见 DFT 页），以及 mini-MD 中 Newton 方程解的存在性。
03
一个结果的保证从哪里来
求解器从不被信任：它只负责提出候选，由经过证明的检查器裁决。这样我们既能用 LAPACK 和高效的浮点代码，又能把每个输出写成一条定理。四个领域走的是同样的四步。
求解器
C 驱动运行 SCF 循环、FEM 组装、Verlet 积分或平衡搜索，最后写出证书。
证书
浮点数按它本来的精确二进制有理数读入。证书里的任何内容都不被假定为正确。
检查器
用精确有理数重新检查一切。可靠性是 Lean 定理；证书有错只会让检查失败或区间变宽。
严格结论
可证明包含真实量的区间：FEM 连续问题的真解、MD 的真轨道、CALPHAD 的全局平衡。
与此同时，DFT 的 SCF 控制器写成 TLA+ 规范并经 TLC 检验（只有残差足够小、能隙打开、证书通过时才能报告“收敛”），每次运行都可以输出轨迹，按这份规范逐步重放检查。
04
目标与路线图各阶段
G1：mini-DFT 与 DFTK 功能对齐 2026-09-29 设定
46 项中完成 6 项，另有 4 项与 DFTK 一致；LDA 交换在 Γ 点加 MP/MV 展宽已有 SCF 解证书。先一维，再 d 维。逐项状态 →
G2：带形式化证明的有限元，对照 scikit-fem 2026-09-30 设定
26 项中完成 11 项；F0（一维 Poisson）已全部完成，F1（一维扩展）进行中。逐项状态 →
G3：带形式化证明的 CALPHAD，对照 pycalphad 2026-10-01 设定
23 项中完成 12 项；C0（二元点平衡）全部完成，C1 中完成了带证书的相图、Inden–Hillert–Jarl 磁性模型、驱动力与单相区化学势的收紧。下一步：间隙溶体与不变反应。逐项状态 →
- 阶段 0最小 DFT进行中
可信账本、Lean 证书检查器、可信报告、trace validation 已建立；四组基准全部通过，包括与 DFTK.jl 的交叉校验。
尚缺连续适定性、平面波先验误差估计、线性混合收敛的文献核对（目标 T1）；Lean 与 Rocq 的接口命题；区间算术的代码层证明（现为 T3，目标 T4）。
- 阶段 1DFT 扩展部分提前完成
k 点采样已实现并有证书；k 点的线程并行协议经模型检验，不同线程数的结果逐位一致。原计划之外还完成了有限温度占据及其自由能、熵与能量证书，Anderson 混合，非自洽能带与态密度，截断误差证书。
LDASlater 交换在 Γ 点加 MP/MV 展宽已有证书；PW92 关联、其他展宽与 k 点与 DFTK 一致，尚无证书。
未开始MPI 并行、三维平面波与赝势。
- 阶段 2MD 与 FEM已达退出标准
两个最小版本都输出可信报告。mini-FEM：一维 Poisson（P1）与梁（三次 Hermite），证书针对真解。mini-MD v0（2026-10-01）：一维 Lennard-Jones 原子链加 Velocity Verlet，证书针对真轨道。Céa 引理（FEM-D03）与 Verlet 辛性（MD-D03）都达到 T3。
未开始halo 交换、原子迁移、并行组装、检查点的 TLA+ 模块；MD 的周期盒子与恒温器。
- 阶段 3可信内核未开始
起点是区间算术内核：其正确性已对逐行模型证明（T3），C 代码无运行时错误已证明（T4）。
- 阶段 4对标未开始
Δ 量规、NVE 能量漂移、制造解收敛阶，连同对应的可信账本一起公开。
CALPHAD 不在纲领原有的阶段之中；它在 2026-10-01 作为目标 G3 加入，完成标准与 G1、G2 相同。
05
不经证明而信任的部分
每个领域的每一个保证都以这个小而明确的可信基为前提。
| Lean 4 | 检查所有证明的内核；Mathlib，只用三条标准公理 |
| Lean 编译器 | 把检查器编译成可执行程序，连同输入解析与十进制输出（下界向下、上界向上取整） |
| TLC | TLA+ 模型检验器 |
| Frama-C / WP | 连同 Why3、Alt-Ergo、Z3，用于 C 内核的运行时安全 |
| C 编译器 | 目前未经验证；可信内核将来可改用 CompCert |
| IEEE 754 | 只信任“就近舍入的结果是最近的 double”，不依赖误差大小 |
每个领域另有自己的建模约定，例如被认证的问题取证书中的精确有理数、TDB 数据库的翻译正确等，在各领域页面中相应的位置注明。
写出这些问题的 C 驱动不受信任，但有几道检查：报告逐行与检查器自己的输出对照；线程协议按 TLA+ 规范重放；在 AddressSanitizer 与 UBSan 下做模糊测试；无法精确写进证书的输入一律拒绝。这些都在 make verify-all 中运行。最大的剩余缺口是检查器既不重算也不回显证书中的问题数据。