Z3 Theorem Prover

Software for solving satisfiability problems

Z3 Theorem Prover

Original author(s)| Microsoft Research
Developer(s)| Microsoft
Initial release| 2012; 13 years ago (2012)
Stable release|

4.15.1[1]  / 10 June 2025; 21 days ago (10 June 2025)

Repository|

* github.com/Z3Prover/z3

Written in| C++
Operating system| Windows, FreeBSD, Linux (Debian, Ubuntu), macOS
Platform| IA-32, x86-64, WebAssembly, arm64
Type| Theorem prover
License| MIT License
Website| github.com/Z3Prover

Z3, also known as the Z3 Theorem Prover, is a satisfiability modulo theories (SMT) solver developed by Microsoft.[2]

## Overview

[edit]

Z3 was developed in the Research in Software Engineering (RiSE) group at Microsoft Research Redmond and is targeted at solving problems that arise in software verification and program analysis. Z3 supports arithmetic, fixed-size bit-vectors, extensional arrays, datatypes, uninterpreted functions, and quantifiers. Its main applications are extended static checking, test case generation, and predicate abstraction.[citation needed]

Z3 was open sourced in the beginning of 2015.[3] The source code is licensed under MIT License and hosted on GitHub.[4] The solver can be built using Visual Studio, a makefile or using CMake and runs on Windows, FreeBSD, Linux, and macOS.

The default input format for Z3 is SMTLIB2. It also has officially supported bindings for several programming languages, including C, C++, Python, .NET, Java, and OCaml.[5]

## Examples

[edit]

### Propositional and predicate logic

[edit]

In this example propositional logic assertions are checked using functions to represent the propositions a and b. The following Z3 script checks to see if  a ∧ b ¯ ≡ a ¯ ∨ b ¯ {\displaystyle {\overline {a\land b}}\equiv {\overline {a}}\lor {\overline {b}}} :

(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (not (= (not (and a b)) (or (not a)(not b)))))
(check-sat)

Result:

unsat

