Tools

This course will use the following tools, which students should have installed on laptops that can be brought to class for in-class exercises.

Sireum

Sireum is a programming language, software engineering, and formal methods framework developed at Kansas State University. This class will use Slang (the Sireum programming Language) and Logika (an automated SMT-based verification environment for Slang)

Download and installation instructions – installation based on git sources is needed for this class

Resources

While the above Sireum/HAMR installation steps will install all of the tools needed for the class, here are some links to other documentation that you might find useful.

Rust

Online Rust Book
Udemy Course on Rust – Ultimate Rust Crash Course – Nathan Stocks
- I also recommend the follow-on course Ultimate Rust Crash Course
Rustlings - free Rust exercises
PropTest Rust property-based testing framework
Verus - Rust verification tool

seL4

HAMR Installation (part of Sireum) with VSCode Extension

Windows Setup Instructions

1. Build\Install Sireum

Open a Command Prompt and run:

git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum\bin\build.cmd

(Recommended) Add the following environment variables so Sireum tools are available from any shell:

set SIREUM_HOME=<path-to-Sireum>\Sireum
set PATH=%SIREUM_HOME%\bin;%PATH%

2. Install IVE

(Interactive Verification Environment based on IntelliJ)

From a command prompt:

%SIREUM_HOME%\bin\sireum setup ive

Launch IVE

start /B %SIREUM_HOME%\bin\win\idea\bin\IVE.exe

3. Install CodeIVE

(Interactive Verification Environment based on VS Codium, for Rust and SysMLv2 IDE support)

From a command prompt:

%SIREUM_HOME%\bin\sireum setup vscode

Launch CodeIVE

start /B %SIREUM_HOME%\bin\win\vscodium\CodeIVE.exe

Linux Setup Instructions

1. Build\Install Sireum

Open a terminal and run:

git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum/bin/build.cmd

(Recommended) Add the following environment variables so Sireum tools are available from any shell:

export SIREUM_HOME=<path-to-Sireum>/Sireum
export PATH=$SIREUM_HOME/bin:$PATH

2. Install IVE

(Interactive Verification Environment based on IntelliJ)

From a terminal

$SIREUM_HOME/bin/sireum setup ive

Launch IVE

$SIREUM_HOME/bin/linux/idea/bin/IVE.sh > /dev/null 2>&1 &

3. Install CodeIVE

Interactive Verification Environment based on VS Codium, for Rust and SysMLv2 IDE support

From a terminal:

$SIREUM_HOME/bin/sireum setup vscode

Launch CodeIVE

$SIREUM_HOME/bin/linux/vscodium/bin/codeive > /dev/null 2>&1 &

macOS Setup Instructions

1. Build\Install Sireum

Open a terminal and run:

git clone --recursive https://github.com/sireum/kekinian Sireum
Sireum/bin/build.cmd

(Recommended) Add the following environment variables so Sireum tools are available from any shell:

export SIREUM_HOME=<path-to-Sireum>/Sireum
export PATH=$SIREUM_HOME/bin:$PATH

2. Install IVE

(Interactive Verification Environment based on IntelliJ)

From a terminal

$SIREUM_HOME/bin/sireum setup ive

Launch IVE

open %SIREUM_HOME/bin/mac/idea/IVE.app

3. Install CodeIVE

Interactive Verification Environment based on VS Codium, for Rust and SysMLv2 IDE support

From a terminal:

$SIREUM_HOME/bin/sireum setup vscode

Launch CodeIVE

open $SIREUM_HOME/bin/mac/vscodium/CodeIVE.app

Rust

Install Rust via rustup according to the official Rust installation instructions. You might want to take a look at the discussion of “Rust tool chains” (essentially, having different versions of Rust installed). In the future, when we start working with Verus, we will need to rely on older version(s) of Rust.

Install the Rustlings exercise framework following the instructions here

Verus

The Verus verification tool provides contract-based verification for Rust programs. What makes things a little tricky is that..

due to a variety of dependency issues, HAMR needs to work with specific versions of Verus
similarly, each version of Verus is tied to a specific version of Rust.

Fortunately, the rustup utility for Rust makes it easy to manage different versions of the Rust toolchain; you can even have multiple versions of Rust installed at the same time.

What this means is for using Rust/Verus with HAMR is…

you need to install the specific version of Verus listed on this web page
you need to use rustup to install/set the Rust tool chain to the specific version of Rust that both HAMR and Versus need

Verus binaries are distributed in .zip files; there is no dedicated installer. So you need to place the unzipped Verus files in a location of your choice, and set your PATH environment variable to include that location.

Note: Versus is also distributed via the VSCode verus-analyzer extension. Conceptually, HAMR can be used in conjunction with this extension installation. However, due to even more complex issues that those considered above, we will recommend first starting with the canonical command-line installation of Verus.

Verus Installation – Command Line

The current Versus version supported by HAMR is

Version: 0.2026.01.23.1650a05
Profile: release

With the following version of the Rust toolchain

1.92.0

Follow the installation instructions at [https://github.com/verus-lang/verus/blob/main/INSTALL.md] but with two differences:

When you get to the point where you download the appropriate release/platform zip file, pick the appropriate version for your computing from the releases for the specific version above
When you get to the step “Install the correct Rust toolchain”, use the specific version of the Rust tool chain listed above. For example, here are the instructions for MacOSx Arm

rustup toolchain install 1.92.0-aarch64-apple-darwin
rustup component add rust-src --toolchain 1.92.0-aarch64-apple-darwin