Formal in Silico

Domain · mini-MD v0 · status snapshot 1 October 2026

mini-MD

A one-dimensional Lennard-Jones chain integrated with velocity Verlet. The Lean checker bounds how far the computed trajectory is from the true solution of Newton’s equations — for every step, and from the initial state over about one vibration period — and computes the conserved quantities exactly. Built on 1 October 2026 as the charter’s phase-2 MD version and cross-checked against ASE 3.29.

14claims in the trust ledger: 4 at T4, 9 at T3, 1 open
0.99true local error ÷ certified local bound: the bound is almost exact
≤ 5×10⁻¹⁴difference from ASE in positions, momenta and energy
≈ 1 periodcovered by the global bound from the initial state (t = 0.5 for 8 atoms)

01

The problem

SystemN ≥ 2 atoms on a line, in order, with masses mi > 0. Free boundaries, every pair interacts, and the Lennard-Jones potential φ(r) = 4ε((σ/r)¹² − (σ/r)⁶) is not truncated.
Equationsq′ = p/m, p′ = F(q). A “true solution” is any solution of these equations; every classical solution qualifies.
IntegratorVelocity Verlet with step h: a half kick, a drift, a half kick. The driver computes it in double precision with no fused multiply-add.
InputParameters and initial state are the exact rationals written in the certificate — the doubles the driver actually used. Their difference from the decimal command line is outside the certificate (assumption A-MD-01).

02

What a certified run reports

An 8-atom chain, 600 steps of h = 0.001, initial temperature 0.01. The driver writes the trajectory as a certificate and the Lean checker certify-md re-checks it in exact rational arithmetic; this is the end of its report.

build/mini-md --N 8 --steps 600 --dt 0.001 --T0 0.01 --certify run.cert --verify
…
Lean  MD_OK 8 600
Lean  E0 -7.186568898605097 -7.186568898605096
Lean  ENERGY_DRIFT 0.00000046826354893195
Lean  MOMENTUM_DRIFT 0.00000000000000029057
Lean  VERLET_RES 0.00000000000000044369
Lean  LOCAL_OK 0.00000000279045942382 0.00000004228626446212
Lean  TRUE_OK 500 0.500000000000 0.00099933951185418332 0.01514386287974667751
Lean  TRUE_HORIZON 500 0.500000000000
Lean  KMAX 19.447984
Lean  EPSMAX 0.00000004460799189706
LineWhat the Lean theorem guaranteesClaim
LOCAL_OK dq dpFor every step k: any true solution started from the computed state (Qk, Pk) is within dq in position and dp in momentum of (Qk+1, Pk+1) one step later. The computed trajectory is a dq-pseudo-orbit of the true flow.MD-B01
TRUE_OK j t dq dpAny true solution from the initial state is within dq / dp of the computed state at time tj.MD-B02
TRUE_HORIZON H tThe global bound covers [0, t]; there the atoms stay ordered and the true energy is exactly E₀.MD-B02, C01
E0 lo hiThe initial energy H(Q₀, P₀), computed exactly and rounded outward.MD-B03
ENERGY_DRIFT, MOMENTUM_DRIFTThe largest change of energy and of total momentum along the computed trajectory, computed exactly.MD-B03
VERLET_RES dThe data satisfy both Verlet equations up to d: the trajectory really is Verlet’s, apart from rounding.MD-B04
KMAX, EPSMAXDiagnostics (largest Lipschitz constant and defect), not claims.—

In this run the computed energy drifts by 4.7×10⁻⁷ while the true energy stays exactly E₀ up to t = 0.5. The drift is Verlet’s own O(h²) energy error — now a certified number rather than an estimate.

03

How the certificate works

For each step the checker builds a curve that is provably close to a solution of Newton’s equations, then uses a tube theorem to conclude that every solution stays close to it. Everything is exact rational arithmetic; the driver’s floating-point numbers are only data.

  1. 1

    Taylor polynomial of the true flow

    At each data point the checker computes the true solution’s first four time derivatives exactly and forms a quartic for each atom. Interpolating the Verlet points instead would leave an O(h) defect, because Verlet’s local error is O(h³).

  2. 2

    Atoms stay apart

    Every pair of atoms keeps a positive distance over the step, by interval bounds on the polynomials; otherwise the checker reports MD_FAIL.

  3. 3

    Defect

    How far the quartic is from solving Newton’s equation, D = m z″ − F(z), with the third derivative of the force enclosed in intervals (MD-A03).

  4. 4

    Lipschitz constant on a box

    The vector field is Lipschitz on the ρ-neighbourhood of the curve, with a constant from interval bounds on φ″ (MD-A02).

  5. 5

    Tube theorem

    If the Grönwall bound δeKt + (ε/K)(eKt − 1) stays below ρ, every solution stays in the box and obeys the bound. The proof argues by the first exit time, so nothing needs to be known in advance about where the solution goes (MD-A01, A04).

