Legacy software, changed magnificently.
We rebuild COBOL, PL/I and Fortran systems — and the spreadsheets critical decisions rest on — in SPARK Ada, and we prove the rebuild against your own system's output, line by line. You get the source, the proofs, and a report naming exactly what was checked and what was not.
Three steps: 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.
The two pieces of work we would rather be judged on are both public, and you can open either without talking to us. ACAS is a complete accounting system written in 1976 and maintained by its author ever since; it runs on this site, free, with a machine-checked twin beside the original and his name on it. Multics is a conversion we cannot finish, and we publish its counts as they stand — including the ones that fell when we measured a second time.
Two case studies: one we finished, one we never will · The production ledger, row by row · Talk to us
Ghillie — the free assistant the factory also makes
Ghillie is a personal assistant that runs on your own computer. He opens no doors to the internet, sends nothing anywhere without your say-so, and every decision that matters is made by a rule that has had its contract discharged by a prover — checked by a machine, not somebody's opinion. He is free, and his workings are open for anyone to read.
How Ghillie grows
Ghillie gains new abilities as extensions, and the factory makes them. Each one arrives as source code with its proof attached, and your machine re-checks the proof before anything installs — what doesn't prove, doesn't run. He never rewrites himself: his abilities rise, his authority never does.
Here is the part we think matters most. With your consent, given in advance and yours to withdraw, Ghillie can notice what he's missing — a rule he needed and didn't have — and order that improvement from the factory himself. An assistant that gets better at helping you, on your terms, with every improvement proved before it runs. Without that consent he simply tells you what he lacks, and the decision stays where it belongs: with you.
Download Ghillie — free, open source (AGPL-3.0), for Windows, Mac and Linux, with checksums. Or start at thereef.ink — where the members who steer what gets built next also live.
Why it matters
Most attacks don't pick a clever lock, they walk in through an ordinary mistake in ordinary software. That's the weakness we go after — a mistake that cannot happen can't be used against you.
This standard used to be for aircraft and defence only, because it took specialists years and nobody else could justify the cost. Machines do that work now, so the same treatment can go on the software that runs a hospital, a bank, a council or a factory floor — and on the assistant sitting on your own desk.
Beyond Ghillie
The factory also works to order, on software that has nothing to do with Ghillie. Two kinds of work: we build new software to your description, and we sort out software you already depend on — including the old system nobody wants to touch. Same rule for both: prove what can be proved, test what can't, and say which is which. I'll be honest — before this factory I would have told you maths on software sounded academic. It isn't. It's the difference between hoping and knowing.
We publish our failures next to our successes — most companies don't, which is half the reason we do. If your software has consequences when it goes wrong, talk to us.
Proof used to need a mathematician. Now it needs a sentence.