It's reference-counted at the boundaries. See https://github.com/Z3Prover/z3/blob/daf2506b6002149d531cb6c9...
In A Dumb Introduction to Z3 (2025)Z3Prover
z3
C++2015–2026
Z3Prover / z3
z3
The Z3 Theorem Prover
42Distinct people
48Mentions
1Explicit recommenders
12.9KGitHub stars
What to know before exploring
What it is
The Z3 Theorem Prover
GitHub
Where it is used
What people are saying
1) For the "how to get started with formal verification outside academia", I'll first get the case of "in/for production" out of the way: a) "use Z3[0] with some…
namibj used a recommendation phrase. One indexed comment matches. This is a phrase match, not a verdict.
No classified warning is attached to this page. Read the discussions before treating silence as approval.
Also in these discussions
- argotorg/solidity · linked in 2 of the same discussions
- dotnet/csharplang · linked in 2 of the same discussions
Mentioned in the same Hacker News threads. That is not proof they are substitutes.
This week on Hacker News
Nov 7–Nov 14 UTC · Direct repository links and separately labeled related project stories. Indexed through 11/14/2026, 3:56:07 PM UTC.
No direct repository links were found in the indexed HN discussions over the past seven days. Older discussions are available below.
Mentions over time
HN mentions by year48 dated mentions
Observed mentions: 2015-03-26 19:02:35 UTC to 2026-04-18 18:51:51 UTC.
* An incomplete calendar period is marked with an outlined bar. Its count is not directly comparable with a full period.
Counts come from the repository’s dated source evidence. Index cutoff: 2026-11-02 08:16:59 UTC.
View mention counts and date ranges
| Period | Start (UTC) | End (exclusive, UTC) | Mentions | Submissions | Comments |
|---|---|---|---|---|---|
| 2015 | 2015-01-01 00:00:00 UTC | 2016-01-01 00:00:00 UTC | 4 | 2 | 2 |
| 2016 | 2016-01-01 00:00:00 UTC | 2017-01-01 00:00:00 UTC | 3 | 1 | 2 |
| 2017 | 2017-01-01 00:00:00 UTC | 2018-01-01 00:00:00 UTC | 3 | 1 | 2 |
| 2018 | 2018-01-01 00:00:00 UTC | 2019-01-01 00:00:00 UTC | 5 | 3 | 2 |
| 2019 | 2019-01-01 00:00:00 UTC | 2020-01-01 00:00:00 UTC | 7 | 1 | 6 |
| 2020 | 2020-01-01 00:00:00 UTC | 2021-01-01 00:00:00 UTC | 2 | 0 | 2 |
| 2021 | 2021-01-01 00:00:00 UTC | 2022-01-01 00:00:00 UTC | 5 | 1 | 4 |
| 2022 | 2022-01-01 00:00:00 UTC | 2023-01-01 00:00:00 UTC | 4 | 0 | 4 |
| 2023 | 2023-01-01 00:00:00 UTC | 2024-01-01 00:00:00 UTC | 4 | 0 | 4 |
| 2024 | 2024-01-01 00:00:00 UTC | 2025-01-01 00:00:00 UTC | 4 | 2 | 2 |
| 2025 | 2025-01-01 00:00:00 UTC | 2026-01-01 00:00:00 UTC | 5 | 2 | 3 |
| 2026 (partial) | 2026-01-01 00:00:00 UTC | 2027-01-01 00:00:00 UTC | 2 | 1 | 1 |
From the project README
An excerpt from the repository, fetched Nov 13, 2026.
Read the project’s introduction
Z3
Z3 is a theorem prover from Microsoft Research.
It is licensed under the MIT license. Windows binary distributions include C++ runtime redistributables
If you are not familiar with Z3, you can start here.
Pre-built binaries for stable and nightly releases are available here.
Z3 can be built using CMake, vcpkg, or Bazel.
It provides bindings for several programming languages.
See the release notes for notes on various stable releases of Z3.
Build status
Pull Request & Push Workflows
WASM Build
Windows Build
CI
Finite-Field Regressions
Determinism Linter
Solver Determinism
Pulse Native Checker Build
Scheduled Workflows
Android Build
Nightly Build
Cross Build
F* Master Build
MSVC Static
MSVC Clang-CL
Build Z3 Cache
Memory Safety
Mark PRs Ready
Clang-Tidy Warning Report
Manual & Release Workflows
Documentation
Release Build
WASM Release
Pyodide Wheel (PyPI)
Specialized Workflows
Nightly Validation
Copilot Setup
Agentics Maintenance
Dispatch NFV Formal Audit
Follow-up / Comment Workflows
Determinism Linter PR Comment
Solver Determinism PR Comment
Pulse Checker Regressions
Agentic Workflows
API Coherence
Code Simplifier
Release Notes
Workflow Suggestion
Academic Citation
Issue Backlog
Memory Safety Report
SMTLIB Benchmark Finder
F* NFV PR Audit
A3 Python Analysis
Code Conventions
Compare Stats Anomaly Reporter
CSA Analysis
Tactic-to-Simplifier
Building Z3 using CMake
CMake is the preferred and most fully featured build system for Z3. A basic
release build is:
cmake -S . -B build -DCMAKE_BUILD_TYPE=Release
cmake --build build --parallel $(nproc)
See README-CMake.md for build options, language bindings,
installation, and instructions for consuming Z3 from another CMake project.
Z3 uses C++20. On Windows, the recommended version of Visual Studio is
therefore VS2019 or later; CMake with the Ninja or Visual Studio generator
builds Z3 from the Visual Studio Command Prompt.
Security Features (MSVC): When building with Visual Studio/MSVC, a couple of security features are enabled by default for Z3:
Control Flow Guard (/guard:cf) - enabled by default to detect attempts to compromise your code by preventing calls to locations other than function entry points, making it more difficult for attackers to execute arbitrary code through control flow redirection
Address Space Layout Randomization (/DYNAMICBASE) - enabled by default for memory layout randomization, required by the /GUARD:CF linker option
These can be disabled using cmake -S . -B build -DZ3_ENABLE_CFG=OFF if needed
Use sudo cmake --install build to install to the system prefix (or set
-DCMAKE_INSTALL_PREFIX= at configure time for a custom prefix). To uninstall,
consult your platform's package manager, or, since CMake tracks installed
files in build/install_manifest.txt, remove those files directly.
Building Z3 using vcpkg
vcpkg is a full platform package manager. To install Z3 with vcpkg, execute:
git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3
Building Z3 using Bazel
Z3 can be built using Bazel. This is known to work on
Ubuntu with Clang (but may work elsewhere with other compilers):
bazel build //...
Dependencies
Z3 itself has only few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading.
It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained
multi-precision functionality. Python is required to build Z3. Building Java, .NET, OCaml and
Julia APIs requires installing relevant toolchains.
Z3 bindings
Z3 has bindings for various programming languages.
.NET
You can install a NuGet package for the latest release Z3 from nuget.org.
With CMake, use the -DZ3_BUILD_DOTNET_BINDINGS=ON option.
See examples/dotnet for examples.
C
These are always enabled.
See examples/c for examples.
C++
These are always enabled.
See examples/c++ for examples.
Java
With CMake, use the -DZ3_BUILD_JAVA_BINDINGS=ON option.
For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code) and troubleshooting, see the Java IDE Setup Guide.
See examples/java for examples.
Go
With CMake, use the -DZ3_BUILD_GO_BINDINGS=ON option. Note that Go bindings use CGO and require a Go toolchain (Go 1.20 or later) to build.
See examples/go for examples and src/api/go/README.md for complete API documentation.
OCaml
With CMake, use the -DZ3_BUILD_OCAML_BINDINGS=ON option.
See examples/ml for examples.
Python
You can install the Python wrapper for Z3 for the latest release from pypi using the command:
pip install z3-solver
With CMake, use the -DZ3_BUILD_PYTHON_BINDINGS=ON option.
Note that it is required on certain platforms that the Python package directory
(site-packages on most distributions and dist-packages on Debian-based
distributions) live under the install prefix. If you use a non-standard prefix
you can use the -DCMAKE_INSTALL_PYTHON_PKG_DIR= option to change the Python
package directory used for installation. For example:
cmake -S . -B build -DCMAKE_INSTALL_PREFIX=/home/leo -DZ3_BUILD_PYTHON_BINDINGS=ON -DCMAKE_INSTALL_PYTHON_PKG_DIR=/home/leo/lib/python3.x/site-packages
If you do need to install to a non-standard prefix, a better approach is to use
a Python virtual environment
and install Z3 there.
Under Windows, recall to build inside the Visual C++ native command build environment.
Note that the build/python/z3 directory should be accessible from where Python is used with Z3
and it requires libz3.dll to be in the path.
virtualenv venv
source venv/bin/activate
cmake -S . -B build -DCMAKE_INSTALL_PREFIX=$VIRTUAL_ENV -DZ3_BUILD_PYTHON_BINDINGS=ON
cmake --build build --parallel $(nproc)
cmake --install build
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_s
Read the full README on GitHubWhat Hacker News says
48 sourcesShow HN: Sigil – A new programming language for AI agents
I've been working on a new programming language for AI agents. I would love your input on what makes programming languages good for AI agents, especially syntax, compiler, and tooling that could help AI agents write code.
What makes Sigil good for coding agents?
I've turned conventions into compiler rules whenever possible. The compiler owns the canonical printer and every AST has one accepted textual representation. For almost every syntax feature I tried to save tokens.
Order and naming conventions are enforced. No more "I think this argument is important so it should come first." Most things are alphabetical. Declarations are categorized and ordered alphabetically; parameters, effects, and record fields are alphabetical too. Types are UpperCamelCase. Everything else is lowerCamelCase, including file names.
No nulls. No undefined.
Bidir
Read the rest
ectional type checking.
No shadowing.
Fat stdlib (still in progress).
`sigil debug` supports replay, stepping, watches, and breakpoints.
`sigil inspect` lets coding agents query the compiler directly, including proof surfaces.
Solver-backed refinements and contracts. Different languages already choose different numeric surfaces: byte, short, smallint, unsigned integers, etc. Sigil pushes that one step further: domain constraints can also define types. `where` lets a named type carry a predicate, and `requires` / `ensures` let functions carry proof obligations across call boundaries.
Here is a contrived example from the roguelite:
t InventoryCount=Int where value≥0
λspendArrow(arrows:InventoryCount)=>InventoryCount
requires arrows>0
ensures result≥0
=arrows-1
Under the hood this is backed by Z3: https://github.com/z3prover/z3 But the surface stays ordinary Sigil syntax. There are no proof scripts and no user-facing SMT language.
No imports, rooted references only. In some languages you can import code and have name clashes, so there are many ways to specify imports. Sigil eliminates all of that by only using rooted references. I think this reduces agent churn because when the model sees a line, it does not have to go hunt for an import statement.
Service dependencies are declared in `src/topology.lib.sigil`, and environment bindings live in `config/<env>.lib.sigil`.
The language has special syntax for tests and they are run in parallel. Every project `src/*.lib.sigil` function must be tested, and if a function can return multiple cases, tests should exercise all of them. "World" is Sigil's model for effects. That is how mocks work: swap one effect for another and make assertions without exercising real external systems.
The compiler toolchain is written in Rust, and Sigil outputs to TypeScript, with a Foreign Function Interface to Node.js. See some small projects here https://inerte.github.io/sigil/projects/ - the Flashcards is useful to learn about Sigil features https://inerte.github.io/sigil/projects/sigil-flashcards/dem...
Caveat: I did NOT type a single line of code for the compiler toolchain. It was all generated with Claude Code and Codex. I run both with permissions dangerously skipped. This actual post I hand crafted every word.
There is also a toy roguelite written in Sigil. It is a work in progress, but it is proof that Sigil can support nontrivial project code. You can play with `pnpm sigil:run:roguelike`.
Repository: https://github.com/inerte/sigil
Website: https://inerte.github.io/sigil/
And I would love if you can find ways to lock down LLM / user programs even more. In Sigil, there should be only one way to do anything.
We care about Z3 because it is a Satisfiability Modulo Theories (SMT) solver.
Satisfiability: In 1971, Stephen A. Cook established that Boolean satisfiability, given an arbitrary Boolean formula whether an assignment to its variables exists that evaluates true, is NP-complete.
https://dl.acm.org/doi/10.1145/800157.805047
Translating between NP-complete problems is at most a polynomial (“fast”) amount of work, so every improvement gained on satisfiability (whose worst case is exponential rather than polynomial time complexity) benefits all other NP-complete problems, and thus the rest of NP.
Modulo Theories: We can think of SMT as a high-level language that automates encoding of other problems into raw Boolean formulas. Applications built on Z3 outsource search by encoding problems via one or more theories and then decoding results back to
Read the rest
the problem domain at hand.
The benefits of doing this are (1) using an existing robust, well-tested suite of algorithms where (2) lots of research effort is concentrated and (3) improvements to Z3 improve your problem’s results more-or-less for free. According to Microsoft, “Z3 is used in a wide range of software engineering applications, ranging from program verification, compiler validation, testing, fuzzing using dynamic symbolic execution, model-based software development, network verification, and optimization.”
https://www.microsoft.com/en-us/research/project/z3-3/
See also:
https://github.com/Z3Prover/z3
Wouldn't this be an optimization problem, that's to say, something like z3 should be able to do - [1], [2]?
I was about to suggest probabilistic programming, e.g., PyMC [3], as well, but it looks like you want the optimization to occur autonomously after you've specified the problem - which is different from the program drawing insights from organically accumulated data.
[1] https://github.com/Z3Prover/z3?tab=readme-ov-file
[2] https://microsoft.github.io/z3guide/programming/Z3%20Python%...
[3] https://www.pymc.io/welcome.html
In Let's Take Esoteric Programming Languages SeriouslyFor what it's worth, the way 14MV does hints is probably by just throwing the board into Z3 (https://github.com/Z3Prover/z3) or some other constraint solver. Microsoft has already done all the hard work for you.
In Making Explainable MinesweeperIf you want to use Z3 with a .NET language, there is also this very useful file with examples of how to use the bindings:
https://github.com/Z3Prover/z3/blob/master/examples/dotnet/P...
The examples are in C#, but easy to adapt to other languages. I found them quite useful to write a program for symbolic execution in F# that calls Z3 to simplify conditionals, here is its interface to Z3:
https://github.com/constructum/asm-symbolic-execution/blob/m...
The bindings are perhaps a bit cumbersome, but rather easy to understand and work very well. Once you appropriately wrap what you need, you can forget about the bindings as well as avoiding SMT-LIB completely.
In Accidentally writing a SAT solverShow HN: Allocate poker chips optimally with mixed-integer nonlinear programming
Every time I play a casual cash poker game with friends, we spend the first several minutes struggling to figure out chip denominations. I built this to automate that process.
Try it out here (the submitted link goes to the GitHub repo): https://jstrieb.github.io/poker-chipper/
It turns out that picking chip denominations optimally—such that as many chips are distributed as possible, and such that the denominations are nice—is hard (in the computational complexity sense). Upon reflection, the problem seemed to be a perfect fit for constrained optimization.
I first got a CLI prototype working with Z3 (an SMT solver with optimization capabilities https://github.com/Z3Prover/z3) in Python. Then, I cross-compiled SCIP (https://www.scipopt.org/) to web assembly, and ported my code to use SCIP instead of Z3 so it could run in the browser.
The w
Read the rest
eb interface is designed to be fast and easy to use on desktop and mobile.
I would love to answer questions and discuss design choices. I'm also open to feedback and bug reports. Thanks for taking a look!
https://github.com/Z3Prover/z3
Here is an actual description:
https://z3prover.github.io/papers/programmingz3.html#sec-int...
In Planner programming blows my mindSee https://cacm.acm.org/magazines/2023/6/273222-the-silent-revo... and also modern production rules engines like https://drools.org/
Oddly, back when “expert system shells” were cool people thought 10,000 rules were difficult to handle, now 1,000,000 might not be a problem at all. Back then the RETE algorithm was still under development and people were using linear search and not hash tables to do their lookups.
Also https://github.com/Z3Prover/z3
Note “the semantic web” is both an advance and a retreat in that OWL is a subset of first order logic which is really decidable and sorta kinda fast. It can do a lot but people aren’t really happy with what it can do.
In Ask HN: What is the current state of "logical" AI?Code correctness is a lost art. I requirement to think in abstractions is what scares a lot of devs to avoid it. The higher abstraction language (formal specs) focus on a dedicated language to describe code, whereas lower abstractions (code contracts) basically replace validation logic with a better model.
C# once had Code Contracts[1]; a simple yet powerful way to make formal specifications. The contracts was checked at compile time using the Z3 SMT solver[2]. It was unfortunately deprecated after a few years[3] and once removed from the .NET Runtime it was declared dead.
The closest thing C# now have is probably Dafny[4] while the C# dev guys still try to figure out how to implement it directly in the language[5].
[1] https://www.microsoft.com/en-us/research/project/code-contra...
[2] https://github.com/Z3Prover/z3
[3] https://github.co
Read the rest
I believe, Nim also has this functionality, although, it uses the [0]Z3Prover tool with a nim frontend [1]DrNim for proving.
[0]https://github.com/Z3Prover/z3
[1]https://nim-lang.github.io/Nim/drnim.html
In Programming languages going above and beyondLove this article and the push to build awareness of what modern SAT solvers can do.
It's worth mentioning that there are higher level abstractions that are far more accessible than SAT. If I were teaching a course on this, I would start with either Answer Set Programming (ASP) or Satisfiability Modulo Theories (SMT). The most widely used solvers for those are clingo [0] and Z3 [1]:
With ASP, you write in a much clearer Prolog-like syntax that does not require nearly as much encoding effort as your typical SAT problem. Z3 is similar -- you can code up problems in a simple Python API, or write them in the smtlib language.
Both of these make it easy to add various types of optimization, constraints, etc. to your problem, and they're much better as modeling languages than straight SAT. Underneath, they have solvers that leverage all the
Read the rest
modern CDCL tricks.
We wrote up a paper [2] on how to formulate a modern dependency solver in ASP; it's helped tremendously for adding new types of features like options, variants, and complex compiler/arch dependencies to Spack [3]. You could not get good solutions to some of these problems without a capable and expressive solver.
[0] https://github.com/potassco/clingo
[1] https://github.com/Z3Prover/z3
[2] https://arxiv.org/abs/2210.08404, https://dl.acm.org/doi/abs/10.5555/3571885.3571931
[3] https://github.com/spack/spack
Showing the 15 most recent of 48 sources. Enable JavaScript to search and browse every indexed mention.