Verification report

Research, not an audit

These pages are research and development and may not match the live app. Do not treat this as an audit. Shared for testing and demo only. Please use responsibly.

This report is for developers, cryptographers, and cybersecurity reviewers. It says what was checked on five libraries — not that a production function is a theorem, and not that the Glitr messenger is verified.

Field	Value
Date	4 October 2026
Subject	signal-protocol, ml-kem, pqxdh, mls, and crypto (core + cascade)
Audience	Developers, cryptographers, cybersecurity reviewers
Status	Research report — subject to change
Not claimed	Formal verification of the Glitr messenger, git mailbox delivery, or a stolen host

Jump to: For developers · For cryptographers · For security

Extract and CI minutiae: Signal Protocol, ML-KEM, PQXDH, MLS, crypto.

What was checked

Five libraries:

• signal-protocol — X3DH and the Double Ratchet, with AES-256-GCM. Source. Gallery: signal.positive-intentions.com.
• ml-kem — ML-KEM-1024 hybrid wrapper (closed-source; gallery only). Gallery: positive-intentions.github.io/ml-kem.
• pqxdh — PQXDH v3 composition and a linked handshake→session path (closed-source; gallery only). Gallery: positive-intentions.github.io/pqxdh.
• mls — RFC 9420 suite-1 façade over AWS mls-rs (closed-source; gallery only). Executable round-trips are tested; ProVerif/F*/Rocq/Lean jobs are stubs. Gallery: positive-intentions.github.io/mls. Details: MLS.
• crypto — crypto-core password envelopes and primitives; crypto-cascade product layer order (closed-source; gallery only). Gallery: positive-intentions.github.io/crypto.

Three activities share the label “formal verification.” They do not prove the same thing.

There is no arrow from tests to extract on purpose: passing tests does not validate the stub path. F*, Rocq, and Lean do not check the libcrux- or X25519-backed production functions.

Status words

Word	Meaning
Tested	An executable test failed or passed on the production build
Modeled	A ProVerif query was discharged on an abstract process — not a statement about extracted or production Rust
Type-checked	Extracted stub code or a hand-written spec compiled. Not functional correctness. The three backends do not prove the same lemmas
Assumed	An axiom: DH commutativity, KEM correctness, AEAD round-trip, CSPRNG, …
Open	Stated as a goal, or the model cannot express it yet
Cited	Recorded from pinned third-party proofs (libcrux), not re-proved here

Length lemmas are proved in F* (precondition includes validation), proved in Rocq on length only, and axioms in Lean. Tested hybrid / ratchet behaviour is on the production backend. It does not prove the spec axiom hybrid_round_trip or extracted encrypt / decrypt.

Rust llvm-cov is the core crate (plus crypto-cascade). WASM is Node/wasm-pack. coverage(off) is only for proven-unreachable helpers (hkdf_derive_short, chunk_prefix_len / read_u32_be, u32_from_be4). ml-kem has none.

What this report does not say

• The messenger is formally verified.
• Git mailbox delivery or a stolen host is in any model.
• X25519, Ed25519, HKDF, AES-GCM, Argon2id, or RSA-OAEP are proved inside these libraries.
• A stolen device, a malicious git host, or a side channel is in the model.
• Closed source is a substitute for review of ml-kem, pqxdh, or crypto. Outsiders cannot replay those scripts from this page alone. Signal Protocol source is public.

Precise library sentences (not a blanket “unclaimed”):

• pqxdh handshake and linked session: Modeled / type-checked under axioms.
• crypto-core password envelope: Tested / Modeled / type-checked under Argon2+AES axioms.
• crypto-cascade layer order and wire v3: Modeled composition; not a proof of the Glitr messenger, git delivery, or a stolen host.

FAQ sentence: signal-protocol (open source) plus ml-kem, pqxdh, and crypto (closed-source) have production tests, symbolic models under idealized primitives, and extracted type-checks of stub builds. Lattice math is cited from pinned libcrux, which is incomplete at that pin. The messenger is not verified.

A public Actions badge on a private ml-kem remote is not a source release.

Results at a glance

signal-protocol

