Imandra by Aesthetic Integration

Dart throwing is out. Mathematical rigour is in.
Join the AI for Algorithms Revolution

Financial Markets

From dark pool matching logics to FIX connectivity, Imandra's powerful algorithm governance tools are used by top financial institutions to ensure safety, transparency and compliance of their most critical algorithms.

Robotics

From self-driving cars to drones and medical robots, Imandra's automated reasoning technology is powering next-generation tools for the design, safety and compliance of autonomous vehicles and cyber-physical systems.

Blockchain

Bugs in smart contracts can lead to catastrophic losses. Imandra's cloud-based formally verified functional programming is powering next-generation tools for the design and analysis of safe and compliant smart contracts.

formally verified functional programming
scaled to the cloud

Try Imandra Now

PhD not required

watch the video

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.

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, Austria
August 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

We’re hiring!

Join us!

Join Us

We're hiring!

Media

ALL MEDIA

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.