Introduction

ImandraX is an advanced tool for formal verification and automated reasoning, designed to enhance usability and efficiency in software development and formal methods. Building on the foundation of its predecessor, Imandra Core, it introduces significant innovations including:

• Modern User Interfaces: A native HTML-based interface, VSCode plugin with LSP integration, CLI for non-interactive workflows, and an HTTP API for seamless integration with Python and OCaml.
• Enhanced Performance: Pervasive caching and incremental proofs reduce redundant computations, enabling faster feedback loops in large projects.
• Tactic System: A sophisticated, modular system for composing proofs using advanced tactics and tacticals, offering fine-grained control over reasoning processes.
• Streamlined Runtime and API Access: Robust HTTP API and companion libraries for seamless programmatic integration and artifact management.
• Incremental and Parallel Proofs: Allows independent verification of lemmas, improving workflow flexibility even in complex proof dependencies.

ImandraX is a powerful evolution in the domain of formal reasoning, empowering developers and researchers with cutting-edge tools for rigorous and scalable analysis of systems.