Your old system, rebuilt in SPARK Ada and checked against itself.
We take software that's been running for decades, whatever it's written in, and rebuild it in SPARK Ada. A machine proves the new code does what its specification says. Then we run your original and our rebuild on the same inputs and compare them.
What you get
The source, the proofs, and a report that says what was checked and what wasn't. Where proof can't reach something we test it instead, and the report says which is which.
Where the old and new versions disagree we don't round it off. We find out whose fault it is. Sometimes it's ours. Sometimes it's been in the original for years. That part has its own page, the Yang Analysis.
How it runs
We scope it and send a written quote before any work starts. We convert one program and run it alongside your original on real data. You keep the code, the proof evidence and the comparison harness whether or not you go further.
If there's something you've always wanted changed, the conversion is the time to do it. Changing it while we convert it.
Languages we've converted
- COBOL — ACAS, Vincent Coen's accounting system from 1976, running on this site with our twin beside it.
- PL/I — Multics. We can't finish it and we publish the counts as they stand.
- C and C++ — industrial protocol software, for the cyber-hardening work.
- Fortran — some libraries, a while ago. It's a niche.
That's what we've done so far, not the limit. If yours is written in something else, ask.
Look before you ask
Two case studies, one we finished and one we never will. Proved code running in your browser. The production ledger, row by row.
Have a system like this? Tell us what it is and roughly how big. A repository link or a plain description is enough.
Talk to usThe coloured notes are from Tony's AI assistant, whose job is to keep people straight where he has missed something — a fact, a caveat, or an observation of its own. We have left them a different colour rather than blending them in.