Has anyone tried proving Z3 with Z3 itself?

Question

Has anyone tried proving Z3 with Z3 itself?

Is it even possible, to prove that Z3 is correct, using Z3?

More theoretical, is it possible to prove that tool X is correct, using X itself?

Ridgway

In the future, please provide more information in the question so that people can understand what you're talking about. On one hand I understand that you are asking people who already know Z3, but since people that don't know what Z3 is will be flagging this question as "what is I don't even..." then you must make sure people know what you're talking about, in this case by at least providing a link to the tool. – Duckboard

Having said that, I'm not altogether sure this question belongs here, I think perhaps Software Engineering is a more suitable place, but I'll wait and see what the community says. – Duckboard

@Lasse Theoretical Computer Science more like. My Goedel-inspired guess would be that any system powerful enough to be interesting is unable to prove its own correctness – Palaeobotany

@Palaeobotany As outlined by Leonardo de Moura in his answer, “proving Z3” would mean for a human to provide invariants that would then participate to the computation of Verification Conditions whose validity would be checked by Z3. Although Z3 is an automated prover, in a sense, it would only be checking the choice of invariants, not doing the proof itself. So there is absolutely no Goedel-like paradox here. – Kensell

Answer 1

The short answer is: “no, nobody tried to prove Z3 using Z3 itself” :-)

The sentence “we proved program X to be correct” is very misleading. The main problem is: what does it mean to be correct. In the case of Z3, one could say that Z3 is correct if, at least, it never returns “sat” for an unsatisfiable problem, and “unsat” for a satisfiable one. This definition may be improved by also including additional properties such as: Z3 should not crash; the function X in the Z3 API has property Y, etc.

After we agree on what we are supposed to prove, we have to create models of the runtime, programming language semantics (C++ in the case of Z3), etc. Then, a tool (aka verifier) is used to convert the actual code into a set of formulas that we should check using a theorem prover such as Z3. We need the verifier because Z3 does not “understand” C++. The Verifying C Compiler (VCC) is an example of this kind of tool. Note that, proving Z3 to be correct using this approach does not provide a definitive guarantee that Z3 is really correct since our models may be incorrect, the verifier may be incorrect, Z3 may be incorrect, etc.

To use verifiers, such as VCC, we need to annotate the program with the properties we want to verify, loop invariants, etc. Some annotations are used to specify what code fragments are supposed to do. Other annotations are used to "help/guide" the theorem prover. In some cases, the amount of annotations is bigger than the program being verified. So, the process is not completely automatic.

Another problem is cost, the process would be very expensive. It would be much more time consuming than implementing Z3. Z3 has 300k lines of code, some of this code is based on very subtle algorithms and implementation tricks. Another problem is maintenance, we are regularly adding new features and improving performance. These modifications would affect the proof.

Although the cost may be very high, VCC has been used to verify nontrivial pieces of code such as the Microsoft Hyper-V hypervisor.

In theory, any verifier for programming language X can be used to prove itself if it is also implemented in language X. The Spec# verifier is an example of such tool. Spec# is implemented in Spec#, and several parts of Spec# were verified using Spec#. Note that, Spec# uses Z3 and assumes it is correct. Of course, this is a big assumption.

You can find more information about these issues and Z3 applications on the paper: http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf

Weksler

Answer 2

No, it is not possible to prove that a nontrivial tool is correct using the tool itself. This was basically stated in Gödel's second incompleteness theorem:

For any formal effectively generated theory T including basic arithmetical truths and also certain truths about formal provability, if T includes a statement of its own consistency then T is inconsistent.

Since Z3 includes arithmetic, it cannot prove its own consistency.

Because it was mentioned in a comment above: Even if the user provides invariants, Gödels's theorem still applies. This is not a question of computability. The theorem states that no such prove can exist in a consistent system.

However you could verify parts of Z3 with Z3.

Edit after 5 years:

Actually the argument is easier than Gödel's incompleteness theorem.

Let's say Z3 is correct if it only returns UNSAT for unsatisfiable formulas.

Assume we find a formula A, such that if A is unsatisfiable then Z3 is correct (and we somehow have proven this relation).

We can give this formula to Z3, but

1. if Z3 returns UNSAT it could be because Z3 is correct or because of a bug in Z3. So we have not verified anything.
2. if Z3 returns SAT and a countermodel, we might be able to find a bug in Z3 by analyzing the model
3. otherwise we don't know anything.

So we can use Z3 to find bugs in Z3 and to improve confidence about Z3 (to an extremely high level), but not to formally verify it.

Sniff

we should not confuse Z3 with the logical system it implements: first-order logic + theories (such as arithmetic). The question is not about whether we can prove the consistency of this logical systems, but whether Z3 is correct or not. These are two different things. We can say Z3 is correct if it does not return unsat for a satisfiable set of assertions. Another remark is that Z3 does not support invariants, the invariants are sent to a software verification tool that usually implements a stronger logical system. – Weksler

How can you proof that Z3 is consistent without showing that its logical system is consistent? You could just take the assumption that the logical system is consistent, but then you are just proving that Z3 is correct, assuming it is correct. – Sniff

Yes, we are assuming that first-order logic + theories such as arithmetic is consistent. Most mathematicians believe this is the case. When we are talking about Z3 correctness, we are considering the algorithms and procedures used in its implementation, and not the consistency of the logical system it is based on. Finally, as I pointed out in my answer, the proof of correctness must be carried in another system that "understands" the semantics of C/C++ (the programming language used to implement Z3). This system may use a different logical system, and may even invoke Z3 as subroutine. – Weksler