Unprecedented automation. Seamless integration of SMT, automated induction, nonlinear decision procedures, and much more.

Game-changing Automation

Historically, Formal Verification has required considerable manual guidance, often from highly trained PhDs. Recent breakthroughs (e.g., SMT, model-driven automated induction and nonlinear decision procedures) have paved the way for unprecedented automation. Imandra Core builds on these advances democratizing access to Formal Verification and dramatically increasing automation.

Speed and Scalability

With Imandra Core, you write programs and verify their properties in the same programming language. This approach -- rooted in efficiently executable formal models expressed in a real-world high-performance programming language -- scales to complex industrial problems and systems. Furthermore, Imandra Core is cloud-native and takes advantage of cloud computing for parallelization and intelligent caching.

Interfaces and Extensions

In addition to several powerful User Interfaces (e.g., Visual Studio Code), Imandra Core may be programmatically integrated into larger applications via its APIs. Imandra Core is also highly extensible - its plugin infrastructure supports the installation of proprietary decision procedures for custom domains.

Seamless integration of bounded and unbounded verification

Imandra has novel features supporting large-scale industrial applications, including a seamless integration of bounded and unbounded verification, first-class computable counterexamples, efficiently executable models and a cloud-native architecture designed to scale.

Seamless integration.

Imandra lifts SMT from first-order monomorphic logic without recursion to a rich computational higher-order logic with recursion and induction. This includes an adaptation of the Boyer-Moore waterfall model for automated induction to our typed, higher-order setting. The result is powerful proof and counterexample automation for a modern functional programming language.

State Dynamics Analysis

Reflection of counterexamples

In the real-world, most systems have (subtle) flaws, and huge amounts of time can be wasted attempting to prove ultimately false goals. In these cases, a succinct counterexample makes all the difference. Imandra has deep automation for the synthesis of complex counterexamples (even in the presence of higher-order recursive functions with complex arithmetic). Imandra counterexamples are first-class values reflected in the runtime and are available for running against your system in the same computational environment as the model itself.

Reflection of counterexamples.

Modern interface languages

A key barrier to entry for FV has been the archaic specification languages used for encoding models and their properties. With Imandra, your mathematical modeling langauge is a real-world programming language. At its lowest level, Imandra Core analyzes pure OCaml programs. Recently, the OCaml toolchain has become popular among web developers with a new language - ReasonML - which is effectively OCaml with a more JavaScript-like syntax. In addition to OCaml/ReasonML, Imandra supports many DSLs and has tools for their rapid construction.

Modern interface languagess.

Powerful UIs

Whether you're working on a massive development project, presenting a carefully crafted proof, or need a quick shell to iterate some ideas, Imandra Core has you covered. Our asynchronous verification plugin supports Language Server Protocol (LSP), and while we use it primarily with Visual Studio Code (see this plugin) and Emacs, you can run with your editor of choice that also supports LSP. Furthermore, we have Jupyter notebook kernels (see installation instructions) which our Try Imandra And for the old-school hackers (like most of us at Imandra), the command line interface is there as well.

Modern interface languagess.

Powerful algorithm analysis features

Knowing how to answer deep questions about the properties of your models is difficult enough. But knowing which questions to ask is often even more challenging. Imandra Core is more than just formal verification: it contains unique features that shine a light on complex algorithms' behavior, allowing you to tackle the "Unknown unknowns." For example, Imandra's Region Decomposition is an automated analysis of algorithm states-spaces - it compresses (typically infinite) state-spaces of algorithms into a finite collection of symbolic regions, each described with a set of constraints on inputs and an invariant result. Such techniques naturally complement Formal Verification.

Powerful algorithm analysis features.

Cloud-native design

While there are ample opportunities to take advantage of parallelizing reasoning in Formal Verification, few FV tools use modern cloud computing. To our knowledge, Imandra is the first cloud-native Formal Verification engine for both automatic and interactive proof. Many classes of problems are automatically distributed to available Kubernetes resources. Furthermore, intelligent caching stores intermediate results for an even faster client experience.

Cloud-native design.

Learn more
about Imandra Core

Let's talkTalk
to an Expert

a contact

Not sure
if we can help?

We'd be happy to discuss your project to suggest the best solution.

a case analysis