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 HAMR’s MCP interfaces.

More commonly, HAMR is used in conjuction 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 Exclipse 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 customatization 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

HAMR is supported for macOS, Linux, and Windows

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-support 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. Building Sireum from source is the slower of the two paths, but only by minutes — around ten on recent hardware, more on a slower machine. Unpacking a prepackaged binary release instead is quicker still.

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.

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 of the four setups, 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, where Z3, Verus and sdfgen are unpacked from releases rather than built from source.

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) Add the following environment variables to your shell configuration file (e.g., your .bashrc file on Linux or MacOS) so Sireum tools are available for any terminal session:

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

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

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 &

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 to rely on older version(s) of Rust (see below).

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.

Installing Verus

The current Versus version supported by HAMR is

Version: 0.2026.08.09.92f466f
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.08.09.92f466f requires the 1.97.1-aarch64-apple-darwin toolchain, so you would run:

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

seL4 Microkit SDK

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

tar xf microkit-sdk-2.3.0-<os>-<arch>.tar.gz
export MICROKIT_SDK=<path-to>/microkit-sdk-2.3.0
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.

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 3945dc5
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.33.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.20260810.80aad0c2 bash provers-setup.sh   # a numbered release; 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 Intergrated 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 intergrates 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 -v 

%SIREUM_HOME%\bin\install\fmide.cmd -v

Launch FMIDE

open $SIREUM_HOME/bin/mac/fmide/fmide.app

$SIREUM_HOME/bin/linux/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 &

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