01
The model
| System | Binary A–B at fixed temperature and pressure; composition x = xB ∈ [0, 1]. Each phase has a Gibbs energy G(x) per mole of atoms, as pycalphad’s GM. |
| Solutions | One mixing sublattice, the others vacancies only: ideal mixing RT(x log x + (1 − x) log(1 − x)) plus a Redlich–Kister excess x(1 − x) Σ Lk(1 − 2x)k. |
| Magnetism | Optional Inden–Hillert–Jarl term RT log(1 + β(x)) g(Tc(x)/T), with Tc and β Redlich–Kister sums of the TC and BMAGN parameters, divided by the antiferromagnetic factor where negative. The two branches of g meet at T = Tc with equal value and slope — an identity Lean proves for every structure factor p. |
| Compounds | Stoichiometric: they exist at one exact composition, such as 2/3. |
| Parameters | Piecewise SGTE expressions in T. The driver picks the range and expands function references; each term is c·Tn or c·Tn log T, with c the exact product of the TDB’s decimal strings. |
| Not yet | The ordered phase of an order–disorder pair (the disordered phase is computed as in pycalphad), interstitial phases, several mixing sublattices, more than two components. Such phases are skipped and listed in the report; the conclusions hold for the phases taken into account. |
The certificate certifies the exact model written in it. Translating the TDB file into that model is done by the untrusted driver (assumption A-CAL-01); the benchmark checks every phase’s G(x) against pycalphad to a relative 5×10⁻¹² (pycalphad adds 10⁻⁹ to Tc to avoid a singularity; the certificate uses the exact continuous form).
02
What is certified
The equilibrium Gibbs energy G*(x₀) is the infimum of the total Gibbs energy over all feasible configurations: any finite collection of phases, compositions and amounts with the right overall composition. Geometrically it is the lower convex hull of all phase curves at x₀.
An equilibrium is a feasible configuration together with a common tangent ℓ(y) = μA(1 − y) + μBy that lies below every phase and touches the configuration; μA and μB are the chemical potentials. Lean proves that equilibria minimise the total Gibbs energy (CAL-C02) and that one always exists (CAL-C03).
A Gibbs-energy minimiser can stop in a local minimum, miss a phase or miss a miscibility gap. The checker’s statements are about every feasible configuration and every equilibrium, so such a mistake can only make the check fail or widen the intervals — never produce a wrong statement.
| Line | What the Lean theorem guarantees |
|---|---|
| G_OK lo hi | G*(x₀) ∈ [lo, hi]: every feasible configuration has total Gibbs energy ≥ lo, and the certificate’s configuration has ≤ hi. |
| MU_OK A|B lo hi | The chemical potentials of any equilibrium lie in these intervals. |
| WINDOW phase a b | In any equilibrium, every composition of this phase lies in one of its windows. |
| ABSENT phase | The phase appears in no equilibrium. |
| DF_OK phase lo hi | The driving force maxx (ℓ*(x) − G(x)) of the phase — pycalphad’s DF, negative for metastable phases, 0 for stable ones — for the tangent ℓ* of any equilibrium. It is the global maximum over all compositions. |
| EXISTS | An equilibrium exists, so the statements above are not vacuous. |
| TANGENT, EPS, KAPPA, FRAC | Diagnostics: whose tangent was used (in single-phase regions the checker computes its own), how far below the phases it lies, the tangent error bound used for the windows, and the certificate’s own configuration. |
03
Worked example: a miscibility gap in Al–Zn
Al–Zn at 600 K and x(Zn) = 0.3, with the Mey (1993) database shipped with pycalphad. At this temperature the fcc solution splits in two: the equilibrium is two fcc phases with about 22% and 49% zinc. The checker proves that LIQUID and HCP_A3 appear in no equilibrium, confines the fcc compositions of every equilibrium to two windows at most 3×10⁻⁷ wide, pins G* and both chemical potentials to the last printed digit, 10⁻⁹ J/mol, and gives each phase’s driving force to the same precision. The run, check included, takes about one second.
…
Lean G_OK -22985.126672267 -22985.126672266
Lean TANGENT cert
Lean EPS -0.000000000002425
Lean FRAC FCC_A1 0.220126286673 0.705704921583
Lean FRAC FCC_A1 0.491533181263 0.294295078416
Lean MU_OK A -20590.725231961 -20590.725231960
Lean MU_OK B -28572.063366314 -28572.063366313
Lean KAPPA 0.000000000022
Lean ABSENT LIQUID
Lean WINDOW FCC_A1 0.220126163802 0.220126409545
Lean WINDOW FCC_A1 0.491533032729 0.491533329798
Lean ABSENT HCP_A3
Lean DF_OK LIQUID -896.512026734 -896.512026733
Lean DF_OK FCC_A1 -0.000000001 0.000000001
Lean DF_OK HCP_A3 -379.321840947 -379.321840946
Lean EXISTS
Al–Zn at 600 K: the fcc phase against the certified tangent
Gibbs energy of FCC_A1 minus the common tangent ℓ, in J/mol. The curve touches ℓ twice — a miscibility gap — and the dots mark the two Lean windows, each at most 3×10⁻⁷ wide. LIQUID and HCP_A3 stay 896.5 and 379.3 J/mol above ℓ at their closest (their certified driving forces), far off this scale. The curve is computed with pycalphad for illustration; the tangent and windows come from the Lean report.
Show the numbers
04
Magnetism: the Cr–Fe miscibility gap
In Cr–Fe the bcc solution is ferromagnetic on the iron side (Tc = 1043 K, β = 2.22) and antiferromagnetic on the chromium side, where TC and BMAGN are negative and are divided by the antiferromagnetic factor. The magnetic energy is what splits the bcc phase into a Cr-rich and an Fe-rich solution below about 860 K. At 600 K and x(Fe) = 0.5 the checker certifies the two compositions to windows 10⁻⁷ wide in about two seconds.
The magnetic term is not a polynomial and has no convenient second derivative, so the checker bounds it on each interval with secant slopes instead of derivatives: log(1 + β), the antiferromagnetic convention, the powers tn and t−n, and both branches of the Inden–Hillert–Jarl function each have rational bounds on the slope between any two points of an interval, proved in Lean (CAL-C04). The resulting lower bound is exact up to a term of the order of the interval width squared, which is enough for the branch and bound to converge.
… 相： BCC_A2（磁性）
Lean G_OK -19793.346508744 -19793.346508743
Lean MU_OK A -19642.803579468 -19642.803579467
Lean MU_OK B -19943.889438020 -19943.889438019
Lean WINDOW BCC_A2 0.432097736118 0.432097836657
Lean WINDOW BCC_A2 0.903631494701 0.903631563012
Lean DF_OK BCC_A2 -0.000000001 0.000000001
Lean EXISTS
Cr–Fe: certified boundaries of the magnetic miscibility gap
Composition x(Fe) of the two bcc solutions in equilibrium, from 400 K to 850 K in steps of 25 K. Each point is the centre of a Lean window, at most 2×10⁻⁶ wide, from one certificate per temperature (57 certificates in all with the single-phase regions). The two boundaries meet near 860 K, where the gap closes. pycalphad’s binplot draws the same curves.
Show the numbers
05
Phase diagrams
--map T1:T2:dT computes an isothermal section at each temperature of a grid: the driver walks the lower convex hull and splits [0, 1] into single-phase regions and common tangents, refines each tangent by Newton’s method, and writes one point-equilibrium certificate at the midpoint of every region. For a two-phase region the two windows of its certificate are the certified phase boundaries at that temperature, and every other phase is proved absent there.
Benchmark: Pb–Sn 300–600 K (43 regions), Al–Zn 400–900 K (35, including the fcc miscibility gap), Cu–Mg 600–1300 K (31), Cr–Fe 400–900 K (31) and Al–Fe 700–1700 K (63 regions, 34 common tangents, with the γ loop near pure iron). All 203 certificates pass, every boundary window is at most 2×10⁻⁶ wide, and pycalphad’s equilibrium gives the same phases and compositions at every certificate point. The certified boundary points lie on pycalphad’s binplot curves; in Al–Fe between 1300 and 1430 K binplot omits the Al2Fe region, which pycalphad’s own equilibrium and our certificates both show.
What is certified is each listed region at its midpoint. Whether the list of regions is complete — no two-phase region narrower than the driver’s grid spacing (5×10⁻⁴) missed — and what happens between grid temperatures is not; the benchmark cross-checks the region list against pycalphad on a composition grid.
06
How the checker works
Everything is exact rational arithmetic. The driver contributes only a candidate tangent, a candidate configuration, probe points and a point near each phase’s minimum.
- 1
Parameter intervals and the tangent
log T is enclosed by rational series bounds shared with mini-DFT; each solution phase becomes a rational polynomial plus the ideal mixing term (and the magnetic term), with a uniform rounding error. In single-phase regions the checker replaces the driver’s double-precision tangent by its own rational tangent at x₀ — soundness holds for any tangent, so this needs no new proof, only sharpens the result.
- 2
Branch and bound below every phase
On each interval, a lower bound for G − ℓ comes from exact Taylor coefficients of the polynomial, the proved quadratic bound on the mixing term (CAL-C01), the secant-slope bound on the magnetic term (CAL-C04) and the exact minimum of a quadratic. Each phase gets its own lower bound ei; their minimum e ≤ 0 bounds all phases from below.
- 3
Interval for G*
Every feasible configuration has total Gibbs energy ≥ ℓ(x₀) + e (CAL-C02); the certificate’s configuration, with amounts from the lever rule, gives the upper end.
- 4
Chemical potentials
Any equilibrium tangent passes through the G* interval at x₀ and stays below the phases at probe points on both sides; that pins its slope, hence μA and μB — to about 10⁻⁹ J/mol in two-phase regions and 10⁻⁸ to 10⁻⁷ J/mol in single-phase regions.
- 5
Driving forces
Any equilibrium tangent is within κ of the certificate’s on [0, 1], so min (Gi − ℓ*) ≥ ei − κ, and the driver’s point near the minimum gives the other end.
- 6
Composition windows
Phases present satisfy G − ℓ ≤ κ. A second branch-and-bound pass excludes every interval whose lower bound exceeds κ; what remains are the windows.
The bisection rule affects only speed and sharpness. Soundness depends only on two facts the proof checks: every excluded interval has a lower bound above the threshold, and the intervals cover [0, 1].
07
Claims in the trust ledger
| Claim | Statement | Tier |
|---|---|---|
| CAL-C01 | Quadratic lower bound on the ideal mixing term S(x) over any interval | T3 |
| CAL-C02 | Equilibria minimise the total Gibbs energy; every phase present touches the tangent; a lower bound on G − ℓ bounds every feasible configuration | T3 |
| CAL-C03 | An equilibrium exists for 0 < x₀ < 1 with at least one solution phase, magnetic phases included (their Gibbs energy is continuous) | T3 |
| CAL-C04 | Interval bounds on the Inden–Hillert–Jarl magnetic term from secant slopes: a polynomial lower bound with second-order error on any interval, and an upper bound at rational points | T3 |
| CAL-B01 | Checker soundness: the interval for G*, and for every equilibrium the chemical potentials, composition windows, absent phases and driving forces; existence | T4 |
08
Goal G3 — certified CALPHAD against pycalphad
Reference: pycalphad 0.11.1 on the same database and the same set of phases. Same completion standard as G1 and G2, and the certificate must speak about the true global equilibrium of the database model. Order: complete the binary case (C0–C1), where branch and bound runs over one composition variable; then multicomponent and sublattice models (C2), where it runs over products of simplices; then derived calculations (C3).
C0 · binary point equilibrium — complete
| Feature | pycalphad | Status | What is certified |
|---|---|---|---|
| TDB reading: functions, piecewise ranges, references, parameters | Database | Done | Outside the trust chain (A-CAL-01); every phase’s G(x) matches pycalphad’s calculate pointwise |
| Substitutional solutions: ideal mixing + Redlich–Kister | Model (GM) | Done | Quadratic mixing bound CAL-C01; checker CAL-B01 |
| Stoichiometric compounds | Model | Done | Composition is an exact fraction such as 2/3 |
| Point equilibrium: phases, compositions, amounts | equilibrium (Phase, X, NP) | Done | WINDOW and ABSENT for every equilibrium; the certificate’s amounts are exact by the lever rule |
| Equilibrium Gibbs energy | equilibrium (GM) | Done | G_OK: a global lower bound over every feasible configuration |
| Chemical potentials | equilibrium (MU) | Done | MU_OK, for every equilibrium |
| Miscibility gaps (two compositions of one phase) | equilibrium | Done | One window around each composition |
| Existence of an equilibrium | — | Done | CAL-C03: EXISTS, so “for every equilibrium” is never vacuous |
C1 · binary extensions — 4 of 8 done
| Feature | pycalphad | Status | What is certified |
|---|---|---|---|
| Binary phase diagrams on a T–x grid | binplot, map | Done | One certificate per region and temperature; boundaries from the windows of the common-tangent certificates. Completeness of the region list is not certified (see gaps) |
| Magnetic contribution (Inden–Hillert–Jarl) | Model (TC, BMAGN) | Done | CAL-C04 (secant-slope bounds) and CAL-C03 for magnetic phases; Cr–Fe and Al–Fe in the benchmark |
| Driving forces | DormantPhase(…).driving_force | Done | DF_OK for every equilibrium; the global maximum over compositions, where pycalphad finds a local one |
| Sharp chemical potentials in single-phase regions | equilibrium (MU) | Done | The checker’s own rational tangent: widths from about 10⁻⁴ down to 10⁻⁸–10⁻⁷ J/mol |
| Completeness of an isothermal section | — | Not started | |
| Invariant reaction temperatures (eutectic, peritectic) | map | Not started | |
| Thermodynamic properties H, S, Cp | calculate | Not started | |
| Interstitial solutions | Model | Not started |
Planned: C2–C3 (7 items, none started)
C2 · multicomponent and sublattice models
- Ternary and higher solutions (Muggianu extrapolation, ternary parameters)
- Several sublattices (compound energy formalism)
- Order–disorder
- Conditions on chemical potential or activity
C3 · further calculations
- Scheil solidification
- Parameter fitting (ESPEI): the fit stays untrusted, conclusions depend only on the final database
- Ionic liquid and quasichemical models
09
Cross-checks and supporting evidence
- Every phase’s G(x) at x = k/20 against pycalphad’s
calculaterelative ≤ 5×10⁻¹² - 29 equilibria in Al–Zn, Pb–Sn, Cu–Mg, Cr–Fe and Al–Fe against pycalphad’s
equilibrium: compositions / Gibbs energy< 10⁻⁶ / < 10⁻⁵ J/mol - pycalphad’s
GM,MUand phase compositionsinside the Lean intervals and windows - 141 driving forces: pycalphad’s
DormantPhasevalue inside the Lean interval, or, in 6 cases where pycalphad stops at a local optimum, pycalphad’s owncalculateat our point inside itall consistent - Phase diagrams: 203 certificates in five systems; pycalphad’s phases and compositions at every certificate pointall pass, windows ≤ 2×10⁻⁶
- Tampered certificatesfail, or still-correct conclusions
- Checking time per equilibrium; whole benchmark0.1 – 2.4 s; 218 s
- Driver under AddressSanitizer and UBSan, point equilibria and phase diagramsclean
- Report validation: every
Leanline in a report is the checker’s own output; a rejecting, crashing or missing checker makes the driver exit with an errorpass - Fuzzing of the driver under AddressSanitizer and UBSan (about 34 000 mutated inputs), after hardening its input parsingno memory errors, undefined behaviour or crashes
At Al–Fe 1000 K, x = 0.9, pycalphad’s multiphase equilibrium returns a GM 6×10⁻⁶ J/mol above its own calculate and its single-phase equilibrium at the same point — just outside the Lean interval. The certificate is right; the benchmark tolerance on pycalphad’s GM is 10⁻⁵ J/mol for this reason.
10
Open gaps
- From TDB file to certified modelChoosing temperature ranges, expanding function references and classifying phases is done by the driver, outside the trust chain (A-CAL-01). The benchmark compares the result with pycalphad. Fuzzing found inputs for which the driver wrote a certificate for a different model, which the checker then accepted:
3*T**1.5read as 3T + 0.5, coefficients truncated in fixed buffers, a phase dropped by overflow in exact site-ratio arithmetic, and command-line numbers such as0.25*2that the driver and the checker read differently. Since 1 October the driver rejects every input it cannot translate exactly; three of pycalphad’s test databases that it had silently misread are now read as pycalphad reads them, and four it cannot translate exactly are rejected. The checker still neither recomputes nor echoes the model. - Completeness of a phase diagramEach listed region is certified at its midpoint; that the list is complete, and the regions between the midpoints and between grid temperatures, are not. Planned: neighbouring certificates’ tangents bracket the equilibrium tangent at any composition in between.
- Order–disorder, interstitial, sublattice and multicomponent modelsNot yet defined in Lean. The driver skips such phases and lists them; the conclusions hold only for the phases included. Magnetic phases whose
TCorBMAGNdepends on log T are also skipped. - The driver itselfIts grid search and Newton iterations are untrusted (T0) and marked so in the report; every result passes through the checker.