Yes! Formally verified implementations of Elliptic Curve algorithms http://adam.chlipala.net/theses/andreser_meng.pdf http://adam.chlipala.net/theses/andreser_m

Yes! Formally verified implementations of Elliptic Curve algorithms http://adam.chlipala.net/theses/andreser_meng.pdf http://adam.chlipala.net/theses/andreser_meng.pdf. Amazon has also made use of TLA+ and lightweight formal methods to prove the correctness of their distributed services such as S3 and DynamoDB which arguably underpin a large portion of the internet https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods https://www.amazon.science/publications/how-amazon-web-servi... The burden of using these extreme approaches is high, but there are definitely circumstances where it is warranted. Think of it as TDD on steroids.