Altran/Praxis Correct-by-Construction for a cert authority
http://www.sis.pitt.edu/jjoshi/Devsec/CorrectnessByConstruct...
Same company ports Skein from C to SPARK, finds trouble
http://www.skein-hash.info/sites/default/files/SPARKSkein.pd...
SPARK Ada is available under GPL and commercial licenses. The book below is quite easy to read compared to most stuff with formal methods. The companies building stuff like this usually also have tools to generate tests (property-based testing) from contracts/specs and can automatically turn anything you can't prove into runtime checks. Shocked it's not used more often in areas like smart contracts or cryptocurrency protocols.
https://www.amazon.com/Building-High-Integrity-Applications-...
Galois built Cryptol for NSA but open sourced it.
Rockwell Collins built SHADE and some other tools for high-assurance crypto. They build stuff for the defense sector mainly funded by NSA. They even have a separation-preserving, verified CPU.
There is no linter that will tell you that using the same AES key for years and keeping a block counter in an untrusted location is a bad idea. And if you make your code obscure enough ("abstract" in all the wrong ways), then people will have a really hard time figuring stuff like this out.
And no one does proofs on protocol implementations in practice. Yes, there are some. Yes, there has been some progress to apply it to e.g. OpenSSL — after everyone has been using it for critical infrastructure for decades — so there's like, literally, one practical implementation that has seen a sliver of formal verification.