Assurance · for auditors & risk owners
Confidence you can
inspect.
Modernization fails when the new system quietly behaves differently from the old one. You find out in production, in an audit, or in court. Constat is built so "it behaves the same" is something you can check, not something you have to believe.
public NIST COBOL-85 programs run byte-exact on real IBM i V7R5. Not our corpus, programs anyone can look up, and run themselves.
See one run on bothHow the guarantee is built
Three mechanisms, not one promise
Run both, compare
The original runs on IBM i. The modernized system runs in Rust. Both process the same real inputs, and we compare the resulting business state directly. Equivalence is measured, not assumed from tests that happen to pass.
A verified engine
The engine that generates the Rust is backed by machine-checked mathematical proofs, with a small trust boundary we state explicitly. It is a verified transpiler, not a best-effort tool that hopes the output matches.
Evidence you can audit
Every modernized program ships with an evidence package: what was produced, how, and the proof it behaves like the original. Your team and your auditors inspect it on their own terms.
The evidence, in three layers
How far each claim is actually proven
We report assurance at three separate levels, widest to narrowest. Most tools blur them together. We keep them apart, so you can see exactly where a guarantee ends and a roadmap begins.
The pipeline parses the languages an IBM i estate is written in and emits idiomatic Rust. This is the widest layer and the weakest guarantee: transpiling code is not, on its own, proof that behavior is preserved.
The engine that writes the Rust is checked inside the Lean 4 kernel, with a small, explicitly named axiom footprint. Nothing load-bearing is assumed off the record.
The narrowest and strongest layer: each program runs on live IBM i hardware while its modern twin runs on the same inputs, compared byte for byte, with a dossier anyone can re-check. This is what we mean by proven.
Every figure here is generated from the artifacts of record. A number without a source does not ship.
The audit trail
Every step is kept, so every step can be checked
Modernization is only trustworthy if you can retrace it. Constat keeps the full trail from your source to the running Rust, and hands it to you. Nothing about the transpilation is a black box.
Formal proofs (Lean 4)
The engine's correctness is proved in the Lean 4 theorem prover. The proofs are machine-checked, and they travel with the result.
Two solvers, cross-checked
The operations we model are discharged by the Z3 SMT solver and independently re-checked by CVC5, so a mistake in one solver does not slip through. The SMT-LIB2 formulas can be emitted for a third party to re-check.
The transpilation trail
We keep the abstract syntax tree and every intermediate representation from each stage. How your code became Rust is open, not hidden.
Source-to-Rust map
Each line of generated Rust links back to the COBOL or RPG it came from. You read the new code against the old, line by line.
Provenance on every artifact
Every artifact is recorded with its provenance, so a third party can confirm nothing was swapped or edited after the fact.
Re-audit it yourself
One command re-checks the whole record end to end: the artifacts, the proofs, and a record of exactly which generator produced them. The process is deterministic, so two runs are byte-identical and directly comparable. Nothing here needs your trust, only your check.
$ axiom audit --json{ "verdict": "COHERENT" }Honest by default
What we don't claim
Equivalence is established per program, on your inputs. It is not a blanket product guarantee. A program we haven't modernized and validated is not covered, and we say so. Where a result is a modernization target rather than a proven lane, it is labelled as one. The scope is always explicit. One more line, on the proofs themselves: the code generator is machine-checked in the Lean kernel, but the final Rust passes through an audited post-processing step. Until that step is folded into the verified generator, it sits in the trusted computing base, and we count it there rather than call it proven.
We keep IBM i (which runs on IBM Power) distinct from the mainframe (IBM Z). Our behavioral validation runs against real IBM i hardware; other targets are validated within each engagement.
Due diligence
Go as deep as you need
For technical evaluation we walk your engineers and auditors through the proof and the evidence for real programs, under NDA. Bring your hardest questions.