Python API Examples

from rich import print  # pretty-print results (optional)
from imandra.u.agents.code_logician.graph import GraphState
from imandra.u.agents.code_logician.command import Command
from imandra.u.agents import create_thread_sync, get_remote_graph
 
##
graph = get_remote_graph("code_logician", api_key="**IMANDRA_UNI_KEY**") # add your own Imandra Universe key here
create_thread_sync(graph)
 
## Let's now create a sample Python program which we'll use to convert into IML.
src_code = """
def f(x: int) -> int:
    if x > 99:
        return 100
    elif 70 > x > 23:
        return 89 + x
    elif x > 20:
        return x + 20
    elif x > -2:
        return 103
    else:
        return 99
 
def g(x: int) -> int:
    if x < 0:
        return f(x)
    else:
        return x + 5
"""
 
# Create an empty agent state (`GraphState`), set the Python source program to the `src_code` element of the state and run the agent.
gs = GraphState()
 
# Option 1 (manual workflow): explicit control over each formalization step.
# Useful for inspecting intermediate results or customizing the pipeline.
gs = gs.add_commands(
    [
        # Initialize state with source code and language
        InitStateCommand(src_code=src_code, src_lang="python"),
        # Retrieve formalization context from the database (required before gen_model)
        GenFormalizationDataCommand(),
        # Generate and admit the IML model
        GenModelCommand(),
        # Generate region decomposition for function g (breaks down behavior by input regions)
        GenRegionDecompsCommand(function_name="g"),
        # Generate test cases from the first region decomposition
        GenTestCasesCommand(decomp_idx=0),
        # Generate and verify a property about function g
        GenVgsCommand(description="function g always returns a positive number"),
    ]
)
 
result, _ = await gs.run(graph)
fs: FormalizationState = result.last_fstate
 
print("=== Manual Workflow Results ===")
print(fs)
print(fs.iml_code) # this contains the resulting IML code
 
# Option 2 (agent workflow): automated formalization with built-in retry
# Handles refactoring, error recovery, and re-attempts automatically.
gs = GraphState()  # Create an empty agent state
gs = gs.add_commands(
    [
        # Initialize state with source code and language
        InitStateCommand(src_code=src_code, src_lang="python"),
        # Run the full agentic formalization pipeline:
        # 1. Check if code is within Imandra's capability
        # 2. Refactor code if needed
        # 3. Retrieve formalization context
        # 4. Generate IML model
        # 5. Retry with error context if admission fails
        AgentFormalizerCommand(),
    ]
)
 
result, _ = await gs.run(graph)
fs: FormalizationState = result.last_fstate
 
print("=== Agent Workflow Results ===")
print(fs)