A scientific program finishes, its residual falls below the tolerance, and a number appears on the screen. What have we actually learned? We may know that an iteration stopped. We may even know that another program gives the same answer. To turn that number into a claim about a material, a molecule, or a structure, however, we need a much longer chain of reasoning. The Formal in Silico programme makes this chain explicit through three kinds of correctness: physical, mathematical, and software correctness. I find the distinction useful because it changes both how we establish trust and what we can learn when a calculation disagrees with reality.
IOne number, three questions
Consider a simulation predicting a semiconductor band gap. Three questions sit behind its output. Does the physical model describe the observable being measured? Have we solved that model accurately enough? Does the actual program implement the intended calculation?
| Correctness | Question | Evidence |
|---|---|---|
| Physical | Does the model describe reality in the claimed range? | Independent observations, documented conditions, and measurement uncertainty |
| Mathematical | Are the model equations solved with controlled error? | Theorems about solutions, discretisation, and iteration |
| Software | Does execution faithfully realise the algorithm? | Specifications, implementation proofs, and certified arithmetic |
These questions cannot substitute for one another. Agreement with experiment can conceal compensating errors. Agreement between programs can reflect a shared approximation. A proof that code implements an algorithm says nothing by itself about whether the underlying model describes nature.
IIPhysical correctness: the equations face the world
A physical model makes choices before any solver starts. Electronic-structure calculations choose a functional and pseudopotentials; molecular dynamics chooses a force field; continuum mechanics chooses a constitutive law and boundary conditions. Those choices determine what world the computation describes.
Solving the resulting equations to more decimal places cannot establish that they describe the world we inhabit. The programme uses the band-gap problem to illustrate this distinction: a carefully converged Kohn–Sham calculation can still disagree with a measured gap. Both the approximation in the model and the relationship between the calculated quantity and the measured observable require scrutiny.
Physical correctness is therefore an empirical claim with a stated scope. Validation needs traceable measurements, their conditions and uncertainties, and a clear account of any corrections. Data used to fit a model should be kept separate from data used to validate it. Fixing the comparison protocol beforehand also makes disagreement a result we can report, rather than a reason to quietly adjust the test. These are central requirements of the programme’s physical validation layer.
A model earns support for particular observables and conditions. Physical correctness remains open to revision by new evidence.
IIIMathematical correctness: convergence needs a destination
Once a model is fixed, we still have to connect a finite calculation to its equations. A differential equation lives in a continuous space; a computer uses a mesh, a basis cutoff, and finitely many iterations. Each transition creates an obligation.
Does a solution exist? Is it unique, or are several solutions possible? How far is the discrete solution from the continuous one? How does a stopping tolerance bound the error in the quantity we care about? A small residual becomes informative only through a theorem connecting it to solution error, with the relevant stability assumptions.
The distinction becomes especially important in nonlinear problems. A self-consistent iteration can converge to a stationary state without establishing that it is the global energy minimum. A certificate for a unique solution near one candidate must say that it is local. It cannot silently become a certificate for the ground state.
Lean can check proofs of these statements against formal definitions. The guarantee follows the theorem’s assumptions and conclusion: a result about a finite basis remains a result about that finite basis until a further bound connects it to the continuous problem. Recording that boundary is part of mathematical correctness.
IVSoftware correctness: the theorem must reach execution
A mathematical algorithm does not send MPI messages, migrate atoms between processes, or recover a checkpoint. Its implementation does. An atom duplicated during migration changes the simulated system even when every local force calculation is accurate.
The programme assigns different tools to different obligations. TLA+ describes concurrent protocols and their invariants. Frama-C addresses properties of selected C kernels. Proved checkers validate numerical certificates. A refinement argument connects an implementation specification to the abstract algorithm whose mathematics has been analysed.
The scope of the evidence matters. Model checking can exhaust the behaviours of a specified finite instance; that alone is not a proof for every process count. Checking an execution trace establishes something about the recorded run. A general refinement theorem supports a broader claim, under its stated assumptions.
Arithmetic belongs in this chain too. Floating-point addition is not associative, so parallel reductions can change results when their order changes. Exact rational arithmetic or outward-rounded interval arithmetic can support rigorous enclosures. Reproducibility is useful evidence about execution, while an error bound explains how the result relates to the intended mathematical quantity.
VSeparating errors makes disagreement informative
For comparable observables under matched conditions, the discrepancy between observation and computation can be written schematically as:
observation − computed value
= measurement error
+ model error
+ discretisation error
+ iterative error
+ arithmetic errorThis accounting presupposes that execution implements the specified algorithm. A program that loses an atom may violate that premise altogether. Each numerical term also needs a bound for the observable being compared, not merely for an unrelated internal residual.
Here is an illustrative example, not a reported project result. Suppose a certificate encloses a model’s exact prediction in [1.095, 1.105] eV, including the relevant discretisation, iteration, and arithmetic errors. Suppose an experiment reports 1.170 eV with statistical uncertainty ±0.010 eV. The difference between the experimental central value and the model prediction is then rigorously enclosed in [0.065, 0.075] eV. The experimental uncertainty must still be reported separately, with its statistical meaning.
With matched conditions and documented corrections, this separates numerical uncertainty from the remaining evidence about model discrepancy. If the certificate covers only the discrete problem, however, the discretisation error is still unresolved. We cannot attribute the entire discrepancy to the physical model.
Bounding computational error makes a disagreement with experiment more scientifically useful. It tells us which explanations remain possible.
VIVerify the checker, and expose its assumptions
Proving every line of a large scientific solver is a formidable task. The programme takes another route: let a complex solver propose a result and a certificate, then have a smaller, proved checker establish precisely what follows.
The solver can be replaced, optimised, or assisted by AI. Its proposal earns a guarantee only after the checker accepts it under a soundness theorem. This concentrates verification effort on a smaller component, while preserving flexibility in the expensive search for a solution.
The guarantee still has dependencies. Formal models, compiler and runtime behaviour, hardware assumptions, and the correspondence between statements in different proof tools must be accounted for. The programme’s toolchain decisions explicitly acknowledge such connections and remaining assumptions.
A trust ledger makes these dependencies inspectable. It records the claim, its evidence, its assumptions, and its status. The programme distinguishes mathematical and software tiers T0–T4 from physical validation grades V0–V3. This lets a strong proof of a computed interval coexist honestly with limited experimental validation. The framework defines the intended standard; individual claims still need to be read at their actual scope and status.
VIIA scientific result should carry its evidence
For AI-assisted science, this architecture suggests a useful division of work. AI can help generate candidate structures, implementations, and proof attempts. Acceptance depends on the appropriate evidence: a checked proof for a mathematical claim, a verified certificate for a numerical enclosure, and independent observations for a claim about reality.
A calculation would then deliver more than a number. It would identify the model and conditions, state which quantity was certified and with what error, name the implementation guarantees, and link to the observations against which the model was tested. It would also expose the assumptions and gaps that remain.
The three kinds of correctness let us ask a more precise question of every simulation: what has been established, by which evidence, and within what limits? When the answer is explicit, agreement becomes easier to trust, and disagreement becomes a better guide to what we should investigate next.
Source and preparationBased on the Formal in Silico programme, consulted on 11 October 2026. This essay develops its central framework; it is not a claim that the full programme has been completed. The numerical example is illustrative. AI assisted with drafting and preparing the English and Chinese versions.