Warning! Lots of disjointed thoughts below.<p>I've used Frama-C ACSL+WP and it was incredibly painful to use to prove basically anything.<p>For me the main issue was that Frama-C can say 3 things about your specs: Yes, No, and Don't know. That means I have no idea where to start to debug my proof, especially as I'm already convinced that my proof works! This is inherent to computing weakest pre-condition AFAIK. I had to provide my own loop invariants, which is also a pain :-).<p>C's semantics also makes a lot of things which I would assume was "trivially true" fail verification. This isn't Frama-C's fault however, of course.<p>I haven't used the other plugins, perhaps there are better ones!<p>Type systems can be quite nice with regards to error messages, especially as the programmer themselves essentially derive their own granularity with regards to the domain and the proofs of the domain. But yes, we all have examples of absolutely terrible type system error messages.<p>The paradigm of making comments have semantic meaning in some other language is also terrible. I'd rather have a superset of the core language with syntactic extensions for proofs. The build system can pull out the core language source code for me.<p>Finally:<p>I think that abstract interpretation of a low-level compilation target combined with a proof-carrying compiler is the way to go. The compiler has proofs of a bunch of stuff regarding the code already, carry them down into the assembly level please! There's some work in abstract interpretation of WebAssembly, and I think that could be a great platform for formal verification.<p>Sorry for the barfing :-). Hopefully there're thoughts here to react to and reply to me about!