Reasoning as

a Service

New! Download VS Code plugin for

Imandra Protocol Language

DOWNLOAD
Imandra Markets Ecosystem Icon

Imandra

Markets

Imandra Markets

Online ecosystem for sharing and analysing machine-reasonable APIs

Secure Online Platform Icon

Secure Online Platform

Create and share your models with select counterparties

Automated Reasoning Icon

Automated Reasoning

Apply Imandra's cutting-edge algorithm analysis tools to ensure your designs are correct and stable

Automated Test Generation Icon

Automated Test Generation

Apply Imandra's powerful ‘region decompositions’ to automatically generate high-coverage test suites to ensure rigorous testing of your connectivity logic

Toolset for Creating Precise Specs Icon

Toolset for Creating Precise Specs

We make it easy for you to encode or convert existing functionality into something precise

Automated Reasoning Icon

Automated Compliance Reports

Generate compliance reports from your connectivity sessions

Automated Reasoning Icon

Model Change Alerts

Ensure you and your upstream users are alerted about all relevant changes

Automated Reasoning Icon

Precise Venue Simulators

Test against precise venue simulators generated automatically from DSL models

Historic and Real-time Audit Icon

Historic and Real-time Audit

Perform historic audit and ensure your production environment is not deviating from the design

Key Functions

Verifies

Verifies

Verifies correctness and stability of system designs for regulatory compliance

Uncovers

Uncovers

Uncovers nontrivial bugs in code and documentation

Tests

Tests

Creates high-coverage test-suites

Imandra Protocol Language

Imandra Protocol Language: Now for FIX!

New!

Download VS Code plugin for Imandra Protocol Language

DOWNLOAD

Coming soon: Eclipse plugin

Make FIX connectivity painless and automatic

With Imandra's Protocol Language, creating and communicating your FIX specs has never been easier. Throw out those out-of-date PDFs and base your connectivity process on precise mathematical specs. From design to testing, simulation and compliance, Imandra's Protocol Language and algorithm analysis tools make connectivity a breeze.

FIX data dictionaries

DSL has built-in support for all recent versions of FIX data dictionaries. Access them with a simple ‘library’ command:

Imandra DSL feature

Intelligent code autocompletion

Look up available fields and values with built-in editor autocompletion:

Imandra DSL feature

Context-aware Help

The language will highlight any missing required fields that your model must support:

Imandra DSL feature

Local records

Locally declared records with linkable fields to messages and record types from FIX data dictionary:

Imandra DSL feature

Float type precision

Explicitly set Float types (Qty, Price etc.) precision for your model:

Imandra DSL feature

FIX Documentation

Access documentation with a mouse-over:

Imandra DSL feature

Full type checking

Imandra Protocol Language is a strongly typed language, making it harder for you to introduce errors:

Imandra DSL feature

Validation on duplicate names

User cannot introduce two fields with the same name - an error will be thrown by the editor:

Imandra DSL feature

Custom fields and enums

Extend the standard FIX enums, records and messages with custom entries:

Imandra DSL feature
Model Certification Icon

Model Certification

With your FIX spec expressed in IPL, Imandra's powerful algorithm analysis tools will automatically analyse your design for correctness and compliance. An Imandra certification means your spec meets rigorous correctness and consistency criteria.

Slash costs and risks by rooting out errors early and automatically.

Model Certification Preview
Region Explorer Icon

Region Explorer

Imandra's region decompositions give you unparalleled insight
into the nuances of your connectivity logic.

Region Explorer Constraints Region Explorer Diagram

Find subtle "edge" cases with ease and ensure
you handle all of them properly.

Venue Simulator Icon

Venue Simulator

Simulators with the push of a button

Turn your spec into a simulator with the push of a button.

Test both Application and Session logic

Combine your precise specs, derived simulators, and Imandra's algorithm analysis and test suite generation to test your systems rigorously and automatically.

Marketplace Icon

Marketplace

Share your specs with full access control

Share your precise specs with your clients counterparties, with full control over who sees what.

Model Certification Preview

Onboard clients more quickly and cheaply

Imandra ensures your clients are up-to-date with all of your changes and features.

Model Certification Preview

Manage your full connectivity life-cycle in one easy-to-use environmet.

