Introducing Imandra Markets

Online ecosystem for sharing and analysing client-facing trading system specifications

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

Model Change Alerts Icon

Model Change Alerts

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

Precise Venue Simulators 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

Empower with Precision

With Imandra, major recent advances in formal verification are at your fingertips. Use Imandra to analyse your algorithms and radically improve design, development, and regulation.

Research is the heart of what we do. This section showcases evolving technologies from our R&D engineers. From academic publications to new Imandra prototypes, join in the excitement as our new scientific results graduate into powerful products.


Imandra EVM:  A formal model of the Ethereum Virtual Machine

Imandra-based formal model of the Ethereum Virtual Machine (EVM). We’ve made the model open source under the Apache 2.0 license. It’s the first public entry in our community models repository.

Read More

Isabelle Language Server Protocol and VSCode Integration

Bringing the power of Isabelle’s Prover IDE to the open-source VSCode and Language Server ecosystems. Part of our broader Imandra Universe effort for collaborative formal verification in the cloud.

Read More

Recent and Upcoming Conferences


Isaac Newton Institute, Cambridge University,
July 1st - August 4th, 2017


Gothenburg, Sweden,
August 6-11, 2017

CICM 2017

Edinburgh, Scotland,
17-21st July, 2017

SC2  2017

Saarbrücken, Germany,
July 31-August 4, 2017

ACL2 2017

Austin, Texas, USA,
May 22-23, 2017

We’re hiring!

Join us!

Join Us

We're hiring!

About AI

Aesthetic Integration (AI) is a financial technology startup based in the City of London.

Created by leading innovators in software safety, trading system design and risk management, AI’s patent-pending Imandra formal verification technology is revolutionising the safety, stability and transparency of global financial markets.

Denis Ignatovich

Denis Ignatovich

Cofounder and Co-CEO

Denis Ignatovich has over a decade of experience in trading, risk management, quantitative modeling and complex trading system design. Prior to joining AI, he was head of the central risk trading desk at Deutsche Bank London. He holds an MSc in Finance from the London School of Economics and degrees in CS and Finance from UT Austin.

Grant Passmore

Grant Passmore

Cofounder and Co-CEO

Grant Passmore has more than ten years’ industrial formal verification experience. He has been a key contributor to safety verification of algorithms at Cambridge, Carnegie Mellon, Edinburgh, Microsoft Research and SRI. He earned his PhD from the University of Edinburgh and is a Life Member of Clare Hall, University of Cambridge.