π-calculus, Session Types research at Imperial College

Go model checker for MiGo types, version 2

Godel2 is a model checker for MiGo types that returns results of liveness and safety checks for channels and mutex locks, as well as the presence of data races on shared pointers.

Below are instructions to try the tool-chain, which was developed for Static Race Detection and Mutex Safety and Liveness for Go Programs and has passed the ECOOP 2020 Artifact Evaluation.

Table of Contents
Overview of artifact

The artifact is a tool-chain and set of examples we used to evaluate our approach, described in Section 8 of the paper. All of the example inputs are Go program source code. We infer their MiGo types, then verify their liveness and safety following the theoretical results presented in the paper. The purpose of this page is to give instructions to reproduce the results of Table 1 (page 24). The tool-chain consists of two separate tools:

  1. MiGoInfer+ takes a Go program source code as input and infer its MiGo type; and
  2. Godel2 verifies liveness and safety properties of a MiGo type

The examples we used can be found in a dedicated repository. Additionally, we give instructions to test your own examples. You can write your own Go programs and feed them into MiGoInfer+ then Godel2 (see limitations). Alternatively, you can write MiGo types directly and check them with Godel2.

Notes on limitations

The inference tool is a prototype, and does not cover all syntax of the Go programming language. In particular, we have no support for dynamically spawning new threads and channel in unbounded (or input dependent) loops. As part of the infrastructure, some extra tools are built to help with troubleshooting in the case of inference error.


Below are instructions to run the artifact, using pre-compiled binaries (for any architecture able to run Docker with at least 2GB of available RAM and 2GB of available disk space). Alternatively, one can find the instructions to compile their own versions of the tools in their respective repositories.

Step 1: Use pre-compiled binaries

First, make sure you have Docker Desktop installed and running on your system.

Second, pull our pre-built Docker image.

docker pull jgabet/godel2

This image contains pre-compiled binaries for MiGoInfer+ and Godel2.

Step 2: Running the artifact

Our examples can be downloaded and run from our benchmark repository. The repository contains a convenience script,, to run all of the provided examples (including a warning and prompt before running the two more time-consuming ones).

The results obtained from running the tools should correspond with the results in the paper and the ones in the above repository’s README.

Alternatively, one can run their own examples using the Docker command line, as explained in Godel2’s source repository, like so:

Infer MiGo types from Go source code:

cd /path/to/example
docker run -ti --rm -v $(pwd):/root jgabet/godel2:latest migoinfer example.go > example.cgo

Model-check MiGo types:

cd /path/to/example
docker run -ti --rm -v $(pwd):/root jgabet/godel2:latest Godel example.cgo # Model check
docker run -ti --rm -v $(pwd):/root jgabet/godel2:latest Godel -T example.cgo # Termination check


We thank Nicholas Ng for his initial help in developing the tool, and David Castro-Perez and Fangyi Zhou for their comments and testing.

Related publications