SpecAMQP
An open specification of AMQP 1.0, written in Lean 4, covering a large and growing fragment of OASIS Parts 0–5. Implementations share that one description and can prove they comply with it. It is a single asset that can be honed, extended, and fixed over time.
What it covers
The specification is a state machine over a fixed interface alphabet, so another implementation can be checked against it directly. Beside it sits a clause ledger: every clause of the standard has a recorded disposition, and every place the standard is silent is written down with the reading that was taken.
Several implementations can share that description. One is written from the standard without reading the specification. The two run the same vectors, and a disagreement means one of them misread the standard. A reference implementation is being grown into a full server that is correct by construction.
The shipped endpoint's protocol core is proved to conform to the specification. Framing laws are proved as well. The socket boundary and the process loop above it are not proved yet, so the binary still rests on Lean's compiler and runtime.
Results
- 579 Clauses in the standard: 238 formalized, 105 covered by test vectors, 180 deferred to named work, and the rest informative, out of scope, or superseded.
- 180 Deferred clauses, mostly sessions and links (49), transactions (44), messages (37), and session state (32).
- 24 Test corpora, replayed step by step against the specification and the reference implementation.
- 20 Offline gates, and 76 Lean modules.
- Proved The specification and the reference agree on every committed corpus. The endpoint protocol core is proved to conform.