Imandra is a cloud-native
automated reasoning engine.

Distributed Ledger Technology shows promise in helping to fix some of the issues facing financial markets. However, as many high-profile costly DLT bugs have shown, the code running on such systems is very difficult to get right, and must be subjected to formal verification.

In 2015, we pioneered the application of formal verification to DLT. In fact, we were the first to create a formal model of the Ethereum Virtual Machine, empowering Imandra to reason about the possible behaviours of Ethereum smart contracts. As new blockchain protocols and stacks are developed, Imandra is powering a new generation of tools helping to ensure the safety and correctness of these systems.

Relevant links:

White papers:

As robots become more ubiquitous and complex, we need to understand and stay in control of what they can and cannot do. We have created an Imandra interface to Robot OS (www.ros.org), allowing you to leverage an existing widely popular framework and write code that you can verify for safety and correctness properties. The Imandra-ROS package is open source and is available here.

Relevant links:

From aerospace to railroads to self-driving cars, the systems we rely on most run on heavily regulated algorithms. Imandra's automated reasoning technology is changing how these industries create and regulate their algorithms by:

1. Providing an accessible and scalable methodology for writing and verifying specs and production-level code, and

2. Providing a scientifically sound methodology for requirements traceability, backed by Imandra's symbolic reasoning and state-space decompositions.

Imandra can be easily plugged in as a reasoning backend into many safety-critical toolchains.

Relevant links:

Modern hardware designs are incredibly complex and leading designers already rely on formal verification to ensure key aspects of their correctness. Imandra's embedding in a high-performance programming language (OCaml), first-class support for computable counterexamples, seamless integration of symbolic model checking and automated and interactive theorem proving (including automated induction, lemma-based conditional rewriting and forward-chaining, decision procedures for nonlinear real arithmetic and more), make it an ideal framework for the most demanding hardware verification tasks.

Relevant links:

The effective regulation of algorithms is of paramount importance. The safety of shared infrastructure and protection of private information must be checked by governments and properly enforced.

At Aesthetic Integration, we continue to be vocal about the need for government regulators to leverage deep advances in automated reasoning for powerful and cost-effective algorithm governance.

Relevant links:

Bad things happen when hackers know more about your web application than you. With GDPR coming online in 2018, companies can face fines as much as 4% of their annual revenue. With Imandra, you can bring the most rigorous software development techniques to bear on web development.

Imandra supports ReasonML, an OCaml language created by Facebook for web development. We’re actively working on an interface to React, one of the most popular Javascript frameworks.

Relevant links:

Historically, computer science departments have often had a separation between theory and practice. Often, the mathematics underlying program correctness is restricted to upper theory courses, far removed from programming practice. It's time we change that!

Imandra bridges this gap, allowing you to teach logic and formal verification in a real-world language that your students can apply immediately in a real-world setting. Imandra's automation allows students to verify deep properties of their code (and crucially, obtain counterexamples to their often false conjectures) long before they understand predicate calculus or induction!

The computational modelling of chemical, biological and physical systems is a foundation of modern science, with much analysis happening from a stochastic or continuous perspective. The phrasing of the evolution of a system as an "algorithm" is key.

Automated reasoning can bring powerful new analyses to bear on such problems, especially when it comes to taming nontrivial discrete combinatorics of interactions. From drug discovery to CRN correctness, we'd love to help you apply Imandra to your deepest problems.

Contractual agreements have a lot in common with algorithms. In fact, many contracts can be directly represented in a machine-reasonable way, making it possible to apply automated reasoning to understand their implications, edge-cases and potential exploits.

Imandra's cloud-native automated reasoning APIs are the ideal foundation for building next-generation contract analysis tools. We'd love to help you get started!