This is a fair question really. Calling it a static analyser is misleading and seems to be editorialised. It's not like static analysers in C++.

It's actually a formal verification tool. They call it a "static verifier" not a "static analyser".

Most static analysis tools seek to find potential problems in your code - generally common mistakes - but they aren't proving anything usually. They have false positives and negatives. Formal verification requires you to write properties about your code and then it proves it.