Has anyone tried proving Z3 with Z3 itself?

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.