Autoformalization

Autoformalization is the step where source code, a specification, or plain prose becomes an IML model. It is the part of the workflow an LLM is genuinely good at, and the part where having a reasoning engine in the loop changes the character of the task.

Why an LLM can be trusted with this

Translating Python into IML is exactly the kind of work language models do well: pattern-heavy, syntactic, informed by context. It is also work that is normally impossible to check.

Here it is checkable. Every candidate model goes to ImandraX, which either admits it or returns specific errors: an unknown identifier, a type mismatch, a failed termination proof, a syntax error with a line and column. That is a hard, machine-generated signal, not a judgement call, and it is what makes the loop converge:

The cycle is:

1. Gather context. What types do the variables have? Which external libraries are called? Which loops need rewriting as recursion? Which mathematical functions need approximations? Static analysis of the source language supplies much of this. Type information matters most, because dynamic languages leave it implicit.
2. Generate a model. Produce candidate IML.
3. Submit it. codelogician eval check sends it to ImandraX.
4. Read the errors and refine. Errors name the problem and its location. Feed them back and try again.

Steps 3 and 4 repeat until the model is admitted. This is why the CLI is built around a fast eval loop rather than a single-shot translation: the value is in the iteration, and each round is grounded in something that cannot be hallucinated.

The error-fix corpus exists for step 4. It is a body of ImandraX errors paired with the fixes that resolve them, so common failures are recognised rather than re-derived.

Admitted is not one thing

Getting a model admitted is the first milestone. But admitted models come in two kinds, and the difference determines which analyses you can actually run.

Transparent. Every function in the model has a definition. Nothing is left to assumption. The model is executable, which means ImandraX can evaluate it on concrete inputs. That is what lets region decomposition extract sample points, and what makes test generation possible.

Opaqueness present. The model admits and type-checks, but one or more functions are declared opaque, standing in for something not modelled. You can still verify properties, and a proof over an opaque function is unconditionally strong. But the model cannot be executed, so test generation is unavailable.

This is the single most common reason gen-test produces nothing useful, and the fix is one of the two moves from Handle external dependencies: add axioms to strengthen what you can prove, or substitute an approximation to make the model executable again.

Verification goals are extracted at this point too, either from comments in the source or written by hand against the model.

The model is a deliverable, not scaffolding

It is tempting to treat the IML model as a throwaway intermediate. It is more useful than that.

One framing is model-based software engineering, or working with a digital twin: you have non-trivial code, you want to know the specification is implemented correctly, the edge cases are covered, and the behaviour can be explained. Doing that directly in Python or Java is hard. Their type systems are the first obstacle, and not the last. So you build a model you can reason about mathematically, in the way you would simulate a flight control algorithm before putting it in an aircraft.

IML is a subset of OCaml, with a few directives. Models are readable, and because they carry full type information they translate back to a source language fairly directly. They are worth keeping under version control alongside the code they model: a model that stays current is a specification that stays honest.

Where to go next

• Thinking formally: what makes a model easy to reason about
• Handle external dependencies: the fix for opaqueness
• Region decomposition: exhaustively reason about an algorithm's behaviour
• codelogician eval: the loop's commands