有人试过用Z3本身证明Z3吗?
有可能用Z3证明Z3是正确的吗?
更具理论性，是否有可能证明工具X是正确的，使用X本身?
简短的回答是:"不，没有人试图用Z3本身来证明Z3 ":-)
"我们证明了程序X是正确的"这句话是非常误导人的。主要的问题是:什么是正确的。在Z3的情况下，我们可以说Z3是正确的，如果它至少不会对一个不可满足的问题返回"sat"，而对一个可满足的问题返回"unsat"。这个定义可以通过添加额外的属性来改进，例如:Z3不应该崩溃;Z3 API中的函数X具有属性Y等。
在我们就应该证明的内容达成一致之后，我们必须创建运行时模型、编程语言语义(在Z3的情况下是c++)等。然后，使用一个工具(又名验证器)将实际代码转换为一组公式，我们应该使用定理证明器(如Z3)来检查这些公式。我们需要验证器，因为Z3不"理解"c++。验证C编译器(VCC)就是这种工具的一个例子。请注意，使用这种方法证明Z3是正确的并不能明确保证Z3是正确的，因为我们的模型可能是不正确的，验证者可能是不正确的，Z3可能是不正确的，等等。
要使用验证器，如VCC，我们需要用我们想要验证的属性、循环不变量等来注释程序。一些注释用于指定代码片段应该做什么。其他注释用于"帮助/指导"定理证明者。在某些情况下，注释的数量大于正在验证的程序。所以，这个过程不是完全自动的。
另一个问题是成本，这个过程将非常昂贵。这将比实现Z3耗费更多的时间。Z3有30万行代码，其中一些代码基于非常微妙的算法和实现技巧。另一个问题是维护，我们会定期添加新功能并改进性能。这些修改会影响证明。
尽管成本可能非常高，但VCC已被用于验证重要的代码片段，例如Microsoft Hyper-V管理程序。
理论上，任何编程语言X的验证器都可以用来证明自己，只要它也是用X语言实现的。spec#验证器就是这种工具的一个例子。spec#是在spec#中实现的，并且spec#的一些部分是使用spec#进行验证的。注意，spec#使用Z3并假设它是正确的。当然，这是一个很大的假设。
你可以在论文中找到更多关于这些问题和Z3应用的信息:http://research.microsoft.com/en-us/um/people/leonardo/ijcar10.pdf
不，不可能使用工具本身来证明非平凡工具是正确的。这基本上在Gödel的第二个不完备性定理中得到了说明:
对于任何形式有效生成的理论T，包括基本算术真理和关于形式可证明性的某些真理，如果T包含其自身的一致性陈述，则T是不一致的。
由于Z3包含算术，它不能证明自己的一致性。
因为它在上面的评论中提到:即使用户提供不变量，Gödels的定理仍然适用。这不是可计算性的问题。该定理指出在一个一致的系统中不存在这样的证明。
但是你可以用Z3来验证Z3的部分。
5年后编辑:
实际上这个论证比Gödel的不完备定理更简单。
假设Z3是正确的，如果它只对不满足的公式返回UNSAT。
假设我们找到一个公式a，如果a是不可满足的，那么Z3是正确的(并且我们以某种方式证明了这个关系)。
我们可以把这个公式给Z3，但是
- 如果Z3返回UNSAT，可能是因为Z3是正确的或因为Z3中的错误。所以我们还没有验证任何东西。
- 如果Z3返回SAT和反模型，我们可以通过分析模型 找到Z3中的错误。
因此，我们可以使用Z3来查找Z3中的错误，并提高对Z3的信心(达到极高的水平)，但不能正式验证它。