Assurance

It covers the Linux AppImage payload only. Not the .deb, not the .rpm, not macOS, not Windows. Those platforms have published-bytes-match and build provenance, but nothing yet re-derives them from source.

Reproduction needs the published build recipe, not source alone, because one build-time value is compiled in. A third party with no recipe can still prove log inclusion — that half needs no build inputs at all — but not bit-for-bit reproduction.

Two releases were never checked. The rebuild only runs when the release workflow concludes successfully, so v1.9.0 and v1.9.1 were skipped entirely and no verdict exists for them. They are in the table, marked as such, rather than quietly omitted.

Some historical red runs were not real failures. Before commit 564353ae (16 August 2026) the workflow could report "did not reproduce" for a release that was merely not yet published into the log — the underlying check exits cleanly over an empty artifact set, so the wait loop gave up immediately and compared the rebuild against nothing. Two runs failed exactly that way (v1.9.4 and v1.9.5) and both in fact reproduced byte-identically. The reds are left in the table rather than deleted.

v1.9.3 reproduces. Its August 13 rebuild did not, and sat unexplained. Re-running exactly the same check on 17 August — same tag, same public source, no other change — landed on the same CI machine image the release had used and produced a payload byte-identical to the one in the log (07bccca8…, run 32036282718). One variable was different in August; holding it constant makes the bytes match.

What that variable was. A Linux AppImage is not purely a function of our source: the bundler copies the app's system libraries off the build machine into the bundle. GitHub rebuilds the machine image behind its ubuntu-22.04 label every few weeks and rolls it out gradually, so the release build and its rebuild — 36 minutes apart — landed on different images, and seven vendored libraries (Kerberos, SQLite, systemd, udev) came out different. Nothing built from Pollis source changed except the order of a list of content hashes inside the executable, which a compile-time dependency emits in filesystem order and which carries no meaning.

The August run stays in the table, still red, rather than being deleted or quietly recoloured: it genuinely could not perform the comparison it reported on. What changed is that the workflow now reads the machine image the release recorded, compares it against its own, and says which situation it is in — did not reproduce, build environment drifted, or no recorded recipe. All three still fail, because an inconclusive rebuild is not a passing one; only the first is a claim about the shipped binary. The full write-up, with the byte evidence, is in docs/reproducible-builds-residuals.md.

Both are bounded. TLC checks a small model — three clients, a handful of epochs — not an unbounded network, and Kani checks small input domains, not all inputs. A bug that only appears at larger scale is outside both. This is the standard trade: exhaustive over a small space beats sampled over a large one, but it is not a proof about the running system.

They cover the decision functions, not the program. The proofs range over pure functions deliberately extracted for the purpose. The database calls, the network, the MLS library and the UI around them are not verified — they are covered by ordinary tests and a nightly fuzzing soak.

One invariant has no machine-checked defence at all — that the test schema equals the production schema. It is enforced by a mechanical equality check instead, and the design doc says so.

Pollis has audited zero crates itself. supply-chain/audits.toml is empty. 858 exemption entries cover 716 crates, which is the dependency graph as it stood when the gate was switched on. What the gate actually enforces is a ratchet: no new or bumped crate can enter without a deliberate, reviewable change to that file. It is not, and should not be read as, "every dependency has been reviewed".

Duplicate-version and wildcard checks warn rather than fail. A large native tree carries transitive duplicates we do not control, so those are visible in the job log but do not block.

There is no scheduled re-scan and no automated dependency-update bot. Advisories are checked when a pull request runs or on a push to main. A newly published advisory against an unchanged dependency is not caught until the next such run.

Neither gate covers the JavaScript half or vendored C/C++. The renderer's pnpm tree appears in the per-release SBOM but is not vetted by these tools, and the C and C++ compiled inside build scripts (notably the WebRTC crates) is in neither.

GitHub Actions is inside the publishing trust boundary, and the whitepaper says so. The log signing key lives in Actions secrets and the trees are built and signed in CI, so a compromise of that environment could sign a tree. The post-publish self-audit and the equivocation tripwire detect that after the fact; they cannot prevent it. The same is true of the release-signing keys. Pollis operates the only log, which is why the independent verifier is released — so a third party can audit without asking us for anything.

The rotation shipped without an overlap window. The custody design calls for a minimum 90-day period in which both keys are pinned; the rotation that was actually performed did not have one. An auditor holding cached pre-rotation tree heads sees the change as equivocation and has to re-pin from the announcement rather than verify the transition.

Root compromise has no in-band recovery. If the offline root is lost or stolen, the fix does require a client release: mint a new root, ship a build pinning both, wait out the overlap, then publish under the new root alone.

The pinned key is copied by hand into eight places — the Rust core, this website, two workflows, the key-set statement, and three documents — with no check that they agree. One deployed copy going stale has already shown a false tamper alarm to every visitor once.