Skip to main content

Powerful theorem proving for modern applications

Z3 is a high-performance SMT solver from Microsoft Research. Solve complex constraints, verify programs, and build intelligent systems with multi-theory reasoning.

Get startedAPI reference
11,989 GitHub stars
8 language bindings

Quick start

Get Z3 running in your project in minutes

1

Install Z3

Choose your preferred installation method based on your programming language:
pip install z3-solver
2

Create your first solver

Import Z3 and create a solver instance to start solving constraints:
from z3 import *

# Create a solver instance
solver = Solver()

# Create integer variables
x, y = Ints('x y')

# Add constraints
solver.add(x + y == 10)
solver.add(x > 5)
3

Check satisfiability and get results

Use the solver to check if constraints are satisfiable and retrieve the model:
# Check if constraints are satisfiable
if solver.check() == sat:
    # Get the model (solution)
    model = solver.model()
    print(f"Solution found: x = {model[x]}, y = {model[y]}")
else:
    print("No solution exists")

Solution found: x = 6, y = 4

Explore by language

Z3 provides native bindings for multiple programming languages

Python

Pythonic API with intuitive syntax for rapid prototyping and research

C++

High-performance API with smart pointers and operator overloading

Java

Object-oriented API for JVM-based applications

.NET

Comprehensive API for C# and F# with NuGet package support

JavaScript/TypeScript

WebAssembly-powered solver for browser and Node.js

Go

CGO-based bindings for Go applications

Key features

Powerful capabilities for constraint solving and theorem proving

Multi-theory reasoning

Support for arithmetic, bitvectors, arrays, datatypes, strings, floating-point, and finite sets

Optimization solver

MaxSMT and weighted constraint solving with Z3’s optimize component

Tactics & strategies

Customizable solving strategies with over 100 built-in tactics

Incremental solving

Efficient solving with push/pop scopes for incremental constraints

Fixedpoint engine

Datalog and Horn clause solving for program analysis

Production-ready

Battle-tested in industrial verification and analysis tools

Popular use cases

See how developers use Z3 to solve real-world problems

Program verification

Verify correctness properties of software systems using SMT-based symbolic execution and formal methods.

Explore example

Constraint solving

Solve complex combinatorial problems like scheduling, planning, and configuration using declarative constraints.

Explore example

Symbolic execution

Explore execution paths symbolically to find bugs, generate test cases, and analyze program behavior.

Explore example

Model checking

Verify temporal properties and safety invariants of hardware and software systems at scale.

Explore example

Ready to start solving?

Join thousands of developers and researchers using Z3 to solve complex constraint problems and verify critical systems.

Get startedView on GitHub