I'm currently taking a formal methods course at university and a couple of names thrown around as users of FMs were Microsoft (for static analysis of drivers) and Altran Praxis. Coverity were also mentioned for performing static analysis of the internal LHC framework for CERN and the Mars Rover kernel for NASA.

I was wondering if any HN users at smaller companies made use of formal methods, and in what kind of contexts?