Dec 24, 2017

Yes, if you use Z3 as part of a proof assistant like Isabelle/HOL or F-Star.

No, if you use Z3 as part of some other system that does not have its own primitive notion of proofs and proof checking. Many tools are like this: Dafny is one, I think, as is Why3, and the Alive system for checking the correctness of LLVM peephole optimizations. They simply trust Z3.

It's also used in lots of other things that are not "verifiers" as such. For example, to find new compiler optimizations by superoptimization: https://arxiv.org/abs/1711.04422 (And sure enough, if you search the paper for "Z3", the first hit is a paragraph where the authors describe that they once had a miscompilation due to a bug in Z3.)