Omi TLA+ Definitions
September 26, 2026 · View on GitHub
Omi TLA+ definitions describe common binary exchange protocols as TLA+ modules, so what the wire format states is checked rather than assumed: every message encodes to the bytes the model states and decodes back to what was encoded.
These definitions are checked with the TLA+ model checker: TLC
Usage
Each .tla file is a self contained module for one protocol version: the wire primitives, one record per group the tree reads, one choice per message dispatch, and the invariants TLC checks over them. Its .cfg sits beside it, naming the invariants to check. Run one with the TLA+ tools:
java -cp tla2tools.jar tlc2.TLC iex/iexequities/tops/IexEquities_Tops_v1_56.tla
A field is the bytes it occupies; an integer is read only where a rule depends on one — a length, a count, a message type — which are the dependencies the parse rules run on. Each definition is accompanied by a _Captures module carrying packets recorded off the wire, which decode and encode back to exactly the bytes they were read from.
For the model checker and its tools: TLA+ Tools
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 |
|---|---|
| 224 | 217787 |
Testing
Please report any checking 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
Exchanges
GemxOptions · IexEquities · IexOptions · IseOptions · MrxOptions · NomOptions · NordicEquities · NsmEquities · NtxEquities · NtxOptions · PhlxOptions · PsxEquities
Consolidators
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
- Lean Definitions — Lean 4 definitions with machine checked encode and decode proofs
- FIX Dictionaries — QuickFIX format xml data dictionaries, one per FIX version
- Xml Specifications — the exchange protocol specification xmls, matching the original files
License
Omi definitions are free software with the least restrictive licensing possible; see the Omi license terms.
The TLA+ logo above is Copyright Edward Lamport and is used under the MIT license, redrawn from the TLA+ splash image published on Wikimedia Commons:
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
Disclaimer
Any similarities between existing people, places and/or protocols is purely incidental.
Enjoy.