Installing zqel¶
The short version: download one archive, unpack it, run it. There is no Python to install and no solver to configure — the interpreter, the standard library and the pinned Z3 travel inside.
Everything after that is optional, and each extra tool buys exactly one capability. The table further down says which.
1. Get the binary¶
Why every curl below carries -f
Without -f, curl saves an HTTP error body to the output file and exits
successfully. A missing download then arrives as a 27 KB HTML page named
…tar.gz, and the first thing you hear about it is
gzip: stdin: not in gzip format
tar: Error is not recoverable: exiting now
which points at your archive tool instead of at the 404. Measured on
2026-09-14 — that is exactly how it went. -f makes curl fail loudly on
the status code instead.
Linux x86_64¶
There is no Linux package yet, and these instructions used to hand you a
curl for one. Measured 2026-09-15, anonymously from outside: the tarball,
its .sha256, the .deb and the .rpm all answer with 404. They never
existed.
No run has ever produced a Linux package. The standalone build has never
started on a host without /nix — the ELF interpreter of the Nuitka binary
points into /nix/store, so the kernel cannot begin to execute it anywhere
else (#348). The replacement route, building with Nuitka under Nix and then
wrapping the finished closure with nix bundle, is #367.
Until a run succeeds and a host without /nix has been shown to run the
result, there is nothing here to download. Tracking issue #370.
In the meantime, on Linux: nix run github:mprotogerakis/LoLa#zqel -- --help,
or the development shell described below.
macOS arm64¶
There is no macOS package. Not an oversight — there is no macOS build machine,
so nothing on macOS could pass the check the other two packages must pass
before they are published (zqel toolchain --json has to confirm the binary
knows it is a shipped build and loads the pinned prover). An archive built by
hand would look identical and mean less, so there is none. Tracking issue #330.
On macOS, run from source — see running from source below.
Windows x86_64¶
Withdrawn — no address is handed out here. zqel-latest-windows-amd64.zip
is built and verified on every nightly, but delivery is on hold (#534, #538,
580) and the old address answers 404. Downloads carries the¶
current state and will carry the address again when delivery resumes.
Once it does, the steps are:
PS> Get-FileHash .\zqel.zip -Algorithm SHA256 # gegen die .sha256 daneben halten
PS> Expand-Archive zqel.zip -DestinationPath .
PS> .\zqel\zqel.exe --help
Put the directory on your PATH if you want to type zqel rather than a path.
Keep the folder together: the binary reads stdlib/ and the Z3 library beside
it.
Check what you got¶
$ zqel toolchain
machine x86_64
pin_enforced True
platform Linux
shipped_build True
z3_library …/zqel/z3/lib/libz3.so
z3_library_sha256 30c884adb8131bfb…
z3_pinned True
z3_library_sha256 is the library that was actually loaded, not the one a
manifest claims. In a downloaded build pin_enforced is always True — there
is no switch, and a build whose solver is not the pinned one refuses to run.
2. Ask the binary what is missing¶
$ zqel doctor
It lists every capability, whether the tool behind it is usable here, and what to do if it is not — with the command, not a link to go hunting for.
[+] gappa MATCHED prove float64 round-off bounds
[-] cbmc MISSING re-check the generated C with a model checker
cbmc not on PATH
-> from the development shell; version 6.4.0
Two things it deliberately does not do. It never says PROVED — it describes
an environment and closes with nothing was compiled and nothing was proved,
so that "all green" here can never be read as "my proofs are complete". And it
changes nothing: it names the command that would help and does not run it.
zqel doctor --require gappa exits non-zero if that one capability is not
usable, which is the form for a CI preflight.
3. What the extra tools buy you¶
Nothing below is needed to compile a programme and prove its properties. Each
row is one capability you do not have until the tool is on your PATH.
| You want to… | Command | Needs |
|---|---|---|
| compile and prove | zqel prog.zqel |
nothing extra |
| prove float64 round-off bounds | --profile float64 |
Gappa |
| emit Structured Text | --target st |
nothing extra |
| re-check the emitted ST on an independent toolchain | conformance tests | matiec + a C compiler |
| re-check the generated C | --proof cbmc |
CBMC |
| emit Rust | --target rust |
nothing extra |
| run a programme against a process image | zqel run |
rustc ≥ 1.70 |
| prove the Rust with a model checker | --proof kani |
Kani |
| prove the Rust deductively | --proof creusot |
Creusot + Why3 + a prover |
4. Getting the extra tools¶
Gappa¶
| Platform | Where |
|---|---|
| Windows x86_64 | installer — we build it; nothing equivalent exists upstream |
| Linux, macOS | your package manager, or the Nix development shell |
Use 1.4.0. A prover that differs between your machine and the one that produced an earlier verdict is a prover whose results you cannot compare.
matiec and a C compiler¶
| Platform | Where |
|---|---|
| Windows x86_64 | installer, plus MSYS2 for gcc |
| Linux, macOS | built by the development shell from the pinned revision |
Set MATIEC_DIR to the directory holding iec2c (iec2c.exe on Windows) and
lib/. Without a C compiler the conformance path stays skipped — zqel checks
for both and says so rather than failing halfway.
CBMC¶
Windows: cbmc-6.4.0-win64.msi.
Linux and macOS: the development shell.
CBMC on Windows is not the same CBMC
It derives its machine model from the host and uses the MSVC preprocessor by default, so a verdict there is about a different machine and a different C dialect than one obtained on Linux. Until that is pinned, treat Windows CBMC results as informational.
Rust, Kani and Creusot¶
rustc and cargo from rustup on every platform.
Kani: upstream releases or our mirror — Linux and macOS only: linux-x86_64, linux-arm64, macos-x86_64, macos-arm64.
Creusot: from source, plus Why3 and a prover.
Neither runs on Windows, for different reasons
Kani refuses, and it is right to. Its compiler builds a CBMC machine model that assumes Linux or macOS, and the platform check exists to guarantee that model is valid. Removing the check does not port the model.
Creusot builds — we got the whole workspace compiling with three small
portability fixes, and it translated 2177 examples to .coma. What is
missing is Why3. That is effort, not meaning, and it may change.
Until then both run on a Linux machine.
5. Which platform can do what¶
| Linux x86_64 | macOS arm64 | Windows x86_64 | |
|---|---|---|---|
| zqel, compile and prove | ✅ | ✅ | ✅ |
| Gappa — float64 bounds | ✅ | ✅ | ✅ (we build it) |
| matiec — ST conformance | ✅ | ✅ | ✅ (we build it) |
| CBMC | ✅ | ✅ | ⚠️ different model |
Rust, zqel run |
✅ | ✅ | ✅ |
| Kani | ✅ | ✅ | ❌ upstream refuses |
| Creusot | ✅ | ✅ | ❌ Why3 missing |
6. Running from source instead¶
If you want to change zqel rather than use it, the repository has a Nix development shell that brings every tool above in the pinned versions:
$ nix develop
$ pytest -q
That is the environment the gate runs in, and the one the binaries are built from.
What the first run costs. Measured on 2026-09-13, not estimated: of the
5518 store paths in the x86_64-linux development shell, 5239 are already
built in the public cache (94.9%). That number flatters the situation, because
what is missing is precisely the expensive part — the provers do not come from
nixpkgs but from the Creusot flake with its own pins:
| Built from source on your machine | Why it is not in the public cache |
|---|---|
cargo-creusot 0.13.0 and its dependency build |
comes from the Creusot flake, not nixpkgs |
why3 at git pin 54c92f9, why3find, alt-ergo |
a pinned revision, not the cached why3-1.8.0 |
z3 4.15.3 |
a pinned version, not the cached 4.8.17 |
cvc5 1.3.1, cvc4 1.8, cryptominisat, CoCoALib, glpk |
pulled in by the Creusot flake |
There is no binary cache to borrow: neither this flake nor Creusot's declares
a nixConfig, and Creusot's CI configures no cachix (checked at revision
318615b). So the first nix develop compiles those provers.
This is the price of pinning prover identity rather than taking whatever a
distribution currently ships. If you only want to use zqel, take the
binaries from the downloads page instead — they carry Z3 with
them, and zqel doctor will tell you what else a given capability needs.
Without cloning the repository¶
The flake is published as a tarball, so you do not need the repository — or access to any forge — to get the pinned toolchain:
$ nix develop tarball+<address>/<sha256>.tar.gz
The address is currently broken and none is handed out here.
flake-tarball.yml publishes under zqel/flake/, and that prefix answers
404 (measured 2026-09-23); bytes from an older scheme still sit under
flake/, so citing either would be citing something we do not publish. It is
fixed with the move off R2 (#534, #622).
The <sha256> is what matters and does not move: the hash is what makes a
verdict reproducible, and any latest pointer moves. Use such a pointer to
find a version, never to cite one.
The provers come from their own repository¶
The verifier toolchain — Creusot, Why3, the SMT solvers — lives in zqel-toolchain and is published separately, with a signed binary cache:
$ nix shell tarball+https://dl.zqel.org/flake/<sha256>.tar.gz#creusot-free
https://dl.zqel.org/flake/latest.json names that one. Without the cache the
first run compiles the provers; with it, the 22 store paths that
cache.nixos.org does not carry are fetched instead of built. Nix asks once
before it accepts the substituter — declining is a legitimate choice, it only
costs time.
Check it yourself. Whoever builds a distribution tests it on the machine
they built it on — with a repository beside it, a full /nix/store and their
organisation's access. Then everything works and nothing has been shown. The
probe below takes none of that for granted and sends no credentials at all:
$ curl -fsSO https://dl.zqel.org/flake/probe_public_toolchain.py
$ python3 probe_public_toolchain.py --mit-nix --frischer-store \
--url https://dl.zqel.org/zqel/flake/<sha256>.tar.gz
The probe itself is maintained in zqel-toolchain — one file, one publisher.
Point it at whichever tarball you want to check.
It checks that latest.json and the tarball are readable anonymously, that
the file name really is the SHA-256 of its content, that the archive carries
flake.nix and flake.lock, and that every input in that lock is reachable
without an account. With --frischer-store it resolves the flake in an empty
Nix store, so a hit cannot come from something the machine already had.
It also prints what it does not show: which network it ran from. That part only you can establish, by running it somewhere we have never been.