Automation
Historically, Formal Verification required considerable manual guidance from highly trained PhDs. Recent breakthroughs (e.g., SMT, automated-induction, and many others) pave the way for unprecedented automation. Imandra Core builds on these advances democratizing access to Formal Verification for non-experts and dramatically decreasing required manual guidance.
Speed and Scalability
With Imandra Core, you write executable programs and verify their properties in the same programming language. This powerful approach scales FV to even the most complex industrial problems and systems. Furthermore, Imandra Core is cloud-native and takes full 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 induction, SMT, and many other techniques
The field of Formal Verification has benefitted from the work of many great minds: from Boyer-Moore's work on automated induction and executable specifications to Larry Paulson's (and others') Isabelle to Leo De Moura's (and others') Z3 and many others.
We believe all of these great techniques complement each other, so from the beginning, we wanted to create a system that combines them all. For example, when discharging induction schemes, Imandra may find a counter-example, ultimately leveraging SMT and reflecting it into the runtime. Or, when Imandra cannot find a counter-example and does not have sufficient evidence to prove an induction hypothesis, it automatically employs bounded model-checking.
Reflection of counter-examples
Most often, either your model will have a flaw, or the property you wish to verify will be misspecified (perhaps both!). In these cases, a counter-example that you can run against the model makes all the difference. As described above, Imandra combines many different techniques - one of them - Satisfiability Modulo Theories (SMT) is employed deep inside Imandra to search for counter-examples and reflect them into the runtime. We have extended SMT to handle automatic unrolling of recursive functions, nonlinear decision procedures, and much more.
Modern interface languages
One of the main barriers to entry into FV has been the typically archaic languages used for encoding models and their properties. With Imandra, we wanted to change this. At its lowest level, Imandra Core analyzes OCaml programs (their pure subset). For Imandra, the models are programs, and the properties you wish to verify about them are also expressed in OCaml. 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, we've developed several DSLs for specific domains.
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 what questions to ask is 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. Many classes of problems are automatically distributed to available Kubernetes resources. Furthermore, intelligent caching stores intermediate results for an even faster client experience.
