Installation

Install the CodeLogician VS Code extension from the Visual Studio Marketplace

Alternatively, install directly from the extension pane in VS Code.

VS Code extensions marketplace showing the Imandra CodeLogician extension available for installation

Once installed, the extension will guide you through configuring your API key to get started. If this hasn't happened, refer to Configuration

ImandraX

For the full formal verification workflow, Imandra recommends installing the ImandraX extension. The ImandraX extension provides:

IML Support: Full IDE support for IML (Imandra Modeling Language) files
Theorem Prover: Automatically proves or disproves mathematical properties about your code
Interactive Analysis: Explore formal models and proofs interactively

This enables you to verify the formal models and verification goals generated by CodeLogician.

Basic Usage

Supported languages

CodeLogician supports the following languages:

Python
C#
Rust
Java
Kotlin
TypeScript
JavaScript
Go
Ruby
Dart

To begin, open a source file. Then open the CodeLogician extension in the sidebar.

VS Code editor with a source file open and the CodeLogician extension panel visible in the sidebar

Unsupported languages

Formalization may be possible for languages that CodeLogician does not officially support, but results may vary. Select begin to acknowledge this and continue with formalization.

CodeLogician interface showing warning message for unsupported language with option to continue formalization

Commands

CodeLogician provides various commands which can be added to a queue, which is then __ .

Most commands have prerequisites that must be satisfied before they can be used. For example, one must perform a region decomposition before test cases can be generated. The command selector marks commands whose prerequisites haven't been satisfied as unavailable.

CodeLogician command selector interface showing available and unavailable commands based on prerequisites

The Init State command is required always, so it is added to the start of the queue automatically.

The Summary of Interactions, accessed via STATE VIEWERS view in the sidebar, displays the queue.

CodeLogician Summary of Interactions panel displaying the command queue in the STATE VIEWERS sidebar

Run commands using Run pending commands. When commands conclude running, further tasks can be added to the queue.

CodeLogician interface showing the Run pending commands button to execute queued commands

CodeLogician interface showing completed command execution with option to add further tasks to queue

If a command was added by mistake, it can be removed from the queue using Delete command. Only pending commands can be removed. The Clear graph state option can be used to start from a clean slate, although it is not usually necessary.

IML

When formalizing, a formal IML model is created and saved in the code_logician/ subdirectory of the project.

VS Code project explorer showing IML model file created in the code_logician subdirectory during formalization

To update the source code after editing the IML model, first use the Set Model command, then Update Source Code.

Verification Goals

Generate verification goals by adding them to the source code as comments or submitting a VG description when adding the Generate Verification Goals command. An example follows.

Example

Source code

def g(x)
  if x > 22
    9
  else
    100 + x
  end
end
 
def f(x)
  if x > 99
    100
  elsif x > 23 && x < 70
    89 + x
  elsif x > 20
    g(x) + 20
  elsif x > -2
    103
  else
    99
  end
end

In this simple example, we use the following VG description when adding the Generate Verification Goals command:

Verify that f never returns a negative value

CodeLogician interface displaying verification goals appended to IML model with ImandraX verification results

CodeLogician has appended the verification command to the IML model, and the ImandraX extension has checked it.

JSON

Formalization data, test cases, verification goals, and region decompositions can be exported as JSON. These are also saved in the code_logician/ subdirectory of the project.