Comment by klibertp

Maybe they have automatic theorem prover running on Jenkins and they just refuse to merge changes which would be proven to be wrong? Anyway, I'm going to read more about what and how they did, it's fascinating to see a non-trivial software system proven correct.