Model Certification Preview
Testflow Icon

Imandra Testflow

Rigorous testing from start to finish

Use Imandra's Testflow to design complex testing templates, and derive high-coverage test-suites from them automatically.

Automate testing-oriented compliance

Have Imandra give you precise compliance documentation describing your testing methodology, governance processes and results.

Target specific system behaviours

Target specific system behaviours

Easily generate tests that push your system into specific regions of behavior.

Be guided by the spec

Be guided by the spec

Let Imandra guide you to important edge cases, or put yourself in the driver's seat and design a custom testflow.

Expect the Unexpected

Expect the Unexpected

There's nothing worse than an "unknown unknown." Use Imandra to eliminate them as early as possible.

Subscription Plans

Free

Modelling

Certification

FIX Icon

IPL IDE Plugins

Editor support for VS Code and Eclipse

Green Dot Icon
Green Dot Icon
Green Dot Icon
FIX Icon

IPL Wizard

Upload and certify IPL models

Grey Dot Icon
Green Dot Icon
Green Dot Icon
Marketplace Icon

Marketplace

Preview and exchange models with ease

Grey Dot Icon
Green Dot Icon
Green Dot Icon
On-demand Simulators Icon

On-demand Simulators

Simulate your generators or environments

Grey Dot Icon
Grey Dot Icon
Green Dot Icon
On-demand Simulators Icon

Test Services

Test your algorithms instantly

Grey Dot Icon
Grey Dot Icon
Green Dot Icon

Coming Soon

Backtesting Icon

Backtesting

Provision ports and backtest your strategies against precise historical venue models and market data

Audit Icon

Audit

Perform historical system audits to analyse production system spec conformance

MIFID 2 Icon

MIFID II Compliance Pack

Automate MIFID II compliance

Making Algorithms Safe and Fair

Algorithms manage everything from aircraft autopilot systems and financial exchanges to blockchain smart contracts and smart phone apps. Imandra analyses algorithms to help you understand what they do, why they do it, and what can possibly go wrong.

Imandra Diagram Step 1

1 | Modern Software

Software continues to improve communication and commerce around the world. But these improvements come with significant risk. Regulators, businesses, and the general public urgently need to manage the risks these ubiquitous systems present, as they fly our airplanes, run our smart phone apps, and execute blockchain smart contracts.

Imandra Diagram Step 2

2 | Ambiguity and Complexity

Documents describing how complex systems work are often rife with mistakes and ambiguity. We need better means for communicating about how complex algorithms are designed. To this end Imandra leverages formal verification – a mathematical science dedicated to describing and reasoning rigorously about algorithms – to help accurately predict how software should and will behave.

Imandra Diagram Step 3

3 | Cloud Ecosystem

Imandra’s cloud infrastructure marries software documentation and the power of formal verification, providing the first collaborative environment for translating complex algorithms into mathematical models, applying powerful tools to reason about them. Our cloud also incorporates multiple Domain Specific Languages (DSLs), libraries of common properties relevant to financial regulations, models of common system components, and tools for collaborative analysis.

Imandra Diagram Step 4

4 | Mathematical Models

Given a model and a property to reason about, Imandra works to generate a proof that the property will always hold, or to present a concrete counterexample identifying how the property may be violated. For complex systems such counterexamples often identify nontrivial sequences of events that are virtually undiscoverable by hand (or with random number generators).

Imandra Diagram Step 5

5 | Automated Reasoning

Many modern systems operate across virtually infinite state spaces. In other words, all the ways a piece of software could potentially behave are incomprehensible to any person or team. At its core, Imandra employs powerful automated theorem proving techniques to analyse and reason about complex algorithms. Imandra brings tools traditionally reserved for highly specialised teams at institutions like NASA to the general public.

Imandra Diagram Step 6

6 | Governance, Safety, Fairness

Imandra’s deep algorithmic analysis makes effective governance of the modern algorithmic world possible. From financial algorithms to self-driving cars, our mission is to revolutionise safety and fairness of industries that run on algorithms.

White Papers

Case Study: 2015 SEC Fine Against UBS ATS

Read More

Transparent Order Priority and Pricing

Read More

Creating Safe and Fair Markets

Read More