I'm not familar with pyre, but i have experimented with some security static analysis tools. The one's i have experimented with take some normal program and try to analyse it. The analysis is usually far from complete, and as a result has so many false positives that its difficult to adopt.

Anyways, i would say those are rather different from systems where you give an actual proof of correctness.