Omi Lean Definitions
September 26, 2026 · View on GitHub
Omi Lean definitions describe common binary exchange protocols as Lean 4 modules that carry their own proofs.
These definitions are checked with the Lean toolchain: lake
Usage
Each .lean file is a self contained module for one protocol version: a structure per message, an inductive per coded field, a sum type dispatching on the message type, and the theorems relating each decoder to its encoder. The shared Omi/Wire.lean holds the field kinds (big and little endian integers, fixed width text, counted repetition) and their lemmas. Check every proof with lake:
lake build
A definition is used as an ordinary Lean library: decode reads a List UInt8 and returns the message with the bytes that follow, encode writes one, and the theorems are available to anything built on top.
For toolchain information: Lean Toolchain
Development
Updates are greatly appreciated; however, this entire repository is source generated...including the words you are reading right now. If you wish to suggest definition updates, the recommended process is to create an issue with changes and explanation. Time permitting, we will update the models and regenerate.
| Protocol Count | Generated Lines |
|---|---|
| 760 | 2500889 |
Testing
The build checks every proof. The tests under .github/tests/ decode captured packets from omi-data-packets and require each to be consumed exactly; each is a theorem decided at build time, so a failing test fails the build.
Please report any parsing errors as an issue. Include a small note on the protocol and version, and a minimal capture demonstrating the problem. Also consider including a link or pdf specification documenting the correct behavior.
Open Markets Initiative
The Open Markets Initiative (Omi) is a group of technologists dedicated to enhancing the stability of electronic financial markets using modern development methods.
Other generated code can be found at Omi Projects; for Omi rules and regulations, see Omi Directory.
Organizations
24X · A2X · Aquis · Asx · B3 · Bist · Biva · BlueOceanAts · Box · BruceAts · Bse · CixAts · Cme · Coinbase · Eurex · Euronext · Iex · Imperative · Jpx · Miax · Nasdaq · Nse · Sgx · SmallX · Tmx · Txse
Exchanges
24XEquities · A2XEquities · AquisEquities · AsxDerivatives · AsxSecurities · B3Derivatives · BivaEquities · BlueEquities · BorsaIstanbul · BoxOptions · BruceEquities · BseIndia · CoinbaseDerivatives · Deribit · EmeraldOptions · FseEquities · GemxOptions · IexEquities · IntelligentCross · IseOptions · MiaxOptions · MrxOptions · Mx · NfxFutures · NomOptions · NordicEquities · NseCd · NseCm · NseCom · NseEquities · NseFo · NsmEquities · NtxEquities · NtxOptions · OnyxFutures · OseDerivatives · PearlEquities · PearlOptions · PhlxOptions · PsxEquities · SapphireOptions · SmallFutures · SseEquities · TseEquities · Tsx · TsxAlpha · TxseEquities
Platforms
CixAts CixAspen · Cme Globex · Euronext Optiq · Eurex T7 · Sgx TitanDt
Consolidators
NordicMarkets · Uqdf · Utdf · Utp
Related Definitions
The Open Markets Initiative provides protocol definitions in several formats:
- Kaitai Struct Definitions — cross language binary parsers with the kaitai struct compiler
- DFDL Definitions — declarative DFDL schemas for cross language parsing
- P4 Definitions — P4 programs for software and hardware data planes
- Spicy Definitions — declarative Spicy grammars for the spicy toolchain and the zeek network security monitor
- TLA+ Definitions — TLA+ modules whose encode and decode are model checked with TLC
- FIX Dictionaries — QuickFIX format xml data dictionaries, one per FIX version
- Xml Specifications — the exchange protocol specification xmls, matching the original files
Disclaimer
Any similarities between existing people, places and/or protocols is purely incidental.
Enjoy.