Formal in Silico — Progress

Four domains, one standard

Every domain follows the same pattern: an untrusted C driver computes, a Lean checker re-checks its certificate in exact rational arithmetic, and an established code serves as an independent reference on the same problem. Select a domain for its full status.

Goal G1 · reference DFTK.jl 0.8.0

mini-DFT

1D periodic reduced Hartree–Fock with plane waves: ground state, finite temperature, smearing, k-points, bands and DOS, and now LDA exchange.

102claims, 20 at T4 and 74 at T36 / 46DFTK parity items done, 4 more agree≤ 5×10⁻¹⁵energy difference from DFTK

Status of mini-DFT → Goal G2 · reference scikit-fem 12.0.2

mini-FEM

1D Poisson with P1 elements and beams with cubic Hermite elements, certified against the true solution of the continuous problem.

11claims, 3 at T4 and 8 at T311 / 26scikit-fem parity items done, all 1D≤ 3×10⁻¹⁵width of the true-solution nodal intervals

Status of mini-FEM → Version v0 · reference ASE 3.29

mini-MD new

A 1D Lennard-Jones chain with velocity Verlet. Each step’s distance from the true trajectory is certified, along with conserved quantities and Verlet’s structure.

14claims, 4 at T4 and 9 at T30.99true local error ÷ certified bound≤ 5×10⁻¹⁴trajectory difference from ASE

Status of mini-MD → Goal G3 · reference pycalphad 0.11.1

mini-CALPHAD new

Binary phase equilibria, magnetic phases and phase diagrams read from TDB databases. The certificate is about the true global equilibrium, not only the one the solver found.

5claims, 1 at T4 and 4 at T312 / 23pycalphad parity items done (C0 complete, C1 half)29 / 29pycalphad equilibria inside the Lean intervals

Status of mini-CALPHAD →

The trust ledger

Every claim the project makes is registered with its tier, its evidence and the assumptions it depends on. Every line of a run report cites one of these claims. The tiers are defined on the programme page; a claim is only ever marked at the tier it has actually reached.

T4 end to end · 28 T3 machine proof · 95 T2 model-checked · 2 T0 tested · 1 target not yet reached · 6

mini-DFT

foundations · energy · free energy · smearing · k-points · truncation · density · bands · LDA

102

mini-FEM

Poisson · beams · load Taylor models

mini-MD

conservation · Verlet structure · tube theorem · checker

mini-CALPHAD

mixing bound · equilibrium · existence · magnetism · checker

The T4 claims are the soundness theorems of the certificate checkers (which run in exact rational arithmetic, so no floating point is involved) and the proof that the trusted C kernel has no run-time errors. Six claims are below target: five in mini-DFT (listed on the DFT page) and, in mini-MD, the existence of solutions of Newton’s equations.

How a result earns its guarantee

The solver is never trusted. It proposes; a proved checker disposes. This is what lets us use LAPACK and fast floating-point code while still stating every output as a theorem. The same four steps run in every domain.

Untrusted · T0

Solver

A C driver runs the SCF loop, the FEM assembly, the Verlet integrator or the equilibrium search, and writes a certificate.

Data

Certificate

Floating-point numbers read as the exact binary rationals they are. Nothing in it is assumed to be correct.

Proved · Lean

Checker

Re-checks everything in exact rational arithmetic. Its soundness is a Lean theorem; a wrong certificate can only fail or widen the interval.

Guaranteed

Rigorous statement

An interval that provably contains the true quantity: the continuous FEM solution, the true MD trajectory, the global CALPHAD equilibrium.

Alongside, the DFT SCF controller is a TLA+ specification checked with TLC (it can report “converged” only if the residual is small, the gap is open and the certificate passes), and every run can emit a trace that is replayed against that specification.

Goals and roadmap phases

G1 — mini-DFT reaches DFTK parity set 29 Sep 2026

6 of 46 items done and 4 more agree with DFTK; LDA exchange now has SCF-solution certificates at the Γ point with MP/MV smearing. 1D first, then d dimensions. Item-by-item status →

G2 — certified finite elements against scikit-fem set 30 Sep 2026

11 of 26 items done; F0 (1D Poisson) complete, F1 (1D extensions) under way. Item-by-item status →

G3 — certified CALPHAD against pycalphad set 1 Oct 2026

12 of 23 items done; C0 (binary point equilibrium) complete, and in C1 certified phase diagrams, the Inden–Hillert–Jarl magnetic model, driving forces and sharp chemical potentials. Next: interstitial solutions and invariant reactions. Item-by-item status →

PHASE 0Minimal DFTIn progress

Trust ledger, Lean certificate checkers, trust reports and trace validation are in place; all four benchmark groups pass, including the DFTK cross-check.

Remainingliterature checks for continuum well-posedness, the a priori plane-wave estimate and linear-mixing convergence (target T1); the Lean–Rocq interface claim; a code-level proof of the interval arithmetic (now T3, target T4).
PHASE 1DFT extensionsPartly ahead

k-point sampling is implemented and certified; the thread-parallel k-point protocol is model-checked and runs are bitwise identical across thread counts. Beyond the original plan: finite-temperature occupations with free-energy, entropy and energy certificates, Anderson mixing, non-self-consistent bands and DOS, and the truncation-error certificate.

LDASlater exchange certified at the Γ point with MP/MV smearing; PW92 correlation, other smearings and k-points agree with DFTK without certificates yet.

Not startedMPI parallelism, 3D plane waves and pseudopotentials.
PHASE 2MD and FEMExit criteria met

Both minimal versions print trust reports. mini-FEM: 1D Poisson (P1) and beams (cubic Hermite), certified against the true solution. mini-MD v0 (1 Oct 2026): a 1D Lennard-Jones chain with velocity Verlet, certified against the true trajectory. Céa’s lemma (FEM-D03) and Verlet symplecticity (MD-D03) are both at T3.

Not startedthe TLA+ modules for halo exchange, atom migration, parallel assembly and checkpointing; periodic boxes and thermostats for MD.
PHASE 3Trusted kernelsNot started

Starting point: the interval-arithmetic kernel, whose correctness is proved against a line-by-line model (T3) and whose absence of run-time errors is proved on the C code (T4).
PHASE 4BenchmarkingNot started

Δ-gauge, NVE drift and manufactured-solution studies with published trust ledgers.

CALPHAD is not one of the charter’s original phases; it was added as goal G3 on 1 October 2026 and follows the same completion standard as G1 and G2.

What is trusted without proof

Every guarantee in every domain is conditional on this small, explicit base.

Lean 4	The kernel that checks every proof; Mathlib, with only the three standard axioms
Lean compiler	Compiles the checkers into executables, together with their input parsing and decimal output (lower bounds rounded down, upper bounds up)
TLC	The TLA+ model checker
Frama-C / WP	With Why3, Alt-Ergo and Z3, for the run-time safety of the C kernel
C compiler	Unverified for now; CompCert is an option for the trusted kernel
IEEE 754	Only that round-to-nearest returns the nearest double; no error-size property is relied on

Each domain also has its own modelling conventions — for example that the certified problem uses the exact rationals written in the certificate, or that the TDB database is translated correctly — named on its page where they apply.

The C drivers that write those problems are untrusted, but they are kept honest. Their reports are checked line by line against the checkers’ own output. Their thread protocol is replayed against its TLA+ specification. They are fuzzed under AddressSanitizer and UBSan, and they reject any input they cannot write into a certificate exactly. All of this runs in make verify-all. The largest remaining gap is that the checkers neither recompute nor echo the problem data in a certificate.