Type inference
Strongly statically typed language where the type checker deduces types and ensures validity in context.
Mission
Protocol-independent connectivity specs
IPL expresses how systems connect and behave — starting with FIX, extensible to other protocols.
IPL was designed as a protocol-independent language for system connectivity specifications. Today's libraries focus on FIX; the framework generalizes to other protocols.
Markets depend on interconnected systems understanding each other safely. IPL provides a rigorous way to specify and verify trading behaviour — making machine-reasonable regulations actionable.
Read the full introduction here.
Digital Twins
A formal digital twin of your FIX gateway
An IPL model is more than documentation — it can be co-simulated against your production environment so spec and implementation stay in lock-step.
Unlike a PDF of a FIX spec or “rules of engagement,” an IPL model is a program. Imandra FIX Wizard, audit tooling, and onboarding flows all read from the same model, and the model itself can be exercised against the live endpoint.
Every team works from the same source of truth, and divergence between what you document and what you run becomes observable rather than something customers report.
Co-simulated against production
The IPL model is executable and can be run against the live gateway — what your customers read matches what they connect to.
One source of truth
Onboarding, QA, product, and client teams query the same digital twin instead of stitching together PDFs, tickets, and tribal knowledge.
Drift is detectable
Differences between the spec and the running system surface as concrete failures, not customer-reported bugs months later.
From PDF to program
IPL digitizes specifications
The same field that takes a paragraph of prose in a FIX PDF becomes a few lines of typed, machine-checked IPL — easy to encode, hard to introduce errors.
A field tag, its allowed values, and the cross-field rule (“required if OrdType = Pegged”) are all expressed directly in IPL — and the type checker catches mistakes before the spec ever reaches a counterparty.
The model
Infinite state machines, not just FSMs
IPL models a system interface as an infinite state machine — expressive enough to capture real protocols, while still amenable to automated reasoning.
Finite state machines run out of room as soon as state carries quantities, prices, or identifiers. IPL keeps the structure of an FSM but lets state, messages, and actions range over rich data — so you can specify behaviour without flattening it.
State
A global variable that maintains the session — as many fields as the protocol requires, with explicit initial values.
Read in docs
Inbound messages
Messages a client sends to the system. Validity statements constrain fields individually and in combination.
Read in docs
Actions
Internal events — fills, time changes, halts — that can update state and emit outbound messages.
Read in docs
Outbound messages
Messages the model sends back. Their types are defined alongside the receive logic that constructs them.
Read in docs
Capabilities
What IPL gives you
Strong typing, protocol libraries, and reasoning-ready models for connectivity.
Machine-reasonable
Not only machine readable — enables automated verification, test generation, and regulatory reasoning.
Protocol libraries
Built-in FIX protocol libraries with support for multiple versions and extension points for other protocols.
State management
Model state and transitions as state machines — the basis for automated reasoning over connectivity.
Validity checking
Internal validity construction ensuring specifications return messages with all required fields.
IDE integration
Language server with context-aware completion and hover documentation via the IPL VS Code extension.
Read the full types and expressions guide here.
Automated reasoning
From model to test cases, automatically
One of the most-requested IPL features: symbolic decomposition of the model state space, turned into runnable tests that exercise every distinct path through your protocol.
ImandraX analyses each symbolic trace through the model, then generates source code that drives your implementation into the same state transitions and checks the result against expectation.
The output is more than test data — it is a certification artefact that ties a piece of the spec to a concrete, runnable check.
1
Decompose the state space
ImandraX walks the IPL model symbolically, producing distinct regions of behaviour and the symbolic constraints that characterise each one.
2
Generate concrete inputs
For every region, the constraint solver synthesises concrete sample points — message field values, state, and event sequences that satisfy the path.
3
Drive your implementation
The same regions yield runnable test scripts that push your real system through each transition and compare its behaviour against the model.
VS Code Plugin
Use IPL directly in your editor
Install the Imandra Protocol Language extension to get language-aware editing and documentation generation in VS Code.
Start with the Visual Studio Marketplace listing, then use the GitHub repository for source code, issues, and release details.