This section contains the HAMR reference documentation. Use the navigation tree below to browse individual chapters. For recommendations for a plan for going through the documentation, see Recommended Reading Order.
HAMR Documentation
HAMR Semantics Building Blocks and Computational Concepts
Understanding the semantics of HAMR threads (real-time tasks), port-based communication, and scheduling.
Model-Level Development with SysMLv2
System modeling and IDE support for HAMR SysMLv2 workflows.
Code-Level Development for Microkit
Building and organizing HAMR applications targeting the seL4 Microkit platform.
GUMBO Component Contracts
Model-level formal behavior specifications which HAMR translates to code to support both testing and verification.
GUMBOX Rust Executable Contracts
How GUMBO contracts are translated to Rust boolean functions so as to provide 'executable contracts' that can be used in testing and run-time monitoring.
GUMBO Verus Contracts and Formal Verification
How GUMBO contracts are translated to Verus contracts in application code, enabling formal verification that components meet their model-level specified behavior.
GUMBO System Property Specifications and Verification
Model-level formal behavior specifications for systems, which support formal verification and run-time monitoring.