HAMR Installation

Distribution Mechanism

HAMR is distributed as part of the Sireum tool framework developed at Kansas State University. Installing Sireum will install HAMR as well as other tools for building programming language analysis, transformation, and verification tools. These tools include support for Slang, a safety-critical subset of Scala as well as the Logika SMT-based verifier for Slang. Installation instructions are given below.

The primary tools provided by HAMR are:

• tools for checking the well-formedness of the SysMLv2 and AADL modeling language subsets supported by HAMR,
• tools for performing different forms of light-weight verification on HAMR models, and
• tools for generating code and system build infrastructure for HAMR models.

These tools can be invoked from the command line using Sireum’s CLI interface or agentically using Sireum’s MCP server, which sireum --mcp runs and which exposes the HAMR tools to MCP clients such as AI coding assistants.

More commonly, HAMR is used in conjunction with IDEs for the modeling languages supported by HAMR, including:

• A VSCode extension called “CodeIVE” for HAMR SysMLv2 models based on the SysIDE SysMLv2 VSCode extension, and
• An Eclipse plug-in for HAMR AADL models based on the OSATE Eclipse plug-in for AADL.

Both of these expose the HAMR tools for model analysis and code generation described above as menu options within the IDEs. Problems/errors detected by HAMR are presented to the developer using the conventional IDE problems markers.

When installing Sireum, you can use included support to install the CodeIVE for using HAMR with SysMLv2 models and/or the HAMR customization of the OSATE IDE for working with AADL models.

Depending on the programming language that you want to use to program HAMR components (e.g., Rust, Slang, or C) and the target platform (e.g., seL4) you may want to install additional language tools and associated verification tools.

Supported Platforms

Sireum and HAMR, including code generation and the IDEs, run on macOS, Linux, and Windows.

The seL4 Microkit workflow (Rust, Verus, the Microkit SDK and the toolchain that builds and runs its images) is supported natively on Apple Silicon macOS and on Ubuntu 24.04 (x86_64 and arm64). Intel Macs should work but are not tested. On Windows, use the PROVERS environment’s container or VM for it.

Installation Steps - Primary Workflow (SysML, Rust)

For work related to the DARPA PROVERS INSPECTA project which focuses on SysMLv2 and Rust development/verification, you will typically want to

• Install Sireum (which includes HAMR)
• Install CodeIVE for editing SysMLv2 models and invoking HAMR
• Install Rust (if not already installed)
• Install Verus for supporting verification of HAMR-supported Rust components
• Install the seL4 Microkit SDK and the toolchain its generated builds use, if you are targeting Microkit

Tools supporting other workflows (such as using AADL for modeling or Slang for component development) are listed at the end of this page.

There are two ways to get there:

• Automated — the PROVERS environment installs all of it at one pinned set of versions, from a single script. This is the quickest route to a working machine, and the one that gives you the same versions everyone else on the program is using.

• Manual — install each piece yourself. Use this if you want a particular arrangement, are adding HAMR to a machine that already has some of these tools, or are on a platform the automated route does not cover.

Either way, see Keeping Sireum Up To Date afterwards: HAMR’s code generator moves faster than its releases, so the version you land on first is usually not the one you want to stay on.

Automated Installation (the PROVERS Environment)

The PROVERS environment is the DARPA PROVERS development environment — Verus, the seL4 Microkit SDK, LionsOS, sdfgen, Rust and Sireum/HAMR — at one pinned set of versions. It is defined once, as a set of install scripts, and delivered four ways: run on a machine of your own, as a container, as a VirtualBox VM built with Vagrant, or as a prebuilt OVA.

Full documentation is in the provers-env readme.

macOS and Linux

The same script runs natively on both — no VM, no container:

git clone https://github.com/loonwerks/INSPECTA-models.git
cd INSPECTA-models/provers-env
bash provers-setup.sh

