Historically, advanced mathematics for analysing software has been reserved to teams of PhDs at institutions like NASA.
But what if we could democratise these techniques, building on deep advances in AI to make them automatic, collaborative and accessible?
Imandra is AI for algorithms, scaled to the cloud.
Imandra has many advanced features, including first-class computable counterexamples, symbolic model checking, support for polymorphic higher-order recursive functions, automated induction, state-space decompositions and more.
If software is eating the world,
we really should take it more seriously.
When the algorithms we rely on are unsafe, unfair or inexplicable, the results can be catastrophic.
Imandra is powering a new generation of tools for the rigorous design, analysis and governance of complex algorithms.
Try Imandra Now
Imandra.Notebooks
A selection of interactive notebooks is waiting to help you learn Imandra and apply it to your toughest problems. Dive in and experience how fun and powerful automated reasoning can be!
Try Imandra NowPhD not required
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.
White Papers
Creating Safe and Fair Markets
Transparent Order Priority and Pricing
Case Study: 2015 SEC Fine Against UBS ATS
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
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals
Collaborative Verification-Driven Engineering of Hybrid Systems
A computational framework for conceptual blending
Recent and Upcoming Conferences
FMCAD 2018
The University of Texas at Austin, Austin, Texas, USA,October 30-November 2, 2018
CICM 2018
RISC, Hagenberg, AustriaAugust 13-17, 2018
BIG PROOF
Isaac Newton Institute, Cambridge University,July 1st - August 4th, 2017
CADE 26
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
About AI
Aesthetic Integration is an AI startup developing Imandra™, the cloud-scale automated reasoning system bringing rigor and governance to the world’s most critical algorithms.
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.
Dave Aitken
Matt Bray
Simon Cruanes
Barbara Galletly
Elijah Kagan
Kostya Kanishev
Marina Kulikova
Ewen Maclean
Nicola Mometto
Magda Wojcik
Alumni
Cristina Matache
