Learn more
ImandraXSeamless integration of bounded and unbounded verification
ImandraX 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.
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.
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. ImandraX has deep automation for the synthesis of complex counterexamples (even in the presence of higher-order recursive functions with complex arithmetic). ImandraX 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.
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, ImandraX 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.
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, ImandraX has you covered. Our asynchronous verification plugin supports Language Server Protocol (LSP), and while we use it primarily with Visual Studio Code and Emacs, you can run with your editor of choice that also supports LSP. Furthermore, we have Jupyter notebook kernels which our Try Imandra And for the old-school hackers (like most of us at Imandra), the command line interface is there as well.
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. ImandraX 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.
CodeLogician
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.
