CodeLogician Agent Skill

Agent Skills are a lightweight, open format for extending AI agent capabilities with specialized knowledge and workflows.

CodeLogician agent skill teaches an AI agent how to use IML and ImandraX: the language guide, codelogician CLI guide, verification and region-decomposition workflows, and worked examples. It is documentation your agent loads on demand, so pair it with the CodeLogician CLI or other interfaces to actually run the reasoning engine.

Pages under this section mirror the skill documentation at imandrax-tools@8531b02, published so you can read what your agent reads. To install the skill, see Installation.

• codelogicianCodeLogician: agent that utilize IML/ImandraX to reason about programs and their properties (specifications).
• async-workflowMost ways to communicating with ImandraX server support async-only workflow, which means submitting tasks non-blockingly and polling for the results (task...
• codelogician-cliInstallation options:
• eval-command`eval <expr>` evaluates a closed IML expression and reports its value. It is the
• iml-language-guideRougly speaking: IML has OCaml syntax, but:
• import-syntax1. Path Imports with Implicit Module Names:
• python-libraries`imandrax-api-models`:
• region-decomp-intro**Decomposition Goal**: To break down a function `f` into a set of regions `[ {cs_0, inv_0}, {cs_1, inv_1}, ..., {cs_m, inv_m} ]` such that the function's body...
• task-and-artifactsTask is a fundamental concept when interacting with ImandraX.
• termination-provingSince IML serves as both a programming language and a logic, function termination must be provable:
• timeoutsThere exists two types of timeouts:
• basic-verification-with-verify-and-instance`verify <func>`: takes a function representing a goal and attempts to prove it.