title: Has anyone tried proving Z3 with Z3 itself?
body: <p>Has anyone tried proving <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/">Z3</a> with Z3 itself?</p>
  
  <p>Is it even possible, to prove that Z3 is correct, using Z3?</p>
  
  <p>More theoretical, is it possible to prove that tool X is correct, using X itself?</p>