Claim	Status	Where
Core crate line coverage 100%	Tested	Workspace llvm-cov; WASM src/ ignored
WASM and TypeScript wrappers behave	Tested	wasm-pack, Jest
Long-term and ephemeral secrets stay off the attacker’s knowledge	Modeled	Query-specific; the combined model is parallel and unlinked (see Open rows)
X3DH evaluates four DH shares in order	Modeled	Complete and 4-DH models
Old message keys are not recoverable from new chain keys	Modeled	Double Ratchet security model
After compromise, later messages can still be produced	Modeled	Same model
Decrypt implies a prior encrypt on that plaintext	Modeled	Double Ratchet models
Handshake output is fed into the first ratchet state	Open	Combined model has no linking channel
Alice/Bob authentication correspondence on the full X3DH process	Open	Same linking-channel limit
Extracted Double Ratchet is functionally correct	Open	F* CI skips it; Rocq/Lean CI check the axiom module only
Production backend refines the stubs	Open	No refinement proof

X3DH, as modeled, concatenates four Diffie–Hellman shares and a KDF:

$$\begin{aligned} \mathrm{DH}_1 &= \mathrm{DH}(\mathit{IK}_A, \mathit{SPK}_B), \\ \mathrm{DH}_2 &= \mathrm{DH}(\mathit{EK}_A, \mathit{IK}_B), \\ \mathrm{DH}_3 &= \mathrm{DH}(\mathit{EK}_A, \mathit{SPK}_B), \\ \mathrm{DH}_4 &= \mathrm{DH}(\mathit{EK}_A, \mathit{OPK}_B), \\ \mathit{SK} &= \mathrm{HKDF}(\mathrm{salt},\; \mathrm{DH}_1 \,\|\, \mathrm{DH}_2 \,\|\, \mathrm{DH}_3 \,\|\, \mathrm{DH}_4,\; \mathrm{info}). \end{aligned}$$

DH commutativity is assumed in the extracted spec, not proved for X25519:

$$\mathrm{DH}(a, \mathrm{pub}(b)) = \mathrm{DH}(b, \mathrm{pub}(a)).$$

ml-kem

Claim	Status	Where
Core crate line coverage 100%	Tested	Production Rust / CI
Hybrid encrypt/decrypt round-trip; tamper and wrong-key fail	Tested	Production tests
Wrong-length keys fail before the KEM is called	Tested (production); type-checked (spec)	Production try_from / guards; F* lemmas. No refinement to the backend.
Plaintext secrecy against the network attacker	Modeled	Hybrid security model
Shared-secret / AES-key material secrecy	Modeled	Same model
Decrypt event implies a prior encrypt of that plaintext	Modeled	Same model
Honest parties recover the same plaintext	Modeled	Hybrid round-trip model
Full ml-kem-core extract type-checks in F*	Type-checked	Host / F* job
Extracted Rocq modules type-check	Type-checked	Rocq job; ? bodies axiomatized
Wrapper length lemmas in Lean	Assumed	AbstractKem.lean states them as axioms; CI does not prove them
$\mathrm{Decaps}(\mathit{sk}, \mathrm{Encaps}(\mathit{pk})) = \mathit{ss}$	Assumed	Correctness axiom, not IND-CPA. Lattice math cited from libcrux, not linked.
Portable libcrux arithmetic / NTT / serialize / compress	Cited	Pin libcrux-ml-kem 0.0.10
Generic ind_cpa at that pin	Open	Upstream 0/21 at the pin
Production backend refines AbstractKem	Open	No refinement proof

ML-KEM-1024 sizes used by the wrapper (FIPS 203):

$$\lvert \mathit{pk} \rvert = 1568,\quad \lvert \mathit{sk} \rvert = 3168,\quad \lvert \mathit{ct} \rvert = 1568,\quad \lvert \mathit{ss} \rvert = 32.$$

Hybrid envelope:

$$\begin{aligned} (\mathit{ct}, \mathit{ss}) &= \mathrm{Encaps}(\mathit{pk}), \\ k &= \mathrm{HKDF\text{-}SHA256}(\mathit{ss}, \mathrm{salt}, \texttt{ML-KEM-1024-AES-GCM}), \\ c &= \mathrm{AES\text{-}256\text{-}GCM}_{k,\,\mathrm{iv}}(m), \end{aligned}$$

