When crosshair finds no counterexamples, has it used the Z3 solver to prove that my contract holds?
The docs indicate that the absence of a counterexample doesn't guarantee that the property holds, but is that just because the translation or modeling could be incorrect?
Disclaimer: I am the the primary contributor for CrossHair (I'm just using stack overflow as a public way to record answers to questions I've previously been asked)
Apart from the likely many issues with unsound modeling, CrossHair does not provide this guarantee.
CrossHair is a wildly incomplete system. Internally, for each postcondition, it generates three possible results: "confirmed," "rejected," and "unknown." It only produces output for the "rejected" case; therefore, the absence of output does not indicate a verification of the statement.
Why does CrossHair work this way? Two reasons:
It's best to think of CrossHair as a solver-assisted fuzz tester.
All that said, if you'd still like to see what properties are confirmable, you can request this output with a special "report all" option:
crosshair check --report_all [TARGET]
.