I worked on a large financial transaction system for up to $7B per day in Haskell that used formal methods like Agda, TLA+, etc, with a lot of logic in the type

I worked on a large financial transaction system for up to $7B per day in Haskell that used formal methods like Agda, TLA+, etc, with a lot of logic in the type level (i.e. Liquid Haskell), as a test engineer. The entire system was covered in property based tests, proofs, and then normal tests from unit -> system. We literally had two bugs categorised as P2/P1/P0 on release, both of which were design related, and both were fixed before users saw them. It was crazy effective (but took years).