with $\lvert \mathrm{salt} \rvert = 16$ and $\lvert \mathrm{iv} \rvert = 12$. The statement

$$\mathrm{Dec}_{k,\mathit{iv}}(\mathrm{Enc}_{k,\mathit{iv}}(m)) = m$$

is assumed for AES-GCM and modeled in ProVerif as an equation.

Length rejection is a proved lemma on the F* spec (Rocq proves a length-only variant; Lean axiomatizes it):

$$\lvert \mathit{pk} \rvert \neq 1568 \implies \mathrm{pre}_{\mathrm{encap}}(\mathit{pk}) = \mathsf{false}.$$

pqxdh

Claim	Status	Where
Core crate line coverage 100% (both feature builds)	Tested	Production and stub Rust / CI
Honest handshake agrees on SK; initial AEAD abort; handshake→session	Tested	Production tests + handshake_session.rs (proptest is encode/KDF/handshake only)
Implementation KATs replay	Tested	Not official Signal vectors
SK secret if only DH or only KEM is leaked	Modeled	Hybrid-binding model
Forged SPK/PQ signatures do not yield honest SK	Modeled	Security model (honest bundle only)
Handshake SK is the SK the ratchet consumes	Modeled	Linked session / complete models (c_sk)
Extracted stub type-checks	Type-checked	F* full stub; Rocq/Lean axiom depth as siblings
DH / KEM / HKDF / AEAD / ratchet init	Assumed / Cited	Siblings + AbstractPqxdh
Production backend refines AbstractPqxdh	Open	No refinement proof

PQXDH IKM (this crate):

$$\mathit{SK} = \mathrm{HKDF}(0^{32},\; F \,\|\, \mathrm{DH}_{1..n} \,\|\, \mathit{ss},\; \texttt{PQXDH-v1\_CURVE25519\_SHA-256\_ML-KEM-1024}).$$

crypto

Claim	Status	Where
crypto-core line coverage 100% (both features)	Tested	Production and stub rust gates in CI (npm run test:rust:coverage:ci is production only)
crypto-cascade line coverage 100%	Open	Intended --fail-under-lines 100 on the product crate; last measured run after unhiding helpers was not 100%
Official SHA / AES-GCM KATs	Tested	NIST vectors
Argon2id RFC 9106 vectors	Open	Parameter mismatch; pinned implementation vector only
Password-envelope secrecy without the password	Modeled	password_security.pv
Core Aes+Password cascade nests inner keys	Modeled	cascade_core.pv
Five-layer product order and wire v3 outer-only	Modeled	Composition models; not a messenger proof
Empty password / wrong AES sizes fail before primitives	Type-checked	AbstractCrypto glue lemmas
Argon2id, AES-GCM, RSA-OAEP	Assumed	Not re-proved
Extracting encrypt_for_peer through hax	Open	Explicitly out of scope
Production backend refines AbstractCrypto	Open	No refinement proof

Password envelope (this crate):

$$k = \mathrm{Argon2id}_{m=19456,\,t=2,\,p=1}(\mathit{password},\; \mathit{salt}),\quad \mathrm{env} = (1,1,1,\mathit{salt}_{16},\mathit{nonce}_{12},c).$$

For developers

What a green job means, and what it does not.

Production interface

Callers use the functions and sizes above — not WASM bindings or a gallery UI. Signal: identity keys, signed prekeys, one-time prekeys, X3DH, then a Double Ratchet session (32-byte X25519 / Ed25519 keys, 64-byte signatures). ml-kem: generate_key_pair, encapsulate, decapsulate, hybrid encrypt / decrypt at the ML-KEM-1024 sizes in the glance table.

WASM and TypeScript wrappers are tested, not extracted.

Feature split

Production builds enable a crypto backend (X25519 / libcrux / AES-GCM). Extraction builds without that feature (--no-default-features on ml-kem). Concrete calls become stubs (AbstractCrypto, AbstractKem).

There is no refinement proof that the stub and the backend compute the same function. A passing cargo test on the production feature does not prove the extract.

What CI actually ran

The libraries run the same kind of jobs. The depth differs.

