CodeLogician Agent

While the specification for the state and the transition functions is provided in the next section, here we walk you through step-by-step through the process. While the user has access to low-level directives (e.g. decompose a specific function in the model), here we describe the full agentic workflow that’s also accessible.

Process revisited

To get a better idea of how the agent works, let’s go slowly through the entire process step by step. Note that while this entire process can be started, the user has access to the individual steps and can override results and add data.

Step 1: Gather formalization data CodeLogician Process Step 1 When the agent first “sees” the source program, it starts to gather information that would be useful when generating the model. This includes information about variable types, outside libraries that are referenced, complex mathematical functions that are used, etc. In addition to this data, it also tries to refactor the model so that it becomes easier to generate the resulting model. The refactoring may involve rewriting a for loop as a recusive function or wrapping global state variable into one that’s carried across functions (eliminating side-effects). We also have a collection of curated examples that may be pulled in that might be relevant to model generation.

In the prior section title “Thinking formally” we described the type of information that’s gathered and the type of refactoring that’s attempted at this stage.

Step 2: Generating the model and submitting it to ImandraX CodeLogician Process Step 2 Now that we have the full context (all the relevant information background), we can generate the model. Once we have it, we will attempt to get it admitted in ImadnraX.

Step 3: CodeLogician Process Step 3 It may be that the first attempt to submit the model will fail - in this case, we will get the information that ImandraX provided us to make modifications to the model and attempt again.

Step 4: CodeLogician Process Step 4 If we’re in the full “agentic” mode, if the agent cannot generate a model that’s admitted to ImandraX successfully after 3 tries (this is configurable), it will stop and ask for human feedback. This is referred to as ‘Human in the loop’ feature of agentic programs.

Step 5: CodeLogician Process Step 5 Eventually the model is successfully admitted to ImandraX. This may mean a number of things, depending on the state of the model:

  • Transparent - refers to the case where all of the information is contained within the model - it has no opaque functions. In this case the model is executable and we can generate test cases from it.
  • Opaqueness present - in this case opaque functions are in the model. You can still verify properties about this model, but they will be subject to any assumptions about the behavior of opaque functions. The agent will suggest that you add assumptions to the opaque functions to strengthen your verification goals, or you introduce approximations which are IML fuctions that approximate and are susbstituted for opaque functions. If you add

In either case, the agent will extract verification goals from comments within the code - note that with non-agentic functions you can manually introduce verification goals for the agent to then attempt to prove about the model.

Step 6: CodeLogician Process Step 6 In this step we assume the model is fully transparent - it is then executable and we can generate test cases. Similarly to verification goals the user can request specific functions to be decomposed and used to generate test cases.

Design of CodeLogician

Let’s now return to the design of CodeLogician, which is implemented in LangGraph as a (infinite) state machine with transition functions which can be described as through several categories:

  • Initialization and State Management - these deal with explicit change to the
    • InitStateCommand: Start a new formalization with source code
    • EditStateElementCommand: Directly modify state elements
  • Formalization Pipeline:
    • CheckFormalizationCommand - check if source code contains any functions that are hard to formalize in IML. If so, relevant context will be retrieved from the FDB to help the later formalization.
    • GenProgramRefactorCommand - refactor source code for easier formalization
    • GenFormalizationDataCommand - retrieve relevant context for formalization
    • GenModelCommand - generate IML model from source code
    • AdmitModelCommand - submit model to ImandraX for validation
    • SetModelCommand - replace the current IML model
  • Analysis and Verification:
    • GenVgsCommand - generate verification goals from the comments in the source program code
    • GenRegionDecompsCommand - generation decomposition commands from comments the source program code
    • GenTestCasesCommand - extract test cases for a specific region decomposition
  • Synchronization:
    • SyncSourceCommand - update source code based on IML model changes
    • SyncModelCommand - update IML model based on source code changes
  • User-initiated Commands:
    • SuggestFormalizationActionCommand - provide feedback on formalization failures to guide the next attempt
    • SuggestAssumptionsCommand - suggest assumptions for a specific opaque function
    • SuggestApproximationCommand - suggest approximations for a specific opaque function
  • Read-only Commands:
    • GetStateElementCommand - retrieve specific state elements (read-only)
    • SearchFDBCommand - query the formalization database for relevant information (read-only)
  • Agentic Flows:
    • AgentFormalizerCommand - execute the complete formalization pipeline with options to customize the process