RESEARCH
Research
Research notes and published papers from Ironproof. Every figure traces to a cited source, and each note states what it does not show.
PUBLISHED PAPERS · ARXIV
arXiv:2610.11073
IRONPROOF: COBOL-to-Python Transpilation with SMT-Based Equivalence Checking
arXiv:2610.10992
The Hint Weight of ML-DSA Signatures Is Key-Dependent: An Empirical Study across the Three FIPS 204 Parameter Sets
arXiv:2604.06712
Broken Quantum: A Systematic Formal Verification Study of Security Vulnerabilities Across the Open-Source Quantum Computing Simulator Ecosystem
arXiv:2604.05292
Broken by Default: A Formal Verification Study of Security Vulnerabilities in AI-Generated Code
RESEARCH NOTES
· Ironproof Research
What our proofs do not prove
A verification verdict is only as strong as the question it was asked. For each thing Ironproof checks: what we guarantee, what holds only within bounds, and what is still open.
· Ironproof Research
Zero barriers, one reviewer
Four 2026 agent containment failures, aggregated. The detection window in one was 5.5× longer than the time a comparable agent needed to fully compromise a production estate in another.
STATE OF THE ENGINE
What works today. What is in progress. What is still open.
The same three states we give every result, applied to ourselves. Each line says how to check it.
As of
WORKS TODAY
Code translation, checked by proof
A Python module of four functions with loops, translated to Rust. Equivalence is proved for every input series of up to six values, and the loops are proved for any per-step calculation. Beyond six values, 100,000 random runs found no difference. Test files are available to reviewers on request.
MISRA C on translated code
The C translation of a signal-processing function passes the open-source MISRA C:2012 checker (cppcheck) on the whole program, and its equivalence with the Python original is re-proved. This is a free tool covering part of the rules, not a certification.
Authorization of critical actions
Every request routed through Ironproof is checked against your rules before it runs. Allowed, it runs. Not allowed, it never does. Either way, the decision is sealed. Open a sealed decision and check it yourself, in your browser, with no server and no account.
CHECK A SEALED RECORDTry to get past the gate
Four attacks against the sealed sample payment policy, computed in your browser. Some get through, and the page says exactly why.
OPEN THE LAB
IN PROGRESS
Legacy modernization
IBM’s GenApp insurance programs, checked under a CICS model we write ourselves and tested against a real CICS. A run on z/OS and an outside replay are still to come. Same-behavior answers from our translation checker are suspended after audits reproduced dozens of false ones, on cases written to attack the tool.
READ THE RESEARCHC software security
Checking that a security fix really closes the flaw, on real fixes from open-source projects. The checker is being rebuilt; earlier results are not presented as complete proofs.
READ THE RESEARCHSecurity fix in Rust
A published flaw in a Rust library (RUSTSEC-2017-0004). The original code and a plausible false fix are both caught. The real fix is proved on the actual code for standard line lengths, and for any length on a hand-written model whose link to the code is not yet checked by a machine.
OPEN PROBLEMS
Faithfulness
Showing that the logic we check says the same thing as the original policy, code or program. A proof is only as good as this step.
Fixes written by language models
Proving that a C fix proposed by a model closes the flaw, not just that it passes the tests.
COBOL that reads real data
Equivalence for every input a program can receive, not for one run.
Working on one of these? We want to take them on with university researchers. WRITE TO US