Verify the Sparse Post-Quantum Ratchet (SPQR) using Lean

A project to formally verify SparsePostQuantumRatchet, a Rust implementation of Signal's post-quantum secure ratchet protocol.

The verification uses Lean 4 and relies on the Lean representation of the Rust code produced by Aeneas.

Maintained by The Beneficial AI Foundation.

Repository Structure

Path	Contents
src/	Rust source of the SPQR crate (pinned upstream commit, with any local edits captured in src-modifications.diff).
SrcTranslated/	Aeneas-auto-generated Lean files (Types.lean, Funs.lean, never edited by hand) plus hand-written externals (TypesExternal.lean, FunsExternal.lean).
Spqr/Math/	Project-wide mathematical infrastructure, implemented in Lean.
Spqr/Specs/	Lean spec theorem files for individual Rust functions, organised to mirror the Rust module tree.
aeneas-config.yml	Aeneas extraction configuration.
scripts/	Project tooling scripts (extraction, diffing, linting, auditing).
doc/	Style and workflow/PR guides.

Contributing

See CONTRIBUTING.md.

Code of Conduct

We follow the Rust Code of Conduct, with the following additional clause:

• We respect the rights to privacy and anonymity for contributors and people in the community. If someone wishes to contribute under a pseudonym different to their primary identity, that wish is to be respected by all contributors.

License

This repository is dual-licensed:

• Upstream source is licensed under AGPL-3.0-only, inherited from signalapp/SparsePostQuantumRatchet. The Aeneas-generated Lean translation in Types.lean and Funs.lean in SrcTranslated/ is a derivative of that source and is therefore also covered by AGPL-3.0-only.

• Other contributions (such as hand-written Lean code under Spqr/Math/ or Spqr/Specs/) are released under the Apache License, Version 2.0.