24 ms·
I don't quite understand why Z3 is part of the TCB. Isn't Z3 generally used to generate proofs which are then verified by the respective proof assistant?
by mbid 9y ago
I don't quite understand why Z3 is part of the TCB. Isn't Z3 generally used to generate proofs which are then verified by the respective proof assistant?
- tom_mellior 9y agoYes, 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 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.)