It's relatively common in embedded programming (in my experience). A lot of real-time programming is around scheduling. You certainly can use formal proofs there too, but statistical methods would be common at significant scale.