01
The problems
| Poisson | −u″ = f on (0, L) with Dirichlet, Neumann or Robin conditions at each end (not Neumann at both); P1 linear elements on any mesh with rational nodes. |
| Beam | u⁗ = f on (0, L) with clamped, pinned, free or sliding ends in any combination; cubic Hermite elements carrying nodal values and slopes. |
| Loads | Sums and products of polynomials, eλx, sin and cos (also of qπx); the checker re-encloses them with Taylor models and never trusts the solver’s quadrature. |
| Why 1D | Green’s functions and classical solutions avoid Sobolev spaces, so every statement can be about the true solution; 2D will need an H¹ model in Lean. |
02
Claims in the trust ledger
T4 end to end · 3
T3 machine proof · 8
| Claim | Statement | Tier |
|---|---|---|
| FEM-C01 | Poisson: the Green representation is a classical solution, and the only one | T3 |
| FEM-D01 | P1 nodal exactness and the discrete Green representation | T3 |
| FEM-D02 | Pointwise error inside an element: Mh²/8 plus the nodal error | T3 |
| FEM-D03 | Céa’s lemma (abstract setting, in preparation for 2D) | T3 |
| FEM-D04 | Discrete maximum principle | T3 |
| FEM-C02 | Beam: the classical solution exists and is unique | T3 |
| FEM-D05 | Discrete stability of Hermite elements (no maximum principle needed) | T3 |
| FEM-D06 | Hermite nodal exactness and the h⁴/384 interpolation bound | T3 |
| FEM-B02 | Taylor models of the load are sound | T4 |
| FEM-B01 | P1 checker soundness: intervals for u(xi) and a bound on max |u − uh| | T4 |
| FEM-B03 | Beam checker soundness: intervals for values and slopes, and the max-error bound | T4 |
03
Goal G2 — certified finite elements against scikit-fem
Reference: scikit-fem 12.0.2 on the same discrete problem. The standard is the same as G1, with one addition: wherever possible, the certificate is about the true solution of the continuous problem, not only the discrete one. In 1D this avoids Sobolev spaces by working with Green’s functions and classical solutions; 2D will need an H¹ model in Lean.
F0
1D Poisson, P1 elements
7 / 7F1
1D extensions
4 / 9F2
2D triangular meshes
0 / 5F3
More physics, 3D
0 / 5F0 · 1D Poisson with P1 elements — complete
| Feature | Status | What is certified |
|---|---|---|
| 1D meshes: uniform, graded, arbitrary rational nodes | Done | The checker verifies the mesh is well ordered |
| P1 elements, stiffness and load assembly | Done | The checker re-encloses the load with Taylor models and does not trust the solver’s quadrature |
| Non-homogeneous Dirichlet boundaries | Done | Covered by the checker’s soundness theorem |
| Polynomial right-hand sides | Done | Integrated exactly |
| Linear solve | Done | The solver is untrusted; its nodal error is bounded exactly |
| True-solution nodal values and pointwise error | Done | Existence and uniqueness of the classical solution, nodal exactness, the h²/8 interpolation bound and the discrete maximum principle are all proved |
| Céa’s lemma (abstract setting) | Done | Proved, in preparation for 2D |
F1 · 1D extensions
| Feature | Status | What is certified |
|---|---|---|
| Neumann and Robin boundaries | Done | All theory proved for general boundary conditions; Neumann at both ends is excluded |
| Non-polynomial right-hand sides | Done | Sums and products of polynomials, exponentials, sines and cosines, via Taylor models with proved remainders; nodal intervals about 10−15 wide |
| Hermite beam elements (fourth-order problem) | Done | Clamped, pinned, free and sliding ends in any combination; rigorous intervals for both nodal values and slopes; the h⁴/384 interpolation bound is proved |
| Adaptive refinement (1D) | Done | Elements are marked by their proved error bounds, not by an estimator; the final mesh is certified |
| Variable coefficients | Not started | |
| P2 and higher-order Lagrange elements | Not started | |
| Eigenvalue problem | Not started | Can reuse the DFT inertia argument |
| Energy-norm error | Not started | |
| Example-by-example comparison with scikit-fem’s 1D gallery | Not started |
Planned: F2–F3 (10 items, none started)
F2 · 2D triangular meshes
- Triangular meshes with checker-verified shape regularity (the Sleipner lesson)
- P1 and P2 triangles
- A Lean model of H¹0
- Guaranteed-upper-bound a posteriori estimates (equilibrated fluxes)
- Quadrilateral elements
F3 · more physics and 3D
- Linear elasticity (Korn’s inequality)
- Stokes and mixed elements (inf-sup)
- Adaptive refinement in 2D
- Tetrahedral and hexahedral meshes
- Parallel assembly, specified in TLA+
04
What a certified run reports today
Rigorous statements about the true solution
- an interval for u(xi) at every node
- for beams, also an interval for the slope u′(xi)
- the exact error of the solver’s own nodal values
- a bound on max |u − uh| over the whole interval, and per element
- an adaptively refined mesh that meets a requested tolerance, with the tolerance certified on the final mesh
05
Cross-checks and supporting evidence
- 11 Poisson and 6 beam cases — Lean nodal intervals contain the reference solutionwidth ≤ 3×10⁻¹⁵
- scikit-fem nodal values against mini-FEM (Poisson / beam)≤ 3×10⁻¹³ / 4×10⁻¹²
- proved max-error bound relative to the sampled actual error0.85 – 1.00
- tampered nodal valuesonly widen the error bound
- 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 14 000 mutated inputs), after hardening its input parsingno memory errors, undefined behaviour or crashes
06
Open gaps
- Other load functionsLogarithms, rational and piecewise functions need their own Taylor models; today only polynomials, exponentials, sines and cosines.
- Neumann at both endsThe solution is defined only up to a constant; a compatibility condition and a normalisation are needed. Both driver and checker reject it.
- Checking time for transcendental loadsAbout 13 ms per element, mostly in exact rational series at element midpoints; an interval series with term-wise rounding would be faster.
- Variable beam stiffness and elastic supportsOnly EI = 1; the checker accepts any 4×4 boundary matrix, but the driver writes only the four standard end conditions.
- The driver itselfUntrusted (T0) with no Frama-C proof; every result passes through the checker. Since 1 October it parses numbers strictly and rejects inputs it cannot write exactly (fuzzing had found a right-hand side truncated at 4 KB and NaN parameters written as zero); the boundary data and load in the certificate are still not echoed by the checker. Phase 3 plans to bring element-stiffness assembly to T4.