The GUMBO Contract Language — Overview and Rationale

GUMBO is HAMR’s contract language for specifying the behavior of thread components at the model level. Contracts are written directly in system models — GUMBO is available in both AADL (as an annex language) and SysMLv2, and this documentation focuses on the SysMLv2 form. GUMBO’s semantics is aligned with HAMR’s execution semantics for threads and port communication, and HAMR automatically translates GUMBO contracts into code-level artifacts that support testing, formal verification, and run-time monitoring of component implementations.

This chapter presents the motivation and rationale for the GUMBO framework as a whole — why contracts belong at the model level, what makes GUMBO’s semantic grounding different from generic SysMLv2 constraint notations, and how the framework’s layers fit together. Companion chapters cover the details:

Before reading this chapter, you should be familiar with the HAMR Overview and with HAMR Modeling Elements and Semantics Concepts — in particular the notions of thread components, ports, entry points, and HAMR’s input-compute-output execution model. GUMBO’s design leans directly on those concepts.

Why Contracts at the Model Level?

In HAMR development, the architecture model is the single source of truth for a system’s structure: its components, their interfaces (ports), and their interconnections. GUMBO extends this principle to behavior — the specification of what a component is required to do lives in the model, immediately next to the ports and properties it constrains.

Placing contracts at the model level has several practical payoffs:

  • Contracts are written in the vocabulary of the architecture. A GUMBO contract refers to a component’s ports, its declared state, and model-level data types — not to the accidental details of any particular implementation language. The contract is meaningful to a systems engineer reviewing the model, even one who will never read the Rust or Slang code.

  • Contracts carry requirements traceability. GUMBO clauses are named and carry optional documentation strings, so requirements can be transcribed directly into the model with their identifiers intact. For example, in the Simple Isolette example used throughout the tutorials, the requirement “If the Current Temperature is less than the Lower Desired Temperature, the Heat Control shall be set to On” becomes a contract case named after the requirement:

    case REQ_THERM_2 "If Current Temperature is less than
                  |the Lower Desired Temperature, the Heat Control shall be set to On.":
  assume (current_temp.degrees < desired_temp.lower.degrees);
  guarantee heat_control == Isolette_Data_Model::On_Off.Onn;

    The name REQ_THERM_2 follows the requirement all the way down: HAMR propagates it into the generated code contracts and test oracles, so a failed test or verification report at the code level points back to the requirement in the model.

  • Contracts are the negotiated interface between roles. A system architect can specify integration constraints and entry point contracts before any application code exists; component developers then implement against those contracts, and integrators rely on them without inspecting component internals. The contract is the hand-off artifact.

What GUMBO Specifies Today

GUMBO currently addresses functional properties: relationships among a component’s input port values, its local state, and its output port values, as observed at each dispatch of the component. These component-level contracts also serve as the foundation for GUMBO system-level properties — end-to-end properties of the composed system, described in GUMBO System Properties.

Two important categories of properties are planned as future extensions and are not currently expressible in GUMBO:

  • Timing properties (e.g., deadlines, response-time constraints stated as contracts)
  • Information flow properties (e.g., declarations that information from one port must not influence another)

The GUMBO grammar reserves syntax for some of these (e.g., infoflow clauses), but the current verification and testing framework addresses functional behavior.

Semantic Foundations: Aligned with HAMR Execution Semantics

The meaning of a GUMBO contract is fixed by HAMR’s execution semantics, which derives from AADL’s standardized threading and port-communication concepts (see HAMR Modeling Elements and Semantics Concepts). The key ideas:

  • A thread’s application code is organized into entry points invoked by the underlying scheduling framework: the Initialize entry point runs once during the system initialization phase, and the Compute entry point runs at each dispatch during the compute phase.
  • Each dispatch is atomic with respect to inputs: input port values are frozen at dispatch (moved from the infrastructure port state into the application port state), the application computes over that consistent snapshot, and outputs are released to the communication infrastructure when the entry point completes. Execution follows the classic Read Inputs; Compute; Write Outputs discipline for analyzable real-time systems.

Because of this discipline, a GUMBO compute contract has a precise and simple reading: it is a relation between the frozen input port values and pre-state of the component at dispatch, and the output port values and post-state when the entry point completes. There is no ambiguity about “when” a contract clause is evaluated — the execution model supplies the pre- and post-points.

Core aspects of HAMR’s execution semantics have been formalized in the Isabelle theorem prover. While HAMR code generation itself is not proven correct in Isabelle, the mechanized semantics guides the design of code generation and the GUMBO contract framework, and it is used to establish the soundness of HAMR’s verification and testing approaches with respect to the abstract execution model.

Stronger than Generic SysMLv2 Constraints

SysMLv2 provides general-purpose constraint and assertion mechanisms, and the OMG community continues to develop specification notations around them. These are valuable for many modeling purposes, but they attach predicates to model elements without a fixed execution semantics: the language itself does not say when a constraint is evaluated, what state it ranges over, or how it relates to the execution of generated or hand-written code.

GUMBO takes a different approach. By tying every contract construct to a specific point in HAMR’s execution model (integration constraints to values flowing across connections; initialize contracts to the completion of the initialization phase; compute contracts to the pre/post points of each dispatch), GUMBO specifications have a strong, execution-grounded semantics. This is what makes two things possible that would be very difficult to achieve with generic model-level assertions:

  1. Stronger reasoning about components and systems — analyses can soundly compose contracts across connections and schedules because each contract has an unambiguous meaning in the execution model.
  2. Model-to-code contract correspondence — HAMR can translate a model-level contract into a code-level contract with the same meaning, so that verifying the code against the generated contract establishes conformance to the model-level specification.

