A structural analysis program can give a wrong number with no visible sign. Over the last weeks we tested every part of Stabileo in several independent ways, found dozens of real defects, many of them unconservative, and fixed most of them. Each one is triaged and, if it may have affected results already in use, published as an advisory with what to do in the meantime; some are still being triaged. This post explains how we look for those defects, what the certificates that come with the results prove and, just as plainly, what lies outside any verification.
One engine
The solver is written in Rust and compiled to WebAssembly: it runs on the user’s own computer, with no installation and without sending the model to any server. It is the same code that runs in continuous integration. In October 2026 we removed the parallel TypeScript calculations that silently replaced the engine when it was unavailable: the application now says so, instead of computing with an unverified copy.
Five ways of looking for errors
No single test finds every error, so we use several that fail in different ways:
- Comparison with other programs. The same models, fixed ones and random ones generated every night, are solved with OpenSees, Code_Aster, Frame3DD, PyNite, MYSTRAN, Kratos and CalculiX. Every difference is investigated until we know whether the error is ours or the two programs model the case differently.
- Published references. An acceptance suite of cases whose results were published by their authors, not by another commercial program, with tolerances set by the precision printed in the source. Design checks are compared with published worked examples (INTI-CIRSOC, AISC and others).
- Physical invariants. Rotating, mirroring or renumbering a model, or changing its units, must change the answer exactly as physics says; superposition, reciprocity and the energy balance must hold. These tests need no reference value at all.
- Derivations. The frame element matrices are derived symbolically from first principles and compared term by term with the code’s; for the other elements there are written derivations for another engineer to review.
- Fuzzing and mutation testing. Millions of generated inputs look for crashes and non-finite results, and errors are introduced into the code on purpose to check that the tests catch them.
| What | Count |
|---|---|
| Independent finite-element programs in the comparison | 7 |
| Acceptance cases with published results | 12 |
| Published reference values in those cases | 105 |
| Lean theorems whose axioms continuous integration checks | 37 |
Certificates: a result with an error bound
For results that support it, Stabileo also attempts a certificate in the background: a bound, computed with interval arithmetic, that contains the exact solution of the system it solved. When it cannot, the result is marked uncertified, with the reason. The bound is on numerical error, not on the discretization error of the mesh or the time step. For linear analysis, combinations, modal and plastic collapse, the core mathematics of that bound is proved in Lean, a proof assistant in which the computer checks every step; some steps (constraints, one condition of the modal check) are not yet formalized. P-Delta, spectral, harmonic and time-history analyses have certificates too, but their mathematics is not yet formalized in Lean. Continuous integration rejects any incomplete proof or added axiom, and for some kinds of certificate the checker that runs is the very Lean code the proofs are about.
What the certificates do not say
- A certificate bounds the error of solving the system as it was assembled. It does not prove that the system represents the model: the assembly of the stiffness matrix and the loads is tested in the ways above, but not certified. When torsional buckling was missing (SA-2026-007), the certificate certified the wrong problem. Since 0.3.0, end-to-end certificates re-assemble the system independently for frames and trusses and check the result against the model itself; shells, solids and connectors are not covered yet.
- Lean proves the mathematics; that the Rust code implements exactly that algorithm is not proved, except for the checkers that are Lean code.
- The certified design checks evaluate their formulas in interval arithmetic, but the formulas themselves are not formalized: they are compared with published worked examples where those exist, and each code’s coverage (which clauses, which examples) is in the maturity matrix. Masonry, connections, foundations and serviceability are not certified.
- No verification of the program verifies the model. Loads, supports and idealisation are the engineer’s decisions; the model review warns about common mistakes, but it does not replace judgement.
- There has not yet been an independent review by a licensed structural engineer. CIRSOC 301 results are still labelled experimental.
AI drafts and reviews; it does not calculate
The AI assistant drafts models from a description and reviews existing ones, but it does not compute results: the numbers come from the solver and the application’s design-check modules. Its explanations are language-model text and can be wrong; the values that count are the ones in the results. Before a change is applied it shows what it will modify, and it can be undone in one step. The AI features send the description and the model to a server that queries a language model; the solver, the results and the checks do not need it and work offline.
When something fails
Defects that may have affected results already in use are published as safety advisories, with how to recognise an affected model and what to do in the meantime; other safety defects are being triaged and are added when they warrant one. Open advisories are closed when the fix is live on stabileo.com.