For weeks now every linear static analysis in Stabileo has gone through a certificate that, when it is obtained, gives a machine-checked bound on the error with which the system of equations K·u = f was solved. But the engine assembles that system itself. If the assembly had a mistake, a wrong sign in a transformation, a missing Timoshenko term, a wrong fixed-end force, the certificate would prove with full rigour that the wrong system was solved correctly.
End-to-end certificates close that gap for frames and trusses, in 2D and 3D: the result is checked against the model as written, not against the matrices the engine assembled.
A second, independent assembly
A separately written checker rebuilds the stiffness and the loads from the model data, without calling any of the engine’s element or assembly functions. It uses its own formulas and its own numbering of the degrees of freedom:
- each member’s bending from the cantilever flexibility, inverted, and the other end by equilibrium, with Timoshenko shear deformation;
- hinges by static condensation, one released rotation at a time;
- member loads as the work on the exact deflected shapes of the unloaded member, with the integrals in closed form;
- local axes, inclined supports, springs, rigid links, diaphragms and multipoint constraints, derived from the model’s conventions.
Everything is computed in interval arithmetic, sines and cosines included, with rigorous bounds: every model input enters as the decimal it was typed as, enclosed in an interval. When a decision depends on a threshold the interval cannot settle, the checker refuses instead of guessing.
What the certificate states
With that exact stiffness, the checker proves that the model has a unique solution and bounds the distance between the displacements the engine returned and that solution, over every degree of freedom the model determines. The engine’s matrices play no part in that statement. They are compared separately: they must agree with the rebuilt ones to one part in 10¹⁰, and the displacements must satisfy the model’s supports and constraints to one part in 10⁹. If they do not, the result is reported as not checked end to end, with the reason.
The theorem behind the bound is proved in Lean. In the app, the results panel shows the line “Checked end to end” with the bound on the displacement error, or the reason it could not be checked.
What it found
| Set | Models | Certified |
|---|---|---|
| 2D test models | 82 | 82 |
| 3D test models | 32 | 32 |
| Random 2D frames | 200 | 200 |
| Random 3D frames | 150 | 150 |
Every test model and hundreds of randomly generated frames agree and are certified, and assembly bugs planted on purpose in the engine make the check fail. It also found real problems:
- a 3D diaphragm in the XZ plane tied the nodes with the rotation of the wrong sign;
- in 2D, a moment on a node where every member is hinged was absorbed by an artificial spring, and the certificate of the assembled system passed it although the model has no solution;
- a rigid link from such a node hid a real mechanism.
The first two are fixed: the diaphragm follows rigid-body rotation, and that moment is refused before the solve. And when the engine changed what a diaphragm means, so that the whole floor rotates as one body, the checker passed nothing false: it stayed honest, with useless bounds, until its conventions were updated. That is exactly what an independent check is for.
What it leaves out
- Shells, solids, connectors, curved beams and warping torsion are not rebuilt yet: they are reported out of scope, never as checked.
- The checker’s formulas encode the model’s mechanics. They are written separately from the engine and compared with it, but they are not proved.
- The Rust implementation is not proved equivalent to the Lean algorithm, as for every certificate.
- A certificate says the result belongs to the model. It does not say the model represents the structure well: that remains the engineer’s work.