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.
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. 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.
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.
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.
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.
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.
