From the look of these bugs, like this one but especially the other race condition bug that suggested 10x the user's input dosage, I'm gonna go out on a limb and say formal verification appears to be used little or none..