Creusot Tutorial

Learn how to formally verify Rust programs with Creusot.

Contents

• Warm up exercises, taken from the slides of the POPL 2026 tutorial presentation
• Exercise 1: Gnome sort
• Exercise 2: Linked list

Check out the solutions for a quick glimpse of Creusot specifications!

Installation

Try Creusot online

You can try Creusot in your browser with Codespaces. In a few clicks, you get a ready-made VS Code session running on Github's servers, with a free quota of 120h monthly per user.

1. Click the button below, select "Machine type: 4-core", and click on "Create codespace". This will open a VS Code session in your browser.

   

2. Wait 2 minutes for the codespace to load on Github's servers.

3. Click on "Allow" if VS Code complains about an unsupported OS version.

4. You are ready to run Creusot!

Install Creusot locally

1. Follow these instructions to install Creusot.

   Note: This tutorial currently works with the master branch of Creusot.

2. (Optional) For VS Code users, you can install Creusot IDE, a VS Code extension that provides syntax highlighting and buttons to run Creusot in the editor.

   • Note: There are two parts to Creusot IDE: the extension itself, which is available on the VS Code Marketplace, and the language server Creusot LSP, which must currently be installed manually. See the README of Creusot IDE for instructions.
   • Note also: Make sure to install the "Pre-release" version of the extension.

3. Clone this repository.

   git clone https://github.com/creusot-rs/tutorial
   cd tutorial

Usage

To get started, in the terminal, run cargo creusot to check that it works. You should see some checkmarks in the output indicating that the initial examples have been proved correct.

VS Code users

If you use VS Code with Rust Analyzer (e.g., if you are on Codespaces), this tutorial repository is already set up to use Creusot to type-check on save. If you also installed the Creusot IDE extension, you should see buttons appear to the left of fn definitions in your editor; clicking on one will run SMT solvers to attempt to prove that the corresponding function satisfies its specification.

• Troubleshooting: If nothing happens in ~10 seconds after cargo creusot, you can try to relaunch the LSP server with the following commands: Ctrl+P (or click the search bar at the top) > Write "> Creusot" (with the >!) > Select "Creusot: Restart language server"".

From the command line

• Run cargo creusot to run the whole pipeline: compile to Coma and run provers.
• Run cargo creusot --prove $NAME to only try proving function $NAME. For example, cargo creusot --prove gnome_sort. This will run the Coma compiler as well to make sure the proofs are up to date.
• Run cargo creusot --only=coma to just type-check and compile to Coma.
• Run cargo creusot --only=prove to just run provers (the Coma code may be out of date!)