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 10

Installation Options

Sireum and associated tools can be installed from sources or from prepackaged binaries.

We present the most common source-based installation approach used by our close collaborators below. Additional options can be found in the Sireum installation.

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 Instructions for all these are provided below.

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

3. Install IVE

(Interactive Verification Environment based on IntelliJ, for Slang/Logika IDE support)

From a command prompt:

%SIREUM_HOME%\bin\sireum setup ive

Launch IVE

start /B %SIREUM_HOME%\bin\win\idea\bin\IVE.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 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 &

3. 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 &

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

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

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.

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