Quick, easy formal verification tools that programmers can use on the spot from the IDE are hard to make for most languages because most languages and their com

Quick, easy formal verification tools that programmers can use on the spot from the IDE are hard to make for most languages because most languages and their compilers weren't made with such thing in mind. I guess Rust might be heading somewhere interesting with tooling, with tools like Flowistry existing (https://github.com/willcrichton/flowistry https://github.com/willcrichton/flowistry) showing what is possible. It's a plugin that can compute backwards / forwards static slices for you, straight in the IDE as a VSCode plugin. I think you need an external program that runs a full program analysis to do the same in C++.