Why the local bound is almost exact: its main term is the jump between the polynomial and the next data point, which is Verlet’s own local error, O(h³); the defect term is O(h⁴). Across three systems the true local error is 0.99 of the bound.

04

The global bound and its horizon

A pointwise bound on a many-body Lennard-Jones trajectory has to grow exponentially: the dynamics are chaotic, and nearby trajectories separate like eKt. The certified bound starts at the true error (ratio 0.91 after 10 steps) and grows at rate K ≈ 19 until it reaches the tube radius at t = 0.5, about one vibration period. After that the checker still certifies every step locally, but no longer the distance from the true trajectory of the initial state.

Distance from the true trajectory · 8 atoms, h = 0.001

Largest position error over the atoms, log scale. The certified bound is Lean’s TRUE_OK; the true error is measured against a high-accuracy reference solution (scipy DOP853, rtol 10⁻¹³), which is for comparison only and not itself rigorous.

Show the numbers

This is a property of the problem, not of the proof technique: long-time pointwise error bounds for chaotic dynamics do not exist. Long-time statements need a different form — shadowing of the pseudo-orbit, backward error analysis through Verlet’s modified Hamiltonian, or statistics of the trajectory — and are listed among the gaps.

05

Claims in the trust ledger

T4 end to end · 4 T3 machine proof · 9 target not yet reached · 1
ClaimStatementTier
MD-C01Energy conservation: a true solution keeps its energy while the atoms stay orderedT3
MD-C02Momentum conservation: forces sum to zero, so total momentum is constantT3
MD-C03Existence: Newton’s equations have a solution on [0, T]not reached
MD-D01Velocity Verlet is time-reversibleT3
MD-D02Velocity Verlet preserves total momentumT3
MD-D03Velocity Verlet is symplectic, in particular for the Lennard-Jones chainT3
MD-A01Tube theorem: a Grönwall bound below the tube radius confines every solutionT3
MD-A02Lipschitz constant of the scaled vector field on a boxT3
MD-A03Defect bound for quartic approximate trajectoriesT3
MD-A04One-step error boundT3
MD-B01Checker soundness: local error of every stepT4
MD-B02Checker soundness: global error from the initial state; ordering and exact energy on the horizonT4
MD-B03Checker soundness: initial energy, energy drift and momentum drift, computed exactlyT4
MD-B04Checker soundness: the data satisfy the Verlet equations up to the reported residualT4

Verlet symplecticity at T3 (MD-D03) is half of the charter’s phase-2 exit criterion; the other half, Céa’s lemma, is on the FEM page.

06

Cross-checks and supporting evidence

  • ASE 3.29 (LennardJones + VelocityVerlet), three chains of 5, 8 and 12 atoms, up to 2000 steps: positions / momenta / energy≤ 3.6×10⁻¹⁵ / 5.0×10⁻¹⁴ / 3.2×10⁻¹⁴
  • Order of the global error and of the energy drift, against a DOP853 reference solution2.00
  • Total momentum along the computed trajectoryconserved to 3×10⁻¹⁶
  • True error ÷ Lean bound, local and global, in all three systems≤ 0.99
  • Global horizon for 8 atoms: T₀ = 0.01, h = 0.001 / T₀ = 0.1, h = 0.002 / T₀ = 0.001, ρ = 10⁻⁴500 / 122 / all 800 steps
  • One tampered position in the certificateonly the residual and local bound grow
  • Negative mass, overlapping atoms, a tube radius smaller than one step’s defectMD_FAIL
  • Checking time, 8 atoms, 1000 steps (grows as N²)≈ 50 s
  • Driver under AddressSanitizer and UBSanclean
  • Report validation: every Lean line 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 10 000 mutated inputs), after hardening its input parsingno memory errors, undefined behaviour or crashes

07

Open gaps

  • Existence of the true solutionThe certificate holds for every solution, and within the tube the solution is unique, but existence is not yet machine-proved (MD-C03). Picard–Lindelöf on the truncated field, or continuation through energy conservation, would close it.
  • Long-time pointwise errorInherent to chaos, as above. A logarithmic norm in the energy norm or Lohner-type linearised propagation would lengthen the horizon; truly long-time claims need shadowing, modified-Hamiltonian arguments or statistics.
  • StatisticsTemperature, radial distribution functions and autocorrelations are exact functions of the computed states, like the energy, but are not implemented yet.
  • Periodic boxes, cutoffs, thermostats, constraints, 2D and 3D, parallelismNot started. A cutoff makes the force discontinuous, so the tube theorem needs a piecewise-smooth version; the parallel protocols (atom migration, halo exchange) are to be specified in TLA+.
  • Checking timeAbout 50 ms per step for 8 atoms, mostly exact rational evaluation of φ and its derivatives; interval arithmetic would be much faster.
  • The driver itselfUntrusted (T0); every result passes through the checker. Since 1 October it rejects non-finite or malformed parameters and stops if the integration produces a non-finite state; the initial state and the Lennard-Jones parameters in the certificate are still not echoed by the checker beyond E0. Phase 3 plans to bring one Verlet step to T4.