Advanced CodeLogician Features

This section covers the internals of CodeLogician: the autoformalization agent, the reasoning server, and the formalization strategies that power the platform.

IML Autoformalization Agent

The CodeLogician agent automatically translates source code into formal IML models that can be analyzed by ImandraX. It handles error recovery, dependency management, and iterative refinement.

• Introduction — overview and capabilities
• Thinking Formally — writing clear formal models
• Agent Architecture — workflow and design
• Walkthrough Examples — practical examples with Cursor

CodeLogician Server

The CodeLogician server provides a persistent, centralized service for code analysis and formal verification. It manages formalization tasks, maintains analysis state, and serves as the backend for the TUI, CLI, and IDE integrations.

Key capabilities:

• Persistent Analysis State — maintains formalization results across sessions
• Multiple Interface Support — serves the TUI, CLI, and IDE extensions
• Project Management — handles multiple codebases and strategies
• Caching — stores analysis results to avoid redundant computation
• Real-time Updates — provides live feedback during formalization

Start the server with:

codelogician server --clean ~/path/to/your/project

The --clean option removes any previously cached analysis and starts fresh. Omit it to resume from saved state.

• Metamodel Formalization — multi-model dependency management
• PyIML Strategy — Python formalization strategy
• TUI Tutorial — using the server with the TUI