HAMR ("[H]igh [A]ssurance [M]odeling and [R]apid engineering for embedded systems’’) is a framework for model-based development of critical systems. HAMR emphasizes three layers of development, explained below.
-
System architecture models are specified using either the Architecture Analysis and Design Language (AADL) or SysMLv2.
-
HAMR generates code for system infrastructure including inter-component communication, real-time tasking infrastructure, and scheduling. For application components, HAMR generates code skeletons with entry points that are invoked by the underlying scheduling framework. Developers fill in these code skeletons with application logic to complete the behavior of the system. HAMR supports code generation and application development in Rust, C, and Slang (a safety-critical subset of Scala).
-
HAMR generates deployment infrastructure for the JVM, Linux, and the seL4 microkernel.
A key theme of HAMR is the incorporation of developer-friendly formal methods that are integrated to work synergistically across the three development layers above. For example, in models, developers can include behavior contracts written the GUMBO contract language. When HAMR generates code, it translates GUMBO contract down into source code contract languages. This enables code level verification tools (e.g., Verus for Rust, and Logika for Slang) to verify the application code conforms to code-level and model-level contracts. HAMR also generates infrastructure for property-based testing against GUMBO-derived test oracles, allowing developers to seamlessly switch between using testing and formal verification to ensure that application conforms to contracts. HAMR deploys code on the seL4 micro-kernel, whose functionality and partitioning have been mathematically proven correct in the Isabelle theorem prover. HAMR’s run-time semantics is modeled in the Isabelle theorem prover, which guides HAMR implementation and enables to prove the soundness of HAMR analysis and verification techniques. HAMR’s application assurance framework helps developers organize correctness claims about their system and to manage the accumulation of assurance evidence for those claims across all three layers of development.
To learn more about HAMR,
-
read a short paper from DASC 2025 about how HAMR is being used in the Collins Aerospace INSPECTA tool chain for high assurance systems
-
read a short HAMR Overview, then a longer HAMR Tour
-
watch overview videos
- HAMR Overview (with emphasis on SysMLv2 based development with Rust) - (Part 1 - model-level development (video, slides)
- HAMR for seL4 (with emphasis on Rust language development, verification, and testing) - keynote talk given by John Hatcliff at the August 2025 seL4 Summit (video, slides). This talk has some overlap with HAMR Overview above, but includes more background on motivation for HAMR’s support for seL4 and details of HAMR integration with seL4.
-
read an older journal article on HAMR C code generation for the seL4 micro-kernel using the CAmkES framework and its application on the DARPA CASE project.
HAMR is being used in several US Department of Defense research projects. The links below include information on the broader objectives of these projects,
- The INSPECTA Project - DARPA PROVERS program - with Collins Aerospace (lead), Dornerworks, CMU, University of New South Wales, University of Kansas.
- (concluded) DARPA Cyber-Assured Systems Engineering (CASE) - with Collins Aerospace (lead), Adventium Labs, and Data61. Collins Aerospace team web site: CASE Overview
HAMR is an project released under the Simplified BSD license.