Imandra CodeLogician
Formalize and analyze your code with automated reasoning. CodeLogician transforms source code into precise mathematical models and applies advanced reasoning techniques to uncover edge cases, decompose complex functions, and verify correctness.
Features
- Automated Formalization: Transform source code into formal mathematical models expressed in Imandra Modelling Language (IML)
- Symbolic Region Decomposition: Decompose complex functions into finite symbolic regions of invariant behavior
- Edge Case Discovery: Identify edge cases where functions behave unexpectedly
- Test Case Generation: Automatically generate test cases for different execution paths
- Verification Goals: Check properties and correctness conditions on your code
- Interactive Analysis: Queue and execute multiple commands, inspect results in real-time
- IML Exploration: Install the ImandraX Extension to interactively explore generated models
Supported Languages
CodeLogician is best supported for Python, with optimization for:
- JavaScript
- TypeScript
- Java
- C#
- Rust
- Go
- Ruby
- Kotlin
- Dart
Other languages can be analyzed, though formalization quality may vary.
Getting Started
1. Sign up for Imandra Universe
Visit Imandra Universe to create an account and generate an API key.
Open VS Code settings and search for imandra.codeLogician.apiKey, then enter your API key.
Alternatively, set the IMANDRA_API_KEY environment variable or create ~/.config/imandra/api_key.
3. Open a project
Open a project containing code in one of the supported languages.
4. Start analyzing
- Open a source file you want to analyze
- Click the Imandra CodeLogician icon in the Activity Bar
- Use Add Command to queue commands for analysis
- Use Run Commands to execute the queue
- View results in the Summary of Interactions panel
- Explore detailed views for Formalization State, Opaqueness, Region Decomposition, and Verification Goals
Tip: New users should start with the agentic formalizer for best results.
Learn More
