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.
Advanced Analysis Features
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.
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.
Powerful User Interfaces
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).
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.
We work with many of the world's largest and most trusted brands, universities and government agencies.
And we would be delighted
to work with you.