Then open a new terminal to pick up the environment. Everything lands under $PROVERS_DIR (default ~/provers), and the environment is wired into your shell startup file. Setup is a matter of minutes.

That installs the command-line tools only. The IDEs are opt-in:

PROVERS_IVE=true PROVERS_CODEIVE=true PROVERS_FMIDE=true bash provers-setup.sh

Which Sireum you get

Left to itself, provers-setup.sh installs the Sireum revision that provers-env pins. That pin is moved by hand, deliberately, so that everyone setting up gets the same environment — which also means it lags kekinian’s master by however long it has been since the last bump. For HAMR work you usually want the current code generator instead, and SIREUM_V is how you ask for it:

SIREUM_V=dev bash provers-setup.sh      # the latest dev build, unpacked
SIREUM_V=master bash provers-setup.sh   # the exact tip, built from source

dev is the one to reach for. It is a release, so it is unpacked rather than compiled, and it is re-cut as kekinian advances — so it carries the recent code generator work without waiting for Sireum to be built from source. Take master when you need the tip exactly, or a change newer than the last dev build. Building from source is the slower of the two, but only by minutes — around ten on recent hardware, more on a slower machine.

If you already have a Sireum checkout you are working in, point SIREUM_HOME at it and that install is adopted — it is neither rebuilt nor checked out to the pinned revision, and the rest of the environment is installed around it:

SIREUM_HOME=<path-to-Sireum>/Sireum bash provers-setup.sh

Per-platform requirements and step-by-step notes:

• Setting up an Apple Silicon Mac — needs the Xcode Command Line Tools and Homebrew. This is the quickest platform to set up, because every upstream publishes an arm64 macOS build, so none of the tools are compiled from source.

• Setting up an Ubuntu 24.04 machine — needs sudo. Slower on aarch64 than on x86_64: on aarch64, Z3 and Verus are built from source, where x86_64 unpacks published releases.

Windows

provers-setup.sh does not run on Windows. Use one of the packaged deliveries instead, both built from the same scripts:

• Container — the command-line tools, suitable for builds and CI. The lighter of the two.

• Prebuilt OVA, or a VirtualBox VM built with Vagrant — a full desktop VM that also carries the GUI tools: the Sireum IVE, CodeIVE and FMIDE. Take the prebuilt OVA if you would rather not wait for a build.

Manual Installation

Sireum

You can install Sireum and its tools via source or prepackaged binaries. We outline the source-based method below which is what is emphasized on the DARPA PROVERS program, but you can find binary installers on the Sireum installation page.

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

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

(Recommended) Make the following environment variables permanent so Sireum tools are available in every terminal session: on macOS and Linux, add them to your shell configuration file (~/.zshrc for macOS’s default shell, ~/.bashrc for bash); on Windows, store them as user environment variables, which new Command Prompt windows pick up (the current window keeps its old values):

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

setx SIREUM_HOME <path-to-Sireum>\Sireum

CodeIVE

CodeIVE is Sireum’s Interactive Verification Environment built on VSCodium. It provides a ready-to-use development setup with the Sireum extension, enabling users to invoke Sireum tools such as Logika and HAMR directly within the editor. In addition, CodeIVE bundles commonly used extensions like SysIDE and Rust Analyzer, offering an integrated environment for modeling, verification, and development workflows.

CodeIVE is recommended when working with SysMLv2 models and developing Microkit projects that utilize Rust or Verus code.

$SIREUM_HOME/bin/sireum setup vscode

%SIREUM_HOME%\bin\sireum setup vscode

Launch CodeIVE

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

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

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

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

seL4 Microkit Development

The following tools are only required if you intend to work on seL4 Microkit systems. Rust and Verus are what HAMR’s Rust components are written and verified against; the SDK and the toolchain below are what a generated project’s make invokes to produce a bootable image, and are needed whether or not you verify.

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). When using Verus, you will need the one specific Rust toolchain that your Verus release is built against (see below), which need not be your default.

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 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 Verus 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.