Note that the script asserts the negation of the proposition of interest. The unsat result means that the negated proposition is not satisfiable, thus proving the desired result (De Morgan's law).

### Solving equations

[edit]

The following script solves the two given equations, finding suitable values for the variables a and b:

(declare-const a Int)
(declare-const b Int)
(assert (= (+ a b) 20))
(assert (= (+ a (* 2 b)) 10))
(check-sat)
(get-model)

Result:

sat
(model
(define-fun b () Int
-10)
(define-fun a () Int
30)

## Awards

[edit]

In 2015, Z3 received the Programming Languages Software Award from ACM SIGPLAN.[6][7] In 2018, Z3 received the Test of Time Award from the European Joint Conferences on Theory and Practice of Software (ETAPS).[8] Microsoft researchers Nikolaj Bjørner and Leonardo de Moura received the 2019 Herbrand Award for Distinguished Contributions to Automated Reasoning in recognition of their work in advancing theorem proving with Z3.[9][10]

## See also

[edit]

* Free and open-source software portal

* Formal verification

## References

[edit]

1. ^ "Release 4.15.1". 10 June 2025. Retrieved 13 June 2025.
2. ^ "Using the SMT solver Z3" (PDF). Archived from the original (PDF) on 2020-11-17. Retrieved 2019-12-01.
3. ^ "Microsoft's Visual Studio timeline and Z3 Theorem Prover, Google Cloud Launcher, Facebook's Fresco—SD Times news digest: March 27, 2015". March 27, 2015.
4. ^ "GitHub - Z3Prover/z3: The Z3 Theorem Prover". December 1, 2019 – via GitHub.
5. ^ Bjørner, Nikolaj; de Moura, Leonardo; Nachmanson, Lev; Wintersteiger, Christoph (2019). "Programming Z3". Programming Z3. Archived from the original on February 9, 2023. Retrieved May 21, 2023.
6. ^ "Programming Languages Software Award". www.sigplan.org.
7. ^ Microsoft Z3 Theorem Prover Wins Award
8. ^ ETAPS 2018 Test of Time Award
9. ^ The inner magic behind the Z3 theorem prover - Microsoft Research
10. ^ Herbrand Award

## Further reading

[edit]

* Leonardo De Moura; Nikolaj Bjørner (2008). "Z3: an efficient SMT solver". Tools and Algorithms for the Construction and Analysis of Systems. 4963: 337–340.
* The inner magic behind the Z3 theorem prover

## External links

[edit]

* Official website
* Official playground

* v
* t
* e

Microsoft free and open-source software (FOSS)

Overview|

* Microsoft and open source
* Shared Source Initiative

Software|

| Applications|

* 3D Movie Maker
* Atom
* Conference XP
* Family.Show
* File Manager
* Open Live Writer
* Microsoft Edit
* Microsoft PowerToys
* Terminal
* Windows Calculator
* Windows Console
* Windows Package Manager
* WorldWide Telescope
* XML Notepad

|

Video games|

* Allegiance

Programming
languages|

* Bosque
* C#
* Dafny
* F#
* F*
* GW-BASIC
* IronPython
* IronRuby
* Lean
* P
* Power Fx
* PowerShell
* Project Verona
* Q#
* Small Basic Online
* TypeScript
* Visual Basic

Frameworks,
development tools|

* .NET
* .NET Framework
* .NET Gadgeteer
* .NET MAUI
* .NET Micro Framework
* AirSim
* ASP.NET
* ASP.NET AJAX
* ASP.NET Core
* ASP.NET MVC
* ASP.NET Razor
* ASP.NET Web Forms
* Avalonia
* Babylon.js
* BitFunnel
* Blazor
* C++/WinRT
* CCF
* ChakraCore
* CLR Profiler
* Dapr
* DeepSpeed
* DiskSpd
* Dryad
* Dynamic Language Runtime
* eBPF on Windows
* Electron
* Entity Framework
* Fluent Design System
* Fluid Framework
* Infer.NET
* LightGBM
* Managed Extensibility Framework
* Microsoft Automatic Graph Layout
* Microsoft C++ Standard Library
* Microsoft Cognitive Toolkit
* Microsoft Design Language
* Microsoft Detours
* Microsoft Enterprise Library
* Microsoft SEAL
* mimalloc
* Mixed Reality Toolkit
* ML.NET
* mod_mono
* Mono
* MonoDevelop
* MSBuild
* MsQuic
* Neural Network Intelligence
* npm
* NuGet
* OneFuzz
* Open Management Infrastructure
* Open Neural Network Exchange
* Open Service Mesh
* Open XML SDK
* Orleans
* Playwright
* ProcDump
* ProcMon
* Python Tools for Visual Studio
* R Tools for Visual Studio
* RecursiveExtractor
* Roslyn
* Sandcastle
* SignalR
* StyleCop
* SVNBridge
* T2 Temporal Prover
* Text Template Transformation Toolkit
* TLA+ Toolbox
* U-Prove
* vcpkg
* Virtual File System for Git
* Voldemort
* VoTT
* Vowpal Wabbit
* Windows App SDK
* Windows Communication Foundation
* Windows Driver Frameworks
* KMDF
* UMDF
* Windows Forms
* Windows Presentation Foundation
* Windows Template Library
* Windows UI Library
* WinJS
* WinObjC
* WiX
* XDP for Windows
* XSP
* xUnit.net
* Z3 Theorem Prover

Operating systems|

* MS-DOS (v1.25, v2.0 & v4.0)
* Barrelfish
* SONiC
* Azure Linux

Other|

* ChronoZoom
* Extensible Storage Engine
* FlexWiki
* FourQ
* Gollum
* Project Mu
* ReactiveX
* SILK
* TLAPS
* TPM 2.0 Reference Implementation
* WikiBhasha
* Windows Subsystem for Linux

Licenses|

* Microsoft Public License
* Microsoft Reciprocal License

Forges|

* CodePlex
* GitHub

Related|

* .NET Foundation
* F# Software Foundation
* Microsoft Open Specification Promise
* Open Letter to Hobbyists
* Open Source Security Foundation
* Outercurve Foundation

Category

* v
* t
* e

Microsoft Research (MSR)

Main
projects|

| Languages, compilers|

* Bartok
* Bosque
* Cω
* F*
* Lean
* P
* Project Verona
* Phoenix
* Polyphonic C#
* SecPAL

|

Distributed–grid computing|

* BitVault
* Confidential Consortium Framework
* DeepSpeed
* Orleans

Internet, networking|

* AjaxView
* Avalanche
* Conference XP
* Gazelle
* HoneyMonkey
* Penny Black
* Wallop
* WikiBhasha

Other projects|

* Automatic Graph Layout
* Cognitive Toolkit
* Digits
* Holoportation
* IllumiRoom
* Image Composite Editor
* Infer.NET
* LightGBM
* LiveStation
* MyLifeBits
* Neural Network Intelligence
* NodeXL
* OneFuzz
* PhotoDNA
* SEAL
* SLAM
* T2 Temporal Prover
* WorldWide Telescope
* Z3 Theorem Prover

Operating systems|

* Barrelfish
* HomeOS
* Midori
* Singularity
* Verve

APIs|

* Accelerator
* Dryad
* Joins
* mimalloc

Launched as products|

* C#
* Comic Chat
* Detours
* F#
* Sideshow
* PixelSense (TouchLight)
* SenseCam
* ClearType
* Group Shot
* Allegiance
* TrueSkill
* Songsmith
* Xbox
* Kinect

MSR Labs
applied
research|

| Live Labs|

| Current|

* Pivot
* Seadragon
* Deep Zoom

|

Discontinued|

* Deepfish
* Listas
* Live Clipboard
* Photosynth

FUSE Labs|

* Docs.com
* Kodu

Other labs|

* Academic Search
* adCenter Labs
* Office Labs

Category
*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template