RE³ is a stability layer that sits around a language model rather than inside it. Its field dynamics are a small, closed-form system, and that system is proven stable in Lean 4: for every real input, exactly, not by testing. This page is the technical account of what is certified, how it is checked, and what it deliberately does not claim.
Mainstream AI ships on evaluations, RLHF, and red-teaming. All of it is behavioural and empirical, and none of it carries a formal guarantee, because a large language model is far too large and too non-linear to formally verify in general. That is not a gap anyone is about to close.
So RE³ does not try. It does not verify the model. It wraps a proven-stable controller around the model and verifies that instead. The model still generates the words. What the certified layer guarantees is that the state governing those words cannot blow up, cannot oscillate without bound, and cannot leave its envelope, whatever the model or the person does.
The governance field is bounded and stabilised by three operators. They are ordinary closed-form mathematics, not learned components, which is precisely why a theorem prover can reach them. The constants below are published in the foundation papers.
A bounded input produces only a bounded, contracting response. No runaway, from any input the system can receive.
κ = √(19/20) per-dyad contractionISS gain ≤ 39.5
A Lyapunov contraction: the state's response to any input sequence stays inside a proven bound, and settles rather than drifting.
κ = 0.85 Lyapunov contractionISS gain 0.288
Bounded input, bounded output. The field state stays inside its range for every admissible input sequence, and the drift channel is hard-clamped.
drift ∈ [−0.04, +0.08]state ∈ [0, 1] BIBO-bounded
A fourth result, the compositional stability certificate, is what lets these compose: the stability of the assembled system follows from the stability of its parts, rather than having to be re-established for every combination. Each result is published under a permanent DOI.
A theorem about an operator on paper says nothing about the operator that actually runs. Three layers connect them, and the middle one is the layer most formal-methods work leaves out.
The properties above are machine-checked theorems, over all real inputs, exactly. This is the actual guarantee. It is not a test suite that passed; it is a statement that no counterexample exists.
An automated check confirms that every shipped constant and operator form matches the theorems, and pins the proof-bearing files by structural identity. An edit made without a new proof diverges and fails the check. This is what makes the code the thing that was proven, rather than something that resembles it.
A falsification search runs the real shipped operators over 100,000 sampled inputs per layer and checks the proven bound held on every one. It looks for a backstop that widens, an accumulator that escapes its bound, a contraction that expands. It finds none. This confirms the code matches the proof; it is belt and braces, not the guarantee itself.
The Lean 4 proofs are about stability: the field cannot run away, cannot oscillate without bound, cannot leave its envelope. That is a real guarantee and it is the foundation the rest stands on. It is not a guarantee that the system will say the right thing to a person in distress. Safety behaviour is engineered, measured, and independently evaluated. It is demonstrated, not proven, and we will not blur those two words.
The envelope search is empirical. Sampling raises confidence; it cannot prove that no counterexample exists in an unsampled region. The proof of absence is the theorem. The search is there to catch the case where the shipped code has quietly stopped being what the theorem describes.
And the language model is still a language model. Nothing here verifies it, because nothing can. The claim is narrower and, we think, more useful: the layer that governs it is certified, and that layer is what holds when the model does something nobody predicted.
The same certified core runs underneath a relational companion holding a person in distress, and underneath a team of AI agents from four different vendors doing research together. Neither domain was designed for the other. That is the argument for calling it infrastructure rather than a safety feature.
A relational companion, live with pilot testers in the EU. The hardest test of the core: a real person, often at their worst hour, where getting it wrong matters most.
Six AI agents from four vendors, working as one research team, every contribution read before it entered the result. A domain the core was never built for.
The conceptual foundations are public and citable. You do not have to take any of the above on our word. The restricted editions, which carry the full operators and proofs, are held privately, and two patent applications are filed with the Finnish Patent and Registration Office.
The AURI³ system paper, which describes the companion built on this core, is published alongside them.
The crew we governed was doing research. Research is a forgiving domain: the worst thing that happens is a wrong sentence in a report, and we caught those. But agents are not staying in forgiving domains. They are being pointed at defence workflows, drone operations, power generation, grid management, industrial control, robotics, autonomous vehicles, and increasingly at other AI teams. The conduct problem does not change when the room gets harder. What changes is the cost of getting it wrong.
That is the part we think is under-built, and it is why we suspect we are scratching the surface. A governor does not need to understand a turbine to notice that an agent stated a contested thing as settled, claimed a source it did not have, or quietly closed a question a person should have decided. Those are properties of the agent's conduct, not of the domain. It is why the same core read six models from four vendors while knowing nothing about any of them. Point it at a crew working on something that matters and it is the same read. The stakes are what move.
We have governed agents doing research. We have not governed agents doing anything that could hurt somebody, and the distance between those two sentences is the whole of the work we cannot do alone. A demonstration on a research task is evidence that the read is domain-independent. It is not evidence that we are ready for a room where a wrong call has consequences.
Every one of those fields carries its own certification regime, built over decades by people who learned the hard way, and an oversight layer does not inherit any of it by being mathematically sound. Nor does the certified stability of the field say anything about whether the conduct rules are the right rules for that domain. Those would have to be written with people who actually work there. We are not claiming to have done that. We are saying it looks possible, and that saying so out loud is more useful than sitting on it.
Where AI agents are already working, and where we suspect the same read applies:
This is a hypothesis, not a roadmap, and we are stating it as one. Two people in Seinäjoki cannot responsibly test it alone, and we are not going to pretend otherwise in order to sound bigger than we are. If you are putting AI agents somewhere the mistakes are expensive, and the idea of reading their conduct before it reaches the work sounds interesting rather than obviously wrong, that is the conversation we are looking for.
RE³ is the engine. AURI is one product on it. If you are working somewhere the failure mode matters more than the demo, we would like to hear what you are building.
Get in touchQuestions? info@real-e3systems.fi · WhatsApp +358 50 3791916