Make sure no other copy of Verus comes ahead of it on your PATH — an older install left in place, for example. which -a verus lists every one your shell can find, first to last, and the first is the one generated builds will use; verus --version should report the version given below.

Note: Verus 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 than those considered above, we will recommend first starting with the canonical command-line installation of Verus.

Installing Verus

The current Verus version supported by HAMR is

Version: 0.2026.10.04.426d8b0
Profile: release

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

• After installing the specific Rust toolchain required by Verus, you must also add the matching standard library source (rust-src). This provides the Rust standard library source code needed by Verus and for builds targeting custom platforms such as seL4 Microkit.

  It is critical that the --toolchain flag matches the exact version that is required by Verus. For example, on macOS (Apple Silicon), Verus 0.2026.10.04.426d8b0 requires the 1.98.1-aarch64-apple-darwin toolchain, so you would run:

  rustup component add rust-src --toolchain 1.98.1-aarch64-apple-darwin
  

Keep Sireum and Verus in step. The Rust crates HAMR generates pin the vstd library of the Verus release that the code generator targets, so a Sireum and a Verus from different releases may not work together. When they do not, make fails while compiling vstd, with an error about Verus’s internals rather than your code — for example unexpected verus diagnostic item or external_trait_private_bound ... is not a private non-local bound. If you see one, check that verus --version reports the version given above and that your Sireum is current, then regenerate the code.

seL4 Microkit SDK

HAMR generates Microkit systems against SDK 2.3.1. Download the release for your platform from the Microkit 2.3.1 release — microkit-sdk-2.3.1-linux-x86-64.tar.gz, -linux-aarch64, -macos-aarch64, or -macos-x86-64 — unpack it, and point MICROKIT_SDK at the result:

tar xf microkit-sdk-2.3.1-<os>-<arch>.tar.gz
export MICROKIT_SDK=<path-to>/microkit-sdk-2.3.1
export MICROKIT_BOARD=qemu_virt_aarch64

Both variables are required: a generated build stops with MICROKIT_SDK must be specified or MICROKIT_BOARD must be specified without them.

