At a Glance
| Applications | SMT Solver Theorem Prover |
| Developers | Microsoft Research |
| Inputs | SMTLIB2 DIMACS |
| Interfaces | CLI Python Rust C C++ Java .NET Online |
| Licenses | MIT |
| Maintenance | Actively Maintained |
Description
Z3 is a theorem prover developed by Microsoft Research, widely used for SAT & SMT solving and related formal verification tasks. It supports a variety of input languages, including SMT-LIB, and offers APIs for multiple programming languages. Z3 is open source under the MIT license and is actively maintained, making it a popular choice for research and industrial applications in software and hardware verification.
APIs and Bindings
Z3 is available through several interfaces, making it a convenient option to build into a project.
- C API: Z3 C API Reference
- C++ API: Z3 C++ Namespace Reference
- .NET API: Z3 .NET Namespace Reference
- Java API: Z3 Java API Reference
- Python bindings: z3-solver PyPI package (Documentation)
- Rust bindings: z3 crate on crates.io
Publications
- Z3: An Efficient SMT Solver (March 2008) by de Moura, Leonardo et. al. | Appears in TACAS | Published by Springer, Berlin, Heidelberg | 10.1007/978-3-540-78800-3_24
Updated