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
Want to learn more?
Read our technical white papers.
We have had the pleasure of working with
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 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 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.
Sergio Baca
Matt Bray
Barbara Galletly
Sergey Grigorchuk
Eduard Grinchenko
Elijah Kagan
Kostya Kanishev
Maja Kovacevic
Marina Kulikova
Ewen Maclean
Magda Wojcik
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 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.
Sergio Baca
Matt Bray
Barbara Galletly
Sergey Grigorchuk
Eduard Grinchenko
Elijah Kagan
Kostya Kanishev
Maja Kovacevic
Marina Kulikova
Ewen Maclean