Create and share your models with select counterparties
Apply Imandra's cutting-edge algorithm analysis tools to ensure your designs are correct and stable
Apply Imandra's powerful ‘region decompositions’ to automatically generate high-coverage test suites to ensure rigorous testing of your connectivity logic
We make it easy for you to encode or convert existing functionality into something precise
Generate compliance reports from your connectivity sessions
Ensure you and your upstream users are alerted about all relevant changes
Test against precise venue simulators generated automatically from DSL models
Perform historic audit and ensure your production environment is not deviating from the design
Verifies correctness and stability of system designs for regulatory compliance
Uncovers nontrivial bugs in code and documentation
Creates high-coverage test-suites
Want to get started without MD signoff?We have a plan for you!
Download VS Code plugin for Imandra Protocol Language
Coming soon: Eclipse plugin
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.
DSL has built-in support for all recent versions of FIX data dictionaries. Access them with a simple ‘library’ command:
Look up available fields and values with built-in editor autocompletion:
The language will highlight any missing required fields that your model must support:
Locally declared records with linkable fields to messages and record types from FIX data dictionary:
Explicitly set Float types (Qty, Price etc.) precision for your model:
Access documentation with a mouse-over:
Imandra Protocol Language is a strongly typed language, making it harder for you to introduce errors:
User cannot introduce two fields with the same name - an error will be thrown by the editor:
Extend the standard FIX enums, records and messages with custom entries:
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.
Imandra's region decompositions give you unparalleled insight
into the nuances of your connectivity logic.
Find subtle "edge" cases with ease and ensure
you handle all of them properly.
Turn your spec into a simulator with the push of a button.
Combine your precise specs, derived simulators, and Imandra's algorithm analysis and test suite generation to test your systems rigorously and automatically.
Share your precise specs with your clients counterparties, with full control over who sees what.
Imandra ensures your clients are up-to-date with all of your changes and features.
Manage your full connectivity life-cycle in one easy-to-use environmet.
Use Imandra's Testflow to design complex testing templates, and derive high-coverage test-suites from them automatically.
Have Imandra give you precise compliance documentation describing your testing methodology, governance processes and results.
Easily generate tests that push your system into specific regions of behavior.
Let Imandra guide you to important edge cases, or put yourself in the driver's seat and design a custom testflow.
There's nothing worse than an "unknown unknown." Use Imandra to eliminate them as early as possible.
Provision ports and backtest your strategies against precise historical venue models and market data
Perform historical system audits to analyse production system spec conformance
Automate MIFID II compliance
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.
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’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.
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).
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’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.