Revolutionary Technology

The complexity of modern software has significantly outpaced the power of traditional tools used to design and regulate it. Imandra’s breakthrough algorithm analysis technology has the power to revolutionise the way algorithms are designed and implemented.

Revolutionary Technology

The complexity of modern software has significantly outpaced the power of traditional tools used to design and regulate it. Imandra’s breakthrough algorithm analysis technology has the power to revolutionise the way algorithms are designed and implemented.


VERIFIES


Verifies correctness and stability of system designs for regulatory compliance


UNCOVERS


Uncovers nontrivial bugs in code and documentation


TESTS


Automatically creates high-coverage test suites


SAVES


Radically reduces associated costs


VERIFIES


Verifies correctness and stability of system designs for regulatory compliance


UNCOVERS


Uncovers nontrivial bugs in code and documentation


TESTS


Automatically creates high-coverage test suites


SAVES


Radically reduces associated costs

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.

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.

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.

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.

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).

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.

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.

Formal Verification

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.

AUTOMATED THEOREM PROVING

NONLINEAR DECISION PROCEDURES

SATISFIABILITY MODULO THEORIES

AUTOMATED INDUCTION

AUTOMATED COMPLIANCE REPORTS

TEST SUITE GENERATION

MODEL CHECKING

TYPE THEORY

We have had the pleasure of working with

Become an early adopter

REQUEST A DEMO SESSION

Become an early adopter

REQUEST A DEMO SESSION

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

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

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.