Use the released SDK as it ships. Domain-scheduled virtual machines need 2.3.1 or later: earlier SDKs leave a VM’s vCPU outside its protection domain’s scheduling domain (seL4/microkit#586), and the guest hangs waiting for its timer.

Build Tools and QEMU

The generated makefiles invoke clang, ld.lld, llvm-ar, llvm-ranlib, llvm-objcopy, dtc, GNU Make 4 or newer, python3, and qemu-system-aarch64 to run the resulting image. They compile for the aarch64-none-elf target using clang’s built-in cross compilation, so no separate cross toolchain is needed.

brew install llvm lld dtc make wget git python@3.12 qemu

export PATH="$(brew --prefix)/opt/make/libexec/gnubin:$(brew --prefix)/opt/llvm/bin:$PATH"

sudo apt-get install -y binutils build-essential clang llvm lld \
  device-tree-compiler libxml2-utils curl wget git \
  python3.12 python3.12-venv qemu-system-arm unzip

A quick check that the toolchain is complete — every one of these should resolve, and make --version should report 4 or newer:

for t in clang ld.lld llvm-ar llvm-ranlib llvm-objcopy dtc make qemu-system-aarch64 python3; do
  command -v $t || echo "MISSING: $t"
done
make --version | head -1

Additional Tools for User-Land Scheduling

HAMR generates Microkit systems under one of two scheduling models, selected by codegen’s --scheduling option. Domain scheduling needs nothing beyond the SDK and tools above. User-land scheduling builds its system description with sdfgen and links against sDDF, so it needs two more pieces.

LionsOS, which vendors both sDDF and libvmm:

git clone https://github.com/au-ts/lionsos.git
cd lionsos
git checkout 7554a0f
git submodule update --init --recursive dep/sddf dep/libvmm
export LIONSOS=$(pwd)

Initialise only those two submodules. Cloning with --recurse-submodules pulls in the rest of what LionsOS vendors, which nothing here builds.

A generated build reports Set SDDF to a copy of https://github.com/au-ts/sddf, or LIONSOS to a checkout that vendors it at dep/sddf if LIONSOS is unset. dep/libvmm is what virtual machine components build against, under either scheduling model.

sdfgen, from PyPI. It is a Python library rather than a command-line tool — the generated meta.py imports it — so install it where the build’s python3 will find it:

python3 -m venv sdfgen-venv
sdfgen-venv/bin/pip install sdfgen==0.35.0
export PATH=<path-to>/sdfgen-venv/bin:$PATH

Keeping Sireum Up To Date

HAMR’s code generator moves faster than Sireum’s numbered releases, so the version you install first is usually not the one you want to stay on. There are three ways to land on a version, and they trade speed against currency:

So a numbered release is much the faster route, and it is the right one if you are pinning a machine deliberately — but it will not have the code generator improvements made since it was cut. If you need those, take dev for the speed or master for an exact revision.

If you installed manually, update the checkout in place and rebuild:

cd $SIREUM_HOME
git pull
git submodule update --init --recursive
bin/build.cmd

cd %SIREUM_HOME%
git pull
git submodule update --init --recursive
bin\build.cmd

To install prebuilt binaries instead, see the Sireum getting started page, which takes the release tag in SIREUM_V.

If you installed with the PROVERS environment, the same choice is SIREUM_V, and re-running the one script is enough:

SIREUM_V=4.20261021.b1efad5d bash provers-setup.sh   # a numbered release (the latest); unpacked
SIREUM_V=dev bash provers-setup.sh                   # the moving dev release; also unpacked
SIREUM_V=master bash provers-setup.sh                # build the current tip from source

Installation Steps - Alternate Workflows

HAMR supports modeling in AADL or SysMLv2, and component application development in Rust, C, and Slang. Workflows based on any combination of these is possible. For example,

• AADL for modeling, Rust for component implementation
• AADL for modeling, Slang for component implementation
• SysMLv2 for modeling, Slang for component implementation
• AADL for modeling, C for component implementation

The instructions above focus on installations to support HAMR’s current research emphases (SysMLv2 with Rust). If you want to use workflows involving AADL or Slang, you will need the following additional tools.

FMIDE (for AADL)

The Formal Methods Integrated Development Environment (FMIDE) is a customized distribution of OSATE and is recommended for high-level architectural modeling and cyber-resiliency analysis using AADL within the DARPA CASE workflow. It integrates a suite of formal analysis tools—such as AGREE, Resolute, and BriefCASE—to verify system-level safety and security properties before a single line of code is written. The bundled Sireum plugin integrates HAMR for automated, “correct-by-construction” code generation from AADL models. Additionally, the plugin integrates AWAS for visualizing and analyzing complex system information flows, ensuring safety and security properties are met at the architectural level.

$SIREUM_HOME/bin/install/fmide.cmd

%SIREUM_HOME%\bin\install\fmide.cmd

Launch FMIDE

open $SIREUM_HOME/bin/mac/fmide.app

$SIREUM_HOME/bin/linux/fmide/fmide > /dev/null 2>&1 &

$SIREUM_HOME/bin/linux/arm/fmide/fmide > /dev/null 2>&1 &

start /B %SIREUM_HOME%\bin\win\fmide\fmide.exe

IVE (for Slang and Logika)

The Sireum Integrated Verification Environment (IVE) is a customized distribution of IntelliJ IDEA specifically designed for developing high-assurance and verified software. It provides out-of-the-box support for the Slang programming language and integrates the Logika verification framework to allow for real-time, automated formal proofs of code correctness.

IVE is recommended when working with Slang/Logika projects.

$SIREUM_HOME/bin/sireum setup ive

%SIREUM_HOME%\bin\sireum setup ive

Launch IVE

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

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

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

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