I know Amazon, Microsoft and Oracle routinely use TLA+, as do many smaller companies. TLA+ is a specification language that includes both a model checker and a theorem prover, and the companies I mentioned use TLA+ tp specify and formally verify real-world code (e.g. Amazon uses it to specify and verify most of the AWS services; Intel uses it to verify chip design).<p>In practice, the theorem prover is not used much in real-world applications because proofs are very, very expensive[1], but the model checker is used very often and I&#x27;ve found it to be extremely useful.<p>[1]: seL4 required 30 man-years to prove a &lt;10KLOC C program. The cost of proofs may grow exponentially in the size of the codebase.