We run your original and our proven twin side by side, and chase every difference.
When we rebuild a program we run the old one and the new one on the same inputs and watch where they part. Where they disagree is where the interesting things are.
Why it exists
Proof tells you the new code matches its specification. It can't tell you the specification was right. A wrong constant, or a wrong guess about what the old compiler did with an overflow, and the proof is happy with both. Running the original is how we catch those.
There's no acceptable divergence rate. Every difference gets explained. It's our fault, or the original's, or the comparison itself is broken, and we say which.
The first time
First time we ran this, 403 of 407 cases agreed. Ninety-nine percent. Everything in me said round it off.
The four were a silent overflow in the original. A field too small for a result nobody had checked, quietly truncating, for decades.
We do the same with the cyber-hardening work.
What you get
A divergence report. Every difference we found, which side it's on, and why.
The name
楊振寧
It's named for Chen-Ning Yang. In 1956 he and Tsung-Dao Lee asked whether parity really holds in weak interactions, when everyone had assumed it did. Chien-Shiung Wu's experiment showed it doesn't.
If you've got an old system and you'd like to know what it's really doing, this is where we'd start.
Talk to us