Automation
Historically, Formal Verification required considerable manual guidance from highly trained PhDs. Recent breakthroughs (e.g. SMT, automated-induction and many others) pave 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 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 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 - Satisfiability Module Theories (SMT) is one of them, which 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, non-linear 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 just 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 page runs. 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 properties of your models is difficult enough. But knowing what questions to ask is even harder. Imandra Core is more than just formal verification, it contains unique features that shine light on behaviour of complex algorithms, 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 make use of 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 even faster client experience.
