Also Frama-C/Eva: https://www.frama-c.com/fc-plugins/eva.html

It took some eagle eye to spot the link, but they have the source in a self-hosted copy of gitlab: https://git.frama-c.com/pub/frama-c and a sibling repo is also interesting where they seem to apply analysis to some open source code as an example: https://git.frama-c.com/pub/open-source-case-studies

Also Mathworks Polyspace Code Prover: https://mathworks.com/products/polyspace-code-prover.html

I _think_ Perforce's QA-C uses abstract interpretation, but I'm not 100% sure.

You can add grammatech‘s codesonar

I believe the "level" referred to is soundness. Codesonar is self-admittedly not sound [1], and instead focuses on other valuable aspects of static analysis. It's a different type of tool.

[1] https://blogs.grammatech.com/how-sound-static-analysis-compl...