IML Autoformalization Agent

The CodeLogician autoformalization agent translates source code into IML (Imandra Modeling Language) models that can be analyzed by the ImandraX reasoning engine.

The agent handles:

• Automatic translation of source code into formal IML models
• Error recovery with iterative refinement when formalization fails
• Dependency management across multi-file projects

In This Section

• Introduction — overview of the agent and its capabilities
• Thinking Formally — how to write clear formal models
• CodeLogician Agent — agent architecture and workflow
• Walkthrough Examples — practical examples with Cursor