[nickpsecurity]

Extra comment to add something I left off. There's at least two types of static analysis and solver tools: unsound and sound. The sound ones, especially RV-Match and Astree Analyzer, use a formal semantics of the code, a formal statement of the property, and automatic analysis to determine if it holds or doesn't depending on the goal. Related, SPARK Ada and Frama-C have their formal specs and code turned into verification conditions that check for code conformance to the specs. The VC's go through Why3 which sends them to multiple, automated solvers to logically check them. Far easier to scale and get adoption of these automated methods than manual proofs.

The main drawback is potential errors in the implementations of the analyzers or solvers that invalidate what they prove. Designs for certifying solvers exist which essentially are verified or produce something verifiable as they go. There's examples like verSAT and Verasco. The tech is there to assure the solvers. Personally, I'm guessing it hasn't been done to industrial solvers due to academic incentives. Their funding authorities push them to focus on quantity of papers published over quality or software improvements with new stuff over re-using good old stuff. Like infrastructure code, everyone is probably just hoping someone else does the tedious, boring work of improving the non-novel code everyone depends on.

Also, given my background in high-assurance research, I'm for each of these tools and methods, mathematical or not, to be proven over many benchmarks of synthetic and real-world examples to assess effectiveness. LAVA is one example. I want them proven in theory and practice. The techniques preventing or catching the most bugs get the most trust.