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
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
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 |
|---|---|
| 1148 | 4119766 |
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.
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 Repositories; for Omi rules and regulations, see Omi Directory.
24X · A2X · Aquis · Asx · B3 · Binance · Bist · Biva · BlueOceanAts · Bme · Box · BruceAts · Bse · Cboe · CixAts · Cme · Coinbase · Currenex · Eurex · Euronext · Finra · Hkex · Ice · Iex · Imperative · Jnx · Jpx · Jse · Lme · Lseg · Ltse · Memx · Miax · Nasdaq · Nse · NsxAustralia · Nyse · Odx · Okx · OtcMarkets · Sgx · Siac · SmallX · Szse · Tmx · Tradelogiq · Txse
24XEquities · A2XEquities · AmexEquities · AmexOptions · AquisEquities · ArcaEquities · ArcaOptions · AsxDerivatives · AsxSecurities · B3Derivatives · BinanceSpot · BivaEquities · BlueEquities · BmeEquities · BmeFixedIncome · BorsaIstanbul · BoxOptions · BrokerTec · BruceEquities · BseIndia · BxeEquities · ByxEquities · BzxEquities · BzxOptions · C1Options · C2Options · CboeEurope · CedxDerivatives · CfeFutures · CoinbaseDerivatives · CurrenexForex · CxaEquities · CxeEquities · CxjEquities · Deribit · DxeEquities · Ebs · EdgaEquities · EdgxEquities · EdgxOptions · FinraOrf · FseEquities · GemxOptions · HkexSecurities · IceFutures · IexEquities · IexOptions · IntelligentCross · IseOptions · JnxBonds · JnxEquities · LinkAts · LinkNqb · LmeSelect · Lse · LtseEquities · LynxAts · MatchNow · Meff · MemxEquities · MemxOptions · MoonAts · MrxOptions · Mx · NasdaqCanada · NationalEquities · NeoEquities · NfxFutures · NomOptions · NordicDerivatives · NordicEquities · NseCd · NseCm · NseCom · NseEquities · NseFo · NsmEquities · NtxEquities · NtxOptions · NyseBonds · NyseEquities · NyseOptions · OdxEquities · OdxSecurityToken · OkxDigital · OmegaAts · OnyxFutures · OseDerivatives · Overnight · PearlEquities · PhlxOptions · PsxEquities · SmallFutures · Sse · SseEquities · Szse · SzseSecurities · TexasEquities · Trace · TradeEcho · TseEquities · Tsx · Turquoise · TxseEquities
CixAts CixAspen · Cme Globex · Jse Itac · Lseg Millennium · NsxAustralia Nets · Euronext Optiq · Eurex T7 · Sgx TitanDt
Cqs · Cts · NyseConsolidated · Opra · TitaniumConsolidated · Uqdf · Utdf · Utp
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
Omi definitions are free software with the least restrictive licensing possible; see the License for the Omi license terms and the TLA+ logo attribution.
Any similarities between existing people, places and/or protocols is purely incidental.
Enjoy.