One Specification, Many Verification and Testing Activities

A central GUMBO mantra is that specifications should support both testing and formal verification. HAMR realizes this by translating every GUMBO specification into two code-level forms:

  • a logical form — contracts in a code-level specification language (Verus contracts for Rust, Logika contracts for Slang) that SMT-based verification tools can discharge, and
  • an executable form — GUMBOX contracts: executable versions of the contracts rendered as boolean functions (e.g., in Rust) that can be evaluated on concrete pre/post states.

The same model-level specification therefore drives a whole portfolio of assurance activities:

Activity Level GUMBO-derived artifact used
Integration constraint checking Model Integration assume/guarantee clauses, checked when ports are connected (HAMR Logika check)
System property verification Model + generated proof crate Component contracts used as behavioral summaries (GUMBO System Properties)
Code-level formal verification Code Verus (Rust) / Logika (Slang) contracts woven into entry point skeletons
Manual unit testing with contract oracles Code GUMBOX executable contracts as test oracles
Automated property-based testing Code GUMBOX oracles + generated random-input generators
Run-time monitoring Deployed system GUMBOX executable contracts evaluated during execution

Developers can move freely along this spectrum — for example, using property-based testing against GUMBOX oracles during early development of a component and switching to full Verus verification for the most critical components — without writing any additional specifications. The Manual Unit Testing chapter illustrates GUMBOX-based testing in the current Rust workflow.

Source-Language Independence

GUMBO contracts are deliberately independent of the component implementation language: they reference only the model-level vocabulary of ports, state variables, and model data types. HAMR currently translates GUMBO to two code-level contract frameworks:

  • Rust / Verus — contracts woven into HAMR-generated Rust entry point skeletons and port APIs, verified with the Verus SMT-based verifier;
  • Slang / Logika — contracts in Slang (a safety-critical subset of Scala developed at Kansas State University), verified with the Logika verifier.

The existence of two complete instantiations is evidence that the framework achieves its language-independence goal. The same strategy could be applied to other contract-equipped targets — for example, C contract languages or SPARK Ada.

Framework Architecture: Three Layers

The GUMBO framework is best understood as three layers, each building on the one below.

Component Contracts: The Core Abstraction

GUMBO component contracts are the core of the framework. A component’s contract is an abstraction — a behavioral summary — of its thread implementation: what it assumes about its inputs, what it guarantees about its outputs and state, at initialization and at every dispatch. Every other capability in the framework consumes this summary. The structure of component contracts is the subject of the GUMBO Component Contracts chapter.

System Reasoning over Contract Summaries

GUMBO system specifications (GUMBO System Properties) reason about end-to-end properties of the composed system — for example, that a value produced by a sensor early in the static schedule is appropriately reflected in an actuator command later in the schedule. System verification uses only the component contracts together with HAMR’s scheduling model; it never inspects component implementation code. This is a deliberate scalability decision: system properties can be stated and verified in terms of small behavioral summaries, so the cost of system verification grows with the number of components and the size of their contracts — not with the volume of implementation code.

Code-Level Representations: Logical and Executable

At the bottom layer, HAMR mechanically translates each component contract into its logical form (Verus/Logika contracts) and its executable form (GUMBOX). Because both are generated from the same model artifact, evidence produced at the code level — a Verus proof, a passing GUMBOX test suite, a clean run-time monitor — discharges obligations stated at the model level. The GUMBOX translation chapter covers the executable form, and the Verus translation chapter covers the logical form together with the practice of discharging it with the Verus verifier (see Where to Go Next).

The Trusted Base

GUMBO reasoning treats the principles of HAMR’s infrastructure — the threading semantics, port communication, port freezing, and scheduling behavior described in the semantics chapter — as axioms. The correctness of HAMR’s code generation for infrastructure code is part of the trusted computing base of the framework.

This has three consequences that matter in practice:

  • Users never verify infrastructure code. Developers write and verify (or test) only the application logic of entry points. The generated glue code — port APIs, communication queues, scheduling harnesses, platform configuration — is trusted, not verified by the user.
  • Infrastructure volume does not degrade verification scalability. The quantity of generated infrastructure code (which can be large, particularly for seL4 targets) has no impact on the size or difficulty of the verification problems users face.
  • Reasoning is platform-independent. Because contracts and their verification are stated against HAMR’s abstract execution model rather than a particular platform’s mechanisms, the same contracts and the same proofs apply whether the system is deployed to the JVM, Linux, or the seL4 microkernel — and regardless of the optimizations used inside the generated infrastructure.

Where to Go Next

  • GUMBO Component Contracts — read next: an example-based walkthrough of contract structure using the Simple Isolette.
  • GUMBO Quick Reference and GUMBO Grammar — reference material for the full construct catalog and syntax.
  • GUMBO System Properties — the system-level layer, with its own technical VC reference.
  • GUMBO to GUMBOX Translation — how HAMR translates GUMBO contracts into executable Rust boolean functions for unit testing, property-based testing, and run-time monitoring.
  • GUMBO to Verus Translation — how each GUMBO clause becomes a Verus requires/ensures contract in the generated Rust application code, with the verification workflow and practical guidance on common Verus limitations.
  • The three-part tutorial series Adding GUMBO Thread Component Contracts to an Existing System (Simple Isolette), linked from the Recommended Reading Order, exercises the full path from model-level contracts through GUMBOX testing to Verus verification.