Introducing Imandra Markets
Online ecosystem for sharing and analysing client-facing trading system specifications
Secure Online Platform
Create and share your models with select counterparties
Automated Reasoning
Apply Imandra's cutting-edge algorithm analysis tools to ensure your designs are correct and stable
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
We make it easy for you to encode or convert existing functionality into something precise
Automated Compliance Reports
Generate compliance reports from your connectivity sessions
Model Change Alerts
Ensure you and your upstream users are alerted about all relevant changes
Precise Venue Simulators
Test against precise venue simulators generated automatically from DSL models
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.
Want to learn more?
Read our technical white papers.
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.
Projects
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.
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.
Select Recent Publications
Formal Verification of Financial Algorithms
Decidability of Univariate Real Algebra with Predicates for Rational and Integer Powers
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL
Collaborative Verification-Driven Engineering of Hybrid Systems
Recent and Upcoming Conferences
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
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
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.
Matt Bray
Barbara Galletly
Sergey Grigorchuk
Eduard Grinchenko
Elijah Kagan
Kostya Kanishev
Maja Kovacevic
Marina Kulikova
Ewen Maclean
Magda Wojcik
