MLS formal verification

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.

mls is an RFC 9420 façade over AWS mls-rs (not the separate OpenMLS project). Gallery: positive-intentions.github.io/mls. Same claim words as the other library pages. A green job is not a proof of the Glitr messenger. Product cascade uses pairwise (2-party) MLS per contact; Glitr groups use a separate N-party GroupSession (welcome / commit / app) with pairwise cascade only as the delivery envelope.

Start from the verification report.

Interface under test

v0.1 targets cipher suite 1:

$$\texttt{MLS\_128\_DHKEMX25519\_AES128GCM\_SHA256\_Ed25519}$$

Public façade (mls-core):

• generate_identity / generate_key_package
• create_group / add_member / add_members / join_group / process_commit
• self_update / remove_member / roster helpers
• encrypt / decrypt application messages

Wire bytes are mls-rs MlsMessage encodings. Identity uses BasicCredential.

Feature	Backend
crypto-backend (default)	mls-rs-crypto-rustcrypto
sibling-crypto	X25519 via signal-protocol-core, local AES-128-GCM, HKDF-SHA-256, HPKE via mls-rs-crypto-hpke
--no-default-features	Stub API for extraction / verify scaffolding

Executable tests

Suite	What it covers	Gate
Rust tests (backend on)	Two- and three-party create → add/welcome → encrypt/decrypt; fail-closed garbage	Must pass
Rust tests (backend off)	Stub identity; ops return CryptoBackendDisabled	Must pass
Sibling feature	Same round-trip with sibling-crypto	Must pass
Line coverage	mls-core façade	100% lines on production + stub builds (coverage(off) only for proven-unreachable MlsMessage::to_bytes)
WASM	wasm32 build + wasm-pack web artifact (Node wasm-pack tests blocked by mls-rs-core ESM date_now)	Must pass

Formal pipelines

Kind	Status
ProVerif	Stub model in formal-proofs/ — open claim, not a discharged MLS secrecy proof
F* / Rocq / Lean	STATUS stubs only; green badge means the stub job ran

Open / not claimed

• Full MLS feature surface (external commits, PSK, X.509, multiple suites)
• Interop with OpenMLS (different stack)
• Full messenger-level proof that Glitr GroupSession + delivery envelopes compose securely
• That a green verify badge proves RFC 9420 security

See also: Cryptography, crypto formal verification (mls-layer cascade stub).