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 Options

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 FMIDE for editing AADL 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.

Sireum

You can install Sireum and its tools via source or prepackaged binaries. We outline the source-based method below, 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 so Sireum tools are available from any shell:

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%

IVE

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

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

FMIDE

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

seL4 Microkit Development

The following tools are only required if you intend to work on seL4 Microkit systems requiring Rust/Verus formal verification.

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.01.23.1650a05
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.01.23.1650a05 requires the 1.92.0-aarch64-apple-darwin toolchain, so you would run:
```
rustup component add rust-src --toolchain 1.92.0-aarch64-apple-darwin
```