Key Features
Automation, scale, and extensibility for industrial formal verification.
Game-changing 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. ImandraX builds on these advances democratizing access to Formal Verification and dramatically increasing automation.
Speed and Scalability
With ImandraX, 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, ImandraX 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), ImandraX may be programmatically integrated into larger applications via its APIs. ImandraX is also highly extensible — its plugin infrastructure supports the installation of proprietary decision procedures for custom domains.
How ImandraX verifies and analyzes
Bounded and unbounded verification, counterexamples, modern languages, and cloud-native scale.
Seamless 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.
Documentation
Read the ImandraX docs for installation, APIs, and verification workflows.
ImandraX docsVS Code plugin
Install ImandraX in Visual Studio Code for interactive verification in your editor.
Get the plugin