The Z3 Theorem Prover
2 days ago
- #Microsoft-Research
- #programming-languages
- #theorem-prover
- Z3 is a theorem prover from Microsoft Research licensed under the MIT license.
- Pre-built binaries for stable and nightly releases are available.
- Z3 can be built using Visual Studio, Makefile, CMake, vcpkg, or Bazel.
- Supports bindings for several programming languages including C++, Java, .NET, OCaml, and Python.
- Security features like Control Flow Guard and Address Space Layout Randomization are enabled by default in MSVC builds.
- Building Z3 requires Python and optionally GMP for multi-precision integers.
- Z3 has a default input format of SMTLIB2 and supports various foreign function interfaces.
- WebAssembly build is available on npm as z3-solver.
- Julia package Z3.jl wraps the C API of Z3.