Job	signal-protocol	ml-kem	pqxdh	crypto
Format, Clippy, production tests	JS lint + Rust tests (no clippy/rustfmt job)	Yes	Yes	core + cascade
100% line coverage on core	workspace, ignore WASM src/	ml-kem-core	both features	core (both features) + cascade gate
WASM tests	Yes	Node wasm-pack	Node + session APIs	Node + envelope/AES
ProVerif suite	7 models	2 models	7 models (incl. linked session)	9 models (core + composition)
F*	Extracted modules except Double Ratchet	Full extract of ml-kem-core	Full stub extract	Full stub extract of crypto-core
Rocq	Hand-written axiom module only	Extract + type-check; ? axiomatized	Same wrapper depth	Same wrapper depth
Lean	Hand-written axiom module only	Extract + AbstractKem	AbstractPqxdh	AbstractCrypto
Third-party primitive proofs	—	verify-libcrux	Cite ml-kem / signal	None (no libcrux job)

verify:host:full on ml-kem is ProVerif + F* + Rocq + Lean. It does not run the libcrux pin job. A green host:full is not the lattice suite.

The wrapper depends on crates.io libcrux-ml-kem 0.0.10 and hax-lib 0.3. The pin file and libcrux job use git commit c5fb80f… and hax-lib 0.3.7. Signal’s verification image documents hax-lib 0.3. CI does not check that the crates.io tarball equals that commit.

Treat a live public CI run as the truth when one exists; otherwise the intended suite is what this report describes. If ml-kem jobs are not visible, even “last green” is invisible for that library.

How to replay

Surface	signal-protocol	ml-kem	pqxdh	crypto
Source	Public — clone	Closed — not released	Closed — not released	Closed — not released
Gallery	signal.positive-intentions.com	positive-intentions.github.io/ml-kem	positive-intentions.github.io/pqxdh	positive-intentions.github.io/crypto
This report	Claims and status	Claims and status	Claims and status	Claims and status

A public Actions badge on a private remote is not a source release.

Coverage gates, WASM/Jest detail: Signal Protocol. Pin checksums and libcrux job fields: ML-KEM. pqxdh and crypto stub llvm-cov (--no-default-features) are CI steps, not npm run test:rust:coverage:ci on crypto (that script is production crypto-core only).

For cryptographers

What was actually proved, assumed, or only type-checked.

Symbolic vs computational

ProVerif is a Dolev–Yao network attacker plus function symbols and equations, for example

$$\mathrm{DH}(a, g^{b}) = \mathrm{DH}(b, g^{a}), \qquad \mathrm{Dec}(k, \mathrm{Enc}(k, m)) = m.$$

Queries are secrecy (“the attacker cannot derive $m$”) and correspondence (“a decrypt event implies a prior encrypt event”).

This is not a computational proof. The AEAD equation is idealized: it is not IND-CCA, nonce-misuse resistance, or key commitment. The models are not machine-linked to the Rust. Constants matching the implementation is intent. The KEM process treats the shared-secret argument as encapsulation coins (kem_enc(pk, ss)), not “encapsulate draws 32 random bytes after validation.”

KEM correctness $\mathrm{Decaps}(\mathit{sk}, \mathrm{Encaps}(\mathit{pk})) = \mathit{ss}$ is assumed. That is correctness, not secrecy, and not IND-CPA.

Method

The same six steps are applied to each library. Later steps never cancel an earlier “open”.

Step 1 — Fix the production interface. Name the functions a caller actually uses. Record sizes and error paths. Everything below is relative to that interface.

Step 2 — Executable tests on the production build. Real primitives. 100% line coverage on the core crate. Tests do not prove secrecy.

Step 3 — Split production crypto from the extractable crate. Production enables a crypto feature. Extraction builds without it. No refinement proof.

Step 4 — Write a symbolic protocol model. ProVerif processes and queries, as above.

Step 5 — Extract Rust and type-check. hax translates the no-backend crate. CI type-checks that stub extract — not the production backend.

The three backends do not prove the same thing:

• F*: length lemmas proved on AbstractKem; KEM/AEAD/hybrid assumed; extracted wrappers type-checked via replace_body. Signal CI is lite: extracted modules except Double Ratchet.
• Rocq: length lemmas proved on a length-only predicate (no ValidatePK in those lemmas); hybrid/KEM functions axiomatized after ? fails to type-check. Signal CI is the hand-written AbstractCrypto module only.
• Lean: even the length lemmas are axioms; CI type-checks AbstractKem / AbstractCrypto only. Extracted Lean needs Mathlib and is not built in the ml-kem job.

