Interesting article. I know you’re not the author, but do you have any idea what these companies use for ‘proof engineering’? Is it mostly TLA+?
Galois itself has a lot of projects on Github: https://github.com/GaloisInc/ , would recommend to check those out. They’ve built quite a few tools themselves (seems to be mostly in Haskell), and seem to work quite a bit with Coq and SMT-Solvers like Z3.