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@183dc80, 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).
• codelogician-cliInstallation commands:
• 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:
• 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...
• termination-provingSince IML serves as both a programming language and a logic, function termination must be provable:
• basic-verification-with-verify-and-instance`verify <func>`: takes a function representing a goal and attempts to prove it.