Holes: where hax’s ? / ControlFlow encoding is not type-correct, those function bodies become axioms at extract time (generate_key_pair, encapsulate, decapsulate, derive_aes_key, encrypt, decrypt on the ml-kem Rocq path).

Step 6 — Cite upstream primitive proofs where they exist. ml-kem does not re-prove Kyber. It pins libcrux-ml-kem 0.0.10 (git c5fb80f…). Portable arithmetic / NTT / serialize / compress are cited. Generic ind_cpa is open (upstream 0/21 at that pin). Lattice math is not linked as a lemma in the wrapper.

Open goals that stay open

• Combined Signal model: X3DH and Double Ratchet run as parallel processes with no linking channel, so handshake-into-ratchet correspondence is open in signal-protocol. pqxdh discharges the analogous query on a private c_sk channel.
• Full X3DH authentication correspondence: same linking-channel limit in signal-protocol.
• Extracted Double Ratchet functional correctness: open (F* CI skips it).
• Refinement from production backends to AbstractCrypto / AbstractKem / AbstractPqxdh: open.
• Extracting crypto-cascade encrypt_for_peer through hax: open (out of scope).
• Argon2id as a memory-hard function: open (public KDF equation only).

Per-model query tables: Signal Protocol, PQXDH, crypto. AbstractKem lemma statements and pin checksums: ML-KEM.

For security

What you can say in a review without the extract notes.

Attacker and trust

Party	What we assume
Network attacker	Sees and rewrites every bit on the wire. This is the ProVerif attacker.
Honest endpoints	Run the modeled processes; they do not leak long-term keys unless a query says so.
Primitive oracles	DH, KEM, HKDF, AEAD behave as the equations or axioms say.
Host	Not modeled. A compromised device is outside both suites.
Git host / mailbox	Not modeled. Delivery and ciphertext-at-rest are product concerns.

Those last two rows are discussed as product analysis on Threat model. The dated product report (Glitr bar vs ideal-messenger gaps) is Threat-model report. Putting them on that folder does not put them in these models.

Forward secrecy in the Double Ratchet model means: after a ratchet step, old message keys are not derivable from the new chain. It does not mean a stolen laptop is safe.

Closed source is a limit on replaying ml-kem scripts. It is not a security property.

You may say

• These four libraries have production tests, including a 100% line-coverage gate on the named core crate(s). crypto-cascade uses the same --fail-under-lines 100 command; that product-crate gate is not yet green after unhiding helpers.
• ProVerif models an idealized network attacker and discharges stated secrecy and correspondence queries on those models.
• Extracted stub crates type-check in F*, Rocq, and Lean under named axioms. Depth differs (Signal F* skips Double Ratchet; Rocq/Lean are often axiom modules).
• pqxdh models a linked handshake→session path; signal-protocol’s combined model still leaves that open.
• crypto-core models the password envelope; crypto-cascade models layer order and wire v3 as composition only.
• ml-kem cites portable libcrux proofs at pin 0.0.10; ind_cpa is still open at that pin.
• Signal Protocol source is public. ml-kem, pqxdh, and crypto are not.

You may not say

• The Glitr messenger is formally verified.
• crypto-cascade’s composition model is a proof of Signal, PQXDH, ML-KEM, git delivery, or a stolen host.
• “The protocol is secure” or “Kyber is proved here.”
• Production encrypt/decrypt was proved in F*, Rocq, or Lean (round-trip is an axiom on the spec; tests run the real backend).
• A stolen device, a malicious git host, or a side channel was in the model.
• A public CI badge means closed-source libraries are released.

FAQ sentence: signal-protocol (open source) plus ml-kem, pqxdh, and crypto (closed-source) have production tests, symbolic models under idealized primitives, and extracted type-checks of stub builds. Lattice math is cited from pinned libcrux, which is incomplete at that pin. The messenger is not verified.

Library pages for the long tables: Signal Protocol, ML-KEM, PQXDH, crypto.