マイクロソフトリサーチは、Z3は、世界最速の定理証明器であると宣言した。Z3は、ほかのアプリケーションへの低レベルツールとして設計されており、単独では動作しない。定理証明器のホストは、 Spec#/Boogie、Pex、Yogi、Vigilante、SLAM、F7、SAGE、VS3、FORMULA、HAVOCを含む数多のプロジェクトで使用されている。
Z3の.NET APIを使用すると、エンコード定義をオブジェクト指向スタイルで行うことができる。しかしながら、たとえば、Z3チュートリアルの例では小さな問題に関しても、非常に退屈なコードになることを示している。Bart De Smet氏は、OOスタイルのAPIをラップして、LINQ to Z3と呼ばれるクエリスタイルのAPIにし、すばらしく簡易化した。以下の例は、Bart De Smet氏のChannel 9インタビューで提示されていたものである。
var theorem = from t in ctx.NewTheorem<Symbols<int, int, int, int, int>>()
where t.X1 - t.X2 >= 1
where t.X1 - t.X2 <= 3
where t.X1 == (2 * t.X3) + t.X5
where t.X3 == t.X5
where t.X2 == 6 * t.X4
select t;
var solution = theorem.Solve();
Console.WriteLine("X1 = {0}, X2 = {1}, X3 = {2}, X4 = {3}, X5 = {4}",
Z3のプライマリサポートはWindowsであるが、LinuxバージョンのZ3も存在している。 Z3は、非商用に“Microsoft Research License Agreement”下で利用可能である。RiSE4fun上でZ3のオンラインバージョンを使うことができる。