Downloads¶
Binaries, and where each one comes from.
Two rules decide what is hosted here and what is only linked:
- What we build ourselves is hosted here — it exists nowhere else.
- What already exists publicly elsewhere is linked there — a second copy would be a second thing that can drift.
There is also an internal mirror on forgejo. It resolves to a private address
(10.30.38.20), so it works inside the HSD network and nowhere else; the links
on this page are the public ones.
zqel¶
Standalone builds. No Python installation is needed: the interpreter, the
contracts, and the pinned Z3 travel inside the archive. Unpack and run
zqel/zqel (zqel\zqel.exe on Windows).
Withdrawn while #534 is open. On 2026-09-20 the
zqelfolder on R2 was deleted so that nothing with incomplete licence notices could be downloaded (#554). Measured the same day, anonymously, byHEAD: 8 of 8 promised addresses answer 404.That original reason is settled. As of 2026-09-23 the licence full texts travel inside the archive —
licenses/nativ/, named per component inNOTICE.txt— and the owner has decided that they satisfy the distribution obligation. Provenance is complete on all three platforms: Linux 39/39, macOS 57/57, Windows 33/33. No licence identifier is printed, on purpose: on Debian it would be read heuristically from a free-form copyright file, on Homebrew it is a formula assurance, and in one column the guess would look like the assurance.The delivery hold was lifted on 2026-09-24 (owner's decision). What is left is mechanical: each address is filled by its own publishing workflow, and none of them has run since. The manifest names the responsible one per file —
nightly-build-windows,nightly-build-macos,publish-linux-tarballfor the Linux tarball andvscode-extensionfor the VSIX. This page starts handing out an address only once that address answers anonymously, because an address that 404s is worse than none.The move off R2 (#534) is still open: building stays on forgejo, delivery moves to GitHub releases.
The macOS archive is not signed with an Apple Developer ID and is not notarised, and it will be published that way (owner's decision, 2026-09-23). macOS may therefore warn about it or refuse to open it. This page said the archive was waiting on signing; that stopped being true on that date. #538 and #580 track the signing pipeline — they are no longer what holds the archive back.
The builders are unchanged and still in the tree. These are pending, not discarded — built, with their producer in place, waiting for the responsible workflow to fill the address.
| Platform | File | Sidecar | State |
|---|---|---|---|
| Linux x86_64 | zqel-latest-linux-x86_64.tar.gz |
….sha256 |
published |
| Windows x86_64 | zqel-latest-windows-amd64.zip |
….sha256 |
published |
| macOS arm64 | zqel-latest-macos-arm64.tar.gz |
….sha256 |
published |
Per-commit builds are kept under https://dl.zqel.org/zqel/nightly/<full-commit>-<platform>/
for Windows and macOS. The Linux nightly no longer writes a dated
address: it publishes one immutable address per commit,
zqel/nightly/<full-commit-sha>-linux-x86_64/. A dated prefix is not
unique — two runs on one day overwrite each other — and it cannot be
quoted in a finding.
VS Code extension¶
One .vsix for every platform. It does not carry a zqel binary: it looks
for an installed zqel on PATH (or at zqel.serverPath) and starts it as
zqel lsp. Shipping the binary inside would put a second copy of the prover
pin somewhere nobody checks.
| File | Sidecar | State | |
|---|---|---|---|
| Extension | zqel-latest.vsix |
….sha256 |
published |
Install it with code --install-extension zqel-latest.vsix. Check the
sidecar first — it names the file it sits next to, so sha256sum -c
zqel-latest.vsix.sha256 works as written (#403).
Measured 2026-09-15, fetched back anonymously from the public address:
550 966 B, seven files, no node_modules and no sources inside. The bundled
JavaScript built on linux/x64 is byte-identical to the same build on
mac/arm64 — the extension is genuinely one artifact, not one per machine.
Distribution packages¶
| Distribution | Latest |
|---|---|
| Debian, Ubuntu | not published — see below (#370) |
| Fedora, RHEL, openSUSE | not published — see below (#370) |
These used to be listed only as a name pattern under the dated prefix —
zqel_<version>_amd64.deb under zqel/nightly/<YYYY-MM-DD>/. Since the
storage serves no directory listings, that asked the reader to guess the date
and the version. Two guesses are not a download.
As of 2026-09-17 they are not produced at all: the Linux nightly builds and
publishes a .tar.gz with a SHA256 sidecar, and nothing else. The sentence
here used to say the dated files were still published — that stopped being
true the moment the .deb/.rpm step was removed, which is exactly the kind
of claim nobody checks from the side it is read from.
Both declare Nix as recommended, not required. zqel does not need Nix — it
needs the provers, and Nix is the most convenient way to get exactly the pinned
ones. A hard dependency would make zqel uninstallable on every system without a
Nix package, for a capability compiling does not need at all. After installing,
zqel doctor says which capability each missing tool unlocks and how to get it.
The packages carry the standalone build, so the pinned Z3 travels with them:
zqel toolchain --json will say so.
Linux x86_64 — published 2026-09-16, and what it was measured against
Supported and tested: Debian GNU/Linux 13 (trixie), x86_64, glibc 2.41.
The support baseline is glibc 2.41 or newer. Older glibc versions and other
Linux distributions are currently unsupported, even if this binary
happens to run there — measured on Ubuntu 24.04 (glibc 2.39) it aborts
with *** stack smashing detected ***, although its highest ELF
requirement is only GLIBC_2.38. A requirement is not a guarantee.
It once had a commit-bound address under zqel/release/, described here
as immutable. That address answers 404 today (measured 2026-09-23),
so the word was wrong: an address is only immutable while someone keeps
it, and nobody was measuring this one. No address is handed out here
until the new delivery path stands (#534, #622).
What identifies the archive is its hash, and that does not move:
commit d10c4d5e4c0f2949f3af95fa9866a1001394f24b, linux-x86_64
78 213 392 bytes
sha256 d4a4fd542f1ebb83c37d624f910014e872051953e6ce042fc6e32d1a458344ce
latest is navigation; the address above is the identity. Both were
fetched anonymously from outside and checked byte for byte:
Both were fetched anonymously from outside, on 2026-09-16, and
sha256sum -c on zqel-latest-linux-x86_64.tar.gz.sha256 answered OK.
The commands are not reproduced here with their addresses: those addresses
are pending and would now 404, and a reader copying a dead
command learns nothing about what the run actually measured.
What the acceptance ran on a separate trixie host with no /nix and no
compiler, on the unpacked archive, in a sparse environment: z3_pinned=true
with the bundled libz3; a real compile that verified two output
properties; all three shipped stdlib/examples from a foreign directory;
initialize answered over LSP; no .py, .pyi or .pyw of ours; and
across all 42 ELF objects no /nix interpreter, no absolute RPATH and no
unresolvable dependency.
.deb and .rpm are not built at all
Only the tarball is released, with a SHA256 sidecar beside it. That is the whole list, and it is a decision rather than a backlog: on 2026-09-16 the owner settled on the tarball and nothing else.
This paragraph used to say the packages "are built but have never been installed and started by any gate (#453)", and that they would stay unlisted "until a gate installs and runs them". Both sentences described the world before #453 — and the second one read like a promise that they were coming back. Measured on 2026-09-17, with a denominator:
tools/build_packages.py, occurrences in the WHOLE tree outside itself: 3
- its own usage line, in its own header comment
- a test that reads its SOURCE (it never runs it)
- a comment in nightly-build.yml
workflows that EXECUTE it: 0 of 23
anything else in the tree that can build a package format: nothing
(Two earlier sweeps of mine hit .deb inside snapshot.debian.org in apt
source lines — a false positive of the pattern, not a package build.)
docs/downloads-manifest.json now carries these two entries as
verworfen, not pending. pending means "coming"; these are not.
The entries stay rather than being deleted, so the reason remains findable.
macOS arm64 — published again 2026-09-17, and what it was measured against
Supported and tested: macOS 15.0 or newer, arm64. That is the highest version any Mach-O object in the archive asks for, measured over all 58 of them.
This page linked a macOS archive for a few hours on 2026-09-15 and then
took it down. The reason was written here and still holds for that
archive: it was built at 11:38 GMT, the encoding fix (#408) was merged at
19:25 GMT, and an archive cannot carry a fix that is younger than it is.
Under LC_ALL=C it died on the first command anyone types:
LC_ALL=C ./zqel/zqel --help -> exit 1
UnicodeEncodeError: 'ascii' codec can't encode '—'
This is a different archive. It comes from run 4472
(nightly-build-macos.yml) on commit 172256ed, and 9c5bb2aa — the
merge that brought #408 — is an ancestor of it. The same measurement, on
the archive now published, fetched anonymously from outside:
$ shasum -a 256 zqel-latest-macos-arm64.tar.gz
9f3957b0389bc83b360df59d9e6bd66c7bc26e05e7f39daad0368c4e228d8e51
$ env -i PATH=/usr/bin:/bin LC_ALL=C LANG=C ./zqel/zqel --help
exit 0, 1371 bytes, nothing on stderr
It was then accepted at the unpacked archive with
tools/abnahme_macos.sh, which clears the Nix store out of PATH first —
the same gate chain the build itself runs through verify_package_starts
before anything is uploaded:
sha256 recomputed after transport ok
toolchain --json, z3_pinned ok
a real compilation with the solver ok UseDot4.zqel -> 47 lines ST
all three stdlib examples,
--target check --profile float64,
from a foreign directory ok
LSP initialize answers with capabilities ok
no .py of ours in the archive ok
58 Mach-O objects, none with a load
name from the Nix store ok
highest macOS version required 15.0
One gate falls: TripLatch.zqel, and it falls frozen on Linux in exactly
the same way (#469). It is a library module, not one of the three examples
the archive promises.
The initialize handshake is named here on purpose: the same run failed on
Windows at precisely that point on 2026-09-15 (#406), and six otherwise
identical checks were green. A gate chain that does not include it would
have called that archive good.
There is no permanent commit-bound address for macOS. Linux keeps one
under zqel/release/<commit>-linux-x86_64/; the macOS workflow writes only
zqel/staging/<commit>-macos-arm64/ (which expires, #430) and a dated
prefix. Measured: zqel/release/172256ed…-macos-arm64/ answers 404.
The dated copy does exist and carries the identical bytes:
zqel/nightly/<full-commit>-macos-arm64/zqel-nightly-<date>-macos-arm64.tar.gz
It is written as a pattern here on purpose: a literal link would be a promise about one build, and the gate that checks this page rejects addresses no workflow produces.
That prefix changed on 2026-09-17 (#442). It used to be
zqel/nightly/<YYYY-MM-DD>/ — a date, not an identity. Two runs on the
same day wrote the same objects, and on 2026-09-16 two macOS runs on
different commits sat in the queue together; only cancelling one by hand
prevented the collision (#436). It then happened for real, to the
extension (#491). A permanent address now carries the full commit;
latest remains the only deliberately moving one.
A dated prefix is not an immutable one, though: two runs on the same day
overwrite each other (#442). Until macOS gets a release address, latest
and the dated copy are what there is, and this page says so rather than
implying an identity that does not exist.
What the archive carries
PIN.txt names the archived Z3 the build is bound to — by artifact hash,
not by version number. The build refuses to publish unless the binary
compiles the example programmes and verifies their properties first.
Tools we build¶
Two tools had no Windows build anywhere: MSYS2 carries neither, and both upstreams publish source only. So we build them, from a pinned source, with the same version the development shell uses on Linux and macOS — a prover that differs per platform would be a prover you cannot compare across platforms.
| Tool | Windows x86_64 | Source |
|---|---|---|
| Gappa 1.4.0 | installer · zip | gappa-1.4.0.tar.gz |
matiec 0.1 (7949c0b) |
installer · zip | matiec-7949c0b.tar.gz |
Both packages carry their licence texts, a NOTICE.txt naming every bundled
library with its licence, and a SOURCES.txt saying where each piece of
compiled source came from. The source archive sits beside the binary, in the
same directory, so the answer to "where is the source" does not point at
someone else's server.
They are linked dynamically against GMP, MPFR and the GCC runtime, and those libraries ship beside the executable rather than inside it. That is deliberate: the LGPL asks that the library can be replaced, and a DLL next to the binary can be.
Tools we mirror¶
These we did not build — they are byte-for-byte the upstream releases, hosted
here so that everything a user needs sits at one address. Each carries a
.notice.txt beside it naming the upstream URL, the checksum, and what the
licence asks of anyone passing it on. Nothing is repacked: repacking would turn
passing something on into modifying it, and different obligations would apply.
| Tool | Platform | |
|---|---|---|
| cvc5 1.2.0 | Windows x86_64 | zip · notice |
| CBMC 6.4.0 | Windows x86_64 | msi · licence |
| Kani 0.67.0 | Linux x86_64 | tar.gz |
| Kani 0.67.0 | Linux arm64 | tar.gz |
| Kani 0.67.0 | macOS x86_64 | tar.gz |
| Kani 0.67.0 | macOS arm64 | tar.gz |
The versions are the ones the development shell uses — cvc5 1.2.0 and CBMC 6.4.0, not the newest releases. A prover that differs per platform is a prover whose results you cannot compare across platforms.
Kani publishes no Windows build, and neither do we: it is a rustc driver, and
porting it is upstream work rather than packaging work.
The upstream projects remain the source. If a copy here ever disappears, these are the originals: cvc5, CBMC, Kani.
Tools we do not ship at all¶
| Tool | Why |
|---|---|
| Z3 | Pinned by artifact hash and already inside the zqel archive; see PIN.txt |
| Why3, Creusot | Source only; on Linux and macOS they come from the development shell |
Verifying what you downloaded¶
Every artifact has a .sha256 beside it.
$ sha256sum -c zqel-latest.vsix.sha256
zqel-latest.vsix: OK
On Windows:
> Get-FileHash zqel-latest-windows-amd64.zip -Algorithm SHA256
The checksum tells you the file arrived intact. It does not tell you which Z3
the build was bound to — PIN.txt inside the archive does that, and the binary
checks the library it actually loads against it.