How GUMBO Contracts are Translated to Verus Contracts to Support Formal Verification of Thread Application Code

This chapter is a developer-oriented, example-based walkthrough of how HAMR translates GUMBO thread component contracts into Verus contracts — requires/ensures specifications woven into the generated Rust code, which the Verus verifier discharges to prove that a component’s application code satisfies its model-level contract. It continues with the same running examples as the GUMBO Component Contracts chapter: the Simple Isolette from the HAMR tutorials repository, first the data-port variant (P-DP) and then the event-data-port variant (P-EDP), both centered on the Thermostat thread.

We assume you have read the GUMBO Component Contracts chapter — every contract translated below is introduced and motivated there — and the Rust implementation chapter, which tours the generated component crate, the verus! macro and its constructs, and the port APIs that this chapter examines from the contract-translation perspective. The companion GUMBOX translation chapter shows the executable rendering of the very same clauses; we cross-reference it throughout, because seeing a clause in both forms — as a logical contract Verus proves and as a boolean function you can run — is often the fastest way to internalize its semantics.

This chapter addresses the logical form of the contracts: what Verus contracts HAMR generates and where, how each GUMBO contract form maps to Verus, how ghost state makes port values speakable in contracts, the workflow for running the verifier, and the Verus limitations HAMR developers most commonly meet. Testing against the executable form is covered in the Manual GUMBOX Testing and Property-Based Testing chapters.

Why Formally Verify Components?

A test evaluates a component on one input; a property-based test campaign evaluates it on thousands. A discharged Verus proof establishes that the entry point satisfies its contract on every input and pre-state the contract’s assumptions admit — including the boundary combinations no test campaign happened to generate. For high-assurance components — the kind deployed on seL4 precisely because failure is not acceptable — this is the assurance step-up that motivates writing formal contracts in the first place: the same GUMBO clauses that served as test oracles become theorems about the code.

The payoff compounds at the system level. HAMR’s compositional analyses — integration constraint checking at model assembly, and system-level property verification — consume component contracts as behavioral summaries, never component code. Those analyses are sound only if each component actually conforms to its contract; per-component Verus verification is exactly the evidence that discharges that assumption. A verified component is therefore not just locally correct — it is a trustworthy building block for every argument made about the composed system.

Verification does not retire testing. Even for a component whose Verus proof discharges completely, testing retains distinct roles:

• Validating the specification itself. A Verus proof shows the code satisfies the contract; it cannot show the contract captures the intent. An incorrect or incomplete GUMBO contract verifies just as cleanly as a correct one. Concrete test cases — and direct interrogation of the executable contracts — are how engineers and reviewers check that the specification means what they think it means (see the auditing section of the GUMBOX chapter).
• Exercising the trusted boundary. Everything marked #[verifier::external_body] — logging helpers, the FFI layer beneath the port APIs, any helper the developer exempts — is trusted by the prover, not verified. Only testing executes that code.
• Covering developer-written helpers. Helper methods and library calls in entry-point bodies have no model-level description, so HAMR generates neither Verus contracts nor GUMBOX oracles for them (details below); their correctness is the developer’s obligation, typically discharged by a mix of hand-written contracts and tests.
• Explaining and documenting. Tests are runnable, human-reviewable scenarios: they record intended use cases, and they turn abstract proof failures into concrete demonstrations anyone can run (below).

In short: Verus proves the code against the contract; testing scrutinizes the contract, the trusted base, and everything the model does not see. The two consume the same GUMBO source, so using both costs no additional specification effort.

Where the Verus Contracts Live

For each thread component, the GUMBO-derived Verus contracts are woven into two generated files in the component crate:

hamr/microkit/crates/<component>/
  src/
    component/
      <component>_app.rs         <- entry-point requires/ensures, state struct,
                                    GUMBO spec functions  (developer-edited file)
    bridge/
      <component>_api.rs         <- port API contracts: ghost port state,
                                    get_/put_ methods    (fully auto-generated)
      <component>_GUMBOX.rs      <- the executable contracts (companion chapter)

The division of labor: <component>_app.rs carries the entry point contracts — each GUMBO initialize and compute clause appears as a requires or ensures on the corresponding skeleton method — while <component>_api.rs carries the integration constraints, as contracts on the get_<port>/put_<port> methods, together with the ghost variables that make port values referable in specifications. The Rust implementation chapter walks the full generated skeleton and the verus! constructs (requires, ensures, ==>, old(...), assert(...), open spec fn, #[verifier::external_body]); here we focus on how each GUMBO form arrives in those files.

For the DP thermostat the two files are thermostat_thermostat_app.rs and thermostat_thermostat_api.rs; the EDP example has files of the same names.

Marker Regions and Contract Regeneration

The two files have different regeneration behavior, and the difference matters for day-to-day work:

• <component>_api.rs is fully auto-generated (// Do not edit this file as it will be overwritten if HAMR codegen is rerun). When contracts change in the model, rerunning code generation simply replaces it.
• <component>_app.rs is developer-edited (// This file will not be overwritten if codegen is rerun) — it holds your application logic. HAMR keeps the contract-derived material in sync by re-weaving only the regions delimited by BEGIN MARKER ... / END MARKER ... comments, leaving everything outside them untouched.

The woven regions in <component>_app.rs are:

The working rule: never hand-edit inside a marker region — change the GUMBO contract in the model and rerun code generation. Anything you type inside the markers is overwritten at the next codegen run; anything outside them (your entry-point bodies, helper functions, additional struct fields) is preserved. This is what lets contracts evolve at the model level while implementation work proceeds at the code level, with the two never drifting apart. (A component with no GUMBO contract gets PLACEHOLDER MARKER ... comments instead — placeholders that become live regions if contracts are later added, as with the DP TempSensor’s app file.)

The Translation at a Glance

Each GUMBO contract form lands in a specific place with a specific Verus shape:

And the expression-level mapping, for reading the woven clauses back to their GUMBO sources:

Every row has an executable counterpart in the GUMBOX translation: the same clause that appears here as a Verus ensures appears there as a pub fn ... -> bool. One GUMBO source, two renderings — the logical one is proved once for all inputs, the executable one is evaluated on one input at a time — and because both are generated from the same clause, they agree by construction. When a Verus clause’s meaning is unclear, calling its GUMBOX twin on a few concrete values is a quick way to see the semantics in action.

The remaining rows of the mapping — ghost variables, old(...), and the port-API contracts — need unpacking; the next three sections do so bottom-up, and then we read the entry point contracts whole.

GUMBO State Variables and the Component Struct

The GUMBO state section of the DP thermostat,

state
  lastCmd: Isolette_Data_Model::On_Off;

becomes a field of the generated component struct, with a default initial value in the constructor:

pub struct thermostat_thermostat {
  // BEGIN MARKER STATE VARS
  pub lastCmd: Isolette_Data_Model::On_Off,
  // END MARKER STATE VARS
}

pub fn new() -> Self
{
  Self {
    // BEGIN MARKER STATE VAR INIT
    lastCmd: Isolette_Data_Model::On_Off::default(),
    // END MARKER STATE VAR INIT
  }
}

The struct is the code-level realization of GUMBO-declared state: entry points receive &mut self, so contracts can relate the state before and after a dispatch. In a requires or ensures clause, old(self).lastCmd denotes the value at entry — this is exactly the translation of GUMBO’s In(lastCmd) — while a bare self.lastCmd in an ensures denotes the post-dispatch value. The model-level In() operator exists because a state variable name must be readable two ways in one clause; Verus’s old(...) is the same device in the code-level idiom.

(The default() in the constructor is a placeholder — the contractual initial value is imposed by the initialize entry point’s ensures, below. Developers may add their own non-GUMBO fields to the struct outside the markers; those are invisible to contracts, as discussed in the GUMBO chapter.)

Ghost Variables: the Abstract State of Ports

Entry point contracts must talk about port values — “the value the component read from current_temp”, “the command placed on heat_control”. But at the code level there is no variable holding “the value on the port”: inputs are fetched by calling get_ methods, outputs are released by calling put_ methods, and the actual values live in infrastructure buffers the application never sees. HAMR bridges this gap with ghost variables on the API object the entry points receive:

pub struct thermostat_thermostat_Application_Api<API: thermostat_thermostat_Api> {
  pub api: API,

  pub ghost current_temp: Isolette_Data_Model::Temp,
  pub ghost desired_temp: Isolette_Data_Model::Set_Points,
  pub ghost heat_control: Isolette_Data_Model::On_Off
}

Fields marked pub ghost exist only at verification time — Verus erases them before the code runs, so they cost nothing at runtime. Each one tracks the abstract value of one port: the specification-level answer to “what is on this port right now.” Because the entry points take api: &mut thermostat_thermostat_Application_Api<API> as a parameter, contracts can then refer to api.heat_control (the output port’s value at completion) and old(api).current_temp (the input port’s value at entry) — which is precisely how the model-level port references of GUMBO clauses are realized.

Two conventions to internalize:

• Inputs are referenced through old(api). An input port’s value is frozen at dispatch (the HAMR execution model); the contract speaks of it as part of the entry state. (In a requires clause this is also a Verus necessity — a &mut parameter has only its entry value to refer to.)
• Outputs are referenced through api. The clause constrains the value on the port when the entry point completes — the value released to the infrastructure.

In verification, the ghost input values at entry are arbitrary (constrained only by the requires clauses and the integration properties of the get_ methods below). That arbitrariness is the whole point: the proof covers every input the contract admits, not the handful a test would supply.

In the EDP variant the same mechanism represents message-oriented ports — the ghost fields for event data ports are Option<T>, None meaning “no message”:

  pub ghost current_temp: Isolette_Data_Model::Temp,
  pub ghost temp_changed: Option<Isolette_Data_Model::Temp>,
  pub ghost desired_temp: Option<Isolette_Data_Model::Set_Points>,
  pub ghost heat_control: Option<Isolette_Data_Model::On_Off>

exactly mirroring the Option<T> encoding of the GUMBOX translation.

The get_/put_ Bridge to Infrastructure

The get_<port>/put_<port> methods are where application code meets infrastructure code — and where the ghost abstraction is maintained. Each method is a verified wrapper around an unverified primitive. Here is the DP thermostat’s input side:

pub fn get_current_temp(&mut self) -> (res : Isolette_Data_Model::Temp)
  ensures
    old(self).current_temp == self.current_temp,
    res == self.current_temp,
    old(self).desired_temp == self.desired_temp,
    old(self).heat_control == self.heat_control,
    // assume ASSM_CT_Range
    (crate::component::thermostat_thermostat_app::Temp_Lower_Bound() <= res.degrees) &&
      (res.degrees <= crate::component::thermostat_thermostat_app::Temp_Upper_Bound()),
{
  self.api.unverified_get_current_temp(&Ghost(self.current_temp))
}

Read the ensures clauses in three groups:

• Framing — old(self).current_temp == self.current_temp and the analogous clauses for the other two ports say that reading this port changes no ghost state. Without framing, Verus would have to assume any call might change anything, and no contract downstream would survive. (The Rust implementation chapter discusses why framing matters at more length.)
• The binding — res == self.current_temp ties the concrete value the application receives to the ghost variable. After this call, whatever the body does with res, the prover knows it is the port value the entry point contract talks about.
• The integration assume — the last clause is GUMBO’s assume ASSM_CT_Range from the thermostat’s integration constraints, woven verbatim: every value read from current_temp lies in [Temp_Lower_Bound(), Temp_Upper_Bound()]. The application may rely on this without checking it — the obligation to actually deliver such values belongs to the producer, as we see next.

Note how the range is expressed by calling Temp_Lower_Bound() / Temp_Upper_Bound() — the GUMBO helper functions, generated into the app file’s GUMBO METHODS region as specification functions:

// BEGIN MARKER GUMBO METHODS
pub open spec fn Temp_Lower_Bound() -> i32
{
  95i32
}

pub open spec fn Temp_Upper_Bound() -> i32
{
  104i32
}
// END MARKER GUMBO METHODS

An open spec fn is a specification-only function: callable in contracts and proofs, erased from executable code. The single-sourcing of requirement constants that GUMBO helper functions provide at the model level thus carries into the verification layer (and, in executable form, into GUMBOX).

The producer side of the handshake lives in the TempSensor’s API. Its GUMBO integration guarantee temp_range becomes a requires on the put_ method:

pub fn put_current_temp(
  &mut self,
  value: Isolette_Data_Model::Temp)
  requires
    // guarantee temp_range
    (96i32 <= value.degrees) &&
      (value.degrees <= 103i32),
  ensures
    self.current_temp == value,
{
  self.api.unverified_put_current_temp(value);
  self.current_temp = value;
}

The direction flip is the heart of the integration-constraint translation: a consumer’s assume becomes something the consumer’s code gets for free (an ensures on its get_), while a producer’s guarantee becomes something the producer’s code must prove (a requires on its put_). Verus will reject any TempSensor implementation that cannot show its argument lies in [96, 103] at every call site. The handshake between the two sides — [96, 103] ⊆ [95, 104] — is discharged separately, once per connection, by HAMR’s model-level integration checking (sireum hamr sysml logika), as described in the GUMBO chapter. The executable counterparts are the GUMBOX I_Assm_<port> / I_Guar_<port> functions (GUMBOX chapter).

The thermostat’s own put_heat_control carries no integration guarantee (the DP model states none), so its contract is framing plus the ghost update:

pub fn put_heat_control(
  &mut self,
  value: Isolette_Data_Model::On_Off)
  ensures
    old(self).current_temp == self.current_temp,
    old(self).desired_temp == self.desired_temp,
    self.heat_control == value,
{
  self.api.unverified_put_heat_control(value);
  self.heat_control = value;
}

The executable statement self.heat_control = value; — an assignment to a ghost field — is how the abstraction is maintained: after the call, the ghost output value is exactly what the application sent, so the entry point’s ensures over api.heat_control can be discharged.

Where verification stops and trust begins

Each verified wrapper delegates to an unverified_* method marked #[verifier::external_body]:

#[verifier::external_body]
fn unverified_get_current_temp(
  &mut self,
  value: &Ghost<Isolette_Data_Model::Temp>) -> (res : Isolette_Data_Model::Temp)
  ensures
    res == value@,
    // assume ASSM_CT_Range
    (crate::component::thermostat_thermostat_app::Temp_Lower_Bound() <= res.degrees) &&
      (res.degrees <= crate::component::thermostat_thermostat_app::Temp_Upper_Bound()),
{
  return extern_api::unsafe_get_current_temp();
}

external_body tells Verus to trust the signature and contract without looking at the body — necessary, because the body crosses into the C bridge and seL4 shared-memory infrastructure that Verus cannot analyze. The ensures res == value@ clause (where value@ reads the ghost wrapper’s contents) is the trusted assumption that the concrete value the infrastructure delivers is the value the ghost variable tracks. This is the precise seam between the verified world and the trusted world: everything above this line (the wrapper’s framing, the entry points, your application logic) is proved; everything below it (the FFI, the queues, the kernel) is part of HAMR’s trusted infrastructure, per the execution semantics. It is also one of the standing reasons testing remains valuable — tests exercise the real path through the trusted layer.

Entry Point Contracts: Verifying Functional Behavior

With ghost port state and the port APIs in place, the entry point contracts can now say everything the model-level contracts say. Recall from the GUMBO chapter that entry point contracts are relational properties over the frozen inputs and pre-state at dispatch, and the outputs and post-state at completion. The Verus rendering is literal: pre-state is old(self) / old(api), post-state is self / api.

Initialize

The DP thermostat’s initialize contract,

initialize
  guarantee
    initlastCmd: lastCmd == Isolette_Data_Model::On_Off.Off;
  guarantee REQ_THERM_1 "The Heat Control command shall be Off initially.":
    heat_control == Isolette_Data_Model::On_Off.Off;

is woven onto the generated skeleton as:

pub fn initialize<API: thermostat_thermostat_Put_Api> (
  &mut self,
  api: &mut thermostat_thermostat_Application_Api<API>)
  ensures
    // BEGIN MARKER INITIALIZATION ENSURES
    // guarantee initlastCmd
    self.lastCmd == Isolette_Data_Model::On_Off::Off,
    // guarantee REQ_THERM_1
    //   The Heat Control command shall be Off initially.
    api.heat_control == Isolette_Data_Model::On_Off::Off,
    // END MARKER INITIALIZATION ENSURES
{
  log_info("initialize entrypoint invoked");

  self.lastCmd = On_Off::Off;
  // REQ_THERM_1: The Heat Control shall be initially Off
  let currentCmd = On_Off::Off;
  api.put_heat_control(currentCmd) 
}

Note the traceability discipline: each woven clause is preceded by a comment carrying the GUMBO clause name and its requirement prose, so the code-level contract reads back to the model (and to the requirements) line by line. There are only ensures — initialization has no inputs, so nothing to require — and the API type parameter enforces the same discipline structurally: thermostat_thermostat_Put_Api provides only put_ methods, so an initialize body cannot read inputs. The proof is direct: the assignment establishes the first clause, and put_heat_control’s ensures self.heat_control == value establishes the second.

timeTriggered

The compute contract — assume, general guarantee, and the three requirement cases from the GUMBO chapter — arrives as:

pub fn timeTriggered<API: thermostat_thermostat_Full_Api> (
  &mut self,
  api: &mut thermostat_thermostat_Application_Api<API>)
  requires
    // BEGIN MARKER TIME TRIGGERED REQUIRES
    // assume ASSM_LDT_LE_UDT
    old(api).desired_temp.lower.degrees <= old(api).desired_temp.upper.degrees,
    // END MARKER TIME TRIGGERED REQUIRES
  ensures
    // BEGIN MARKER TIME TRIGGERED ENSURES
    // guarantee lastCmd
    //   Set lastCmd to value of output Cmd port
    self.lastCmd == api.heat_control,
    // case REQ_THERM_2
    //   If Current Temperature is less than
    //   the Lower Desired Temperature, the Heat Control shall be set to On.
    (old(api).current_temp.degrees < old(api).desired_temp.lower.degrees) ==>
      (api.heat_control == Isolette_Data_Model::On_Off::Onn),
    // case REQ_THERM_3
    //   If the Current Temperature is greater than
    //   the Upper Desired Temperature, the Heat Control shall be set to Off.
    (old(api).current_temp.degrees > old(api).desired_temp.upper.degrees) ==>
      (api.heat_control == Isolette_Data_Model::On_Off::Off),
    // case REQ_THERM_4
    //   If the Current Temperature is greater than or equal 
    //   to the Lower Desired Temperature
    //   and less than or equal to the Upper Desired Temperature, the value of
    //   the Heat Control shall not be changed.
    ((old(api).current_temp.degrees >= old(api).desired_temp.lower.degrees) &&
      (old(api).current_temp.degrees <= old(api).desired_temp.upper.degrees)) ==>
      (api.heat_control == old(self).lastCmd),
    // END MARKER TIME TRIGGERED ENSURES
{
  ...
}

Reading the clauses back to their GUMBO sources:

• The compute assume ASSM_LDT_LE_UDT is the lone requires: the entry point is verified only for dispatches whose frozen desired_temp is well-ordered. As at the model level, the obligation to establish the assumption sits with whoever invokes the component — here the HAMR runtime, and, in testing, the harness’s precondition filter.
• The general guarantee lastCmd is an unconditional ensures relating post-state to output: self.lastCmd == api.heat_control.
• Each compute_cases case is an ensures implication — the case’s assume (over old(api) inputs) ==> the case’s guarantee (over api outputs and self/old(self) state). Conjoined implications reproduce the model-level case semantics exactly, and REQ_THERM_4’s In(lastCmd) surfaces as old(self).lastCmd.

This is, clause for clause, the same contract the GUMBOX chapter renders as compute_CEP_Pre and compute_CEP_Post — there as boolean functions over explicit pre/post parameters, here as requires/ensures over old(...)/current references. If a clause’s reading is ever in doubt, evaluate its GUMBOX twin on concrete values.

How the body proves

The developer’s implementation:

{
  log_info("compute entrypoint invoked");

   // -------------- Get values of input ports ------------------
  let desired_temp: Set_Points = api.get_desired_temp(); 
  let currentTemp: Temp = api.get_current_temp();

  //================ compute / control logic ===========================

  // current command defaults to value of last command (REQ-THERM-4)
  let mut currentCmd: On_Off = self.lastCmd;

  if (currentTemp.degrees > desired_temp.upper.degrees) {
     // REQ-THERM-3
     currentCmd = On_Off::Off;
  } else if (currentTemp.degrees < desired_temp.lower.degrees) {
     assert(api.current_temp.degrees < api.desired_temp.lower.degrees);
     // REQ-THERM-2
     //currentCmd = On_Off::Off; // seeded bug/error
     currentCmd = On_Off::Onn;
  }

  // -------------- Set values of output ports ------------------
  api.put_heat_control(currentCmd);
  self.lastCmd = currentCmd        
}

The proof flows through the port API contracts: each get_ call’s ensures res == self.<port> binds the local variable to the ghost port value (so currentTemp is api.current_temp as far as the prover is concerned), the branch structure mirrors the case structure, put_heat_control sets the ghost output, and the final assignment re-establishes the general guarantee. The assert(...) in the middle branch is a proof hint — an in-body assertion that restates a fact in the vocabulary of the contract (ghost port values) at the point where it holds, helping the SMT solver connect the executable comparison to the case antecedent. Hints like this are occasionally needed in larger bodies; a failing assert also makes an excellent probe when diagnosing why a proof does not go through. (The commented-out seeded bug/error line is a teaching aid we return to below.)

The EDP Variant: Events, Option, and Send Policies

The event-data-port variant exercises the message-oriented constructs. Its timeTriggered requires:

  requires
    // BEGIN MARKER TIME TRIGGERED REQUIRES
    // assume AADL_Requirement
    //   All outgoing event ports must be empty
    old(api).heat_control.is_none(),
    // assume INV_CSP
    //   The latched set points are well-formed.
    (old(self).currentSetPoints).lower.degrees <= (old(self).currentSetPoints).upper.degrees,
    // END MARKER TIME TRIGGERED REQUIRES

The first clause is not from the model’s GUMBO block at all — it is an AADL execution-model requirement HAMR adds for every outgoing event data port: at dispatch, nothing has been sent yet (None), so NoSend-style guarantees are judged against a clean slate. The second is the model’s INV_CSP compute assume over the pre-state of the latched set points.

The ensures clauses translate the latch pair, the invariant maintenance, and the trigger frame condition:

    // guarantee latchSetPointsOnEvent
    //   A newly received set point message is latched.
    api.desired_temp.is_some() ==>
      (self.currentSetPoints.lower.degrees == api.desired_temp.unwrap().lower.degrees) &&
        (self.currentSetPoints.upper.degrees == api.desired_temp.unwrap().upper.degrees),
    // guarantee latchSetPointsNoEvent
    //   Otherwise the latched set points are unchanged.
    !(api.desired_temp.is_some()) ==>
      (self.currentSetPoints == old(self).currentSetPoints),
    // guarantee invCSPMaintained
    //   Well-formedness of the latched set points is
    //   re-established for the next dispatch.
    self.currentSetPoints.lower.degrees <= self.currentSetPoints.upper.degrees,
    // guarantee noTriggerNoChange
    //   Without a triggering event (temperature change or
    //   new set points) the commanded state is unchanged.
    !(api.temp_changed.is_some() || api.desired_temp.is_some()) ==>
      (self.lastCmd == old(self).lastCmd),

and the send-on-change policy — GUMBO’s MustSend/NoSend — unfolds onto the Option-valued output ghost:

    // guarantee mustSendOnChange
    //   A command message is sent exactly when the commanded
    //   state changes, and it carries the new state.
    (self.lastCmd != old(self).lastCmd) ==>
      api.heat_control.is_some() &&
        (api.heat_control.unwrap() == self.lastCmd),
    // guarantee noSendNoChange
    //   No message is sent when the commanded state is unchanged.
    (self.lastCmd == old(self).lastCmd) ==>
      api.heat_control.is_none(),

On the API side, the integration assume on the desired_temp event data port is woven as a guarded ensures — the constraint applies to the payload only when a message is present:

pub fn get_desired_temp(&mut self) -> (res : Option<Isolette_Data_Model::Set_Points>)
  ensures
    old(self).current_temp == self.current_temp,
    old(self).temp_changed == self.temp_changed,
    old(self).desired_temp == self.desired_temp,
    res == self.desired_temp,
    old(self).heat_control == self.heat_control,
    (res.is_none() ||
      // assume ASSM_LDT_LE_UDT
      //   Incoming set point messages must be well-formed
      //   (lower desired temp at most upper desired temp).
      res.unwrap().lower.degrees <= res.unwrap().upper.degrees),
{
  self.api.unverified_get_desired_temp(&Ghost(self.desired_temp))
}

and put_heat_control records a send by setting the ghost to Some(value):

  ensures
    old(self).current_temp == self.current_temp,
    old(self).temp_changed == self.temp_changed,
    old(self).desired_temp == self.desired_temp,
    self.heat_control == Some(value),

Every one of these shapes has its executable twin in the EDP GUMBOX file — the guarded integration wrapper is I_Assm_Guard_desired_temp, the send clauses are compute_spec_mustSendOnChange_guarantee / compute_spec_noSendNoChange_guarantee — see the GUMBOX chapter’s EDP section for the side-by-side.

Helper Methods and Libraries: Your Verification Obligations

Real entry-point bodies rarely consist only of port calls and if-statements. Developers factor logic into helper methods, and reach for Rust library functionality — data structure manipulation, arithmetic utilities, encoding/decoding. Here an important boundary appears:

HAMR generates contracts only for what the model describes. Ports, state variables, and GUMBO clauses have SysMLv2 sources, so they get generated Verus contracts (and GUMBOX oracles, and test infrastructure). A helper method you write in the entry-point body has no model-level counterpart — so HAMR generates no Verus contract for it, no GUMBOX oracle, and no test support. Its specification and validation are entirely the developer’s responsibility:

• Write your own requires/ensures. For the entry point’s proof to use a helper, the helper needs a contract strong enough to support the calling context — Verus reasons about calls through contracts, not bodies.
• Or exempt it and test it. A helper marked #[verifier::external_body] is trusted; its correctness must then be established by unit tests you write (the general-purpose testing patterns of the manual unit testing chapter apply, even though no GUMBOX oracle exists for it).
• Either way, test it. Even verified helpers benefit from example-based tests as documentation and as a check on the contract’s intent — the same spec-validation argument as for component contracts.

The EDP thermostat contains a small, instructive example — a developer-written helper with a developer-written contract:

// Executable equality test on On_Off command values.
// NOTE: inside verus! blocks, `==` cannot be used on enums from the `data`
// crate in EXECUTABLE code (the derived PartialEq is external to Verus);
// pattern matching is used instead.  In SPEC position (the ensures clause
// below), `==` denotes Verus structural equality and is fine.
pub fn on_off_eq(a: On_Off, b: On_Off) -> (res: bool)
  ensures res == (a == b)
{
  match (a, b) {
    (On_Off::Onn, On_Off::Onn) => true,
    (On_Off::Off, On_Off::Off) => true,
    _ => false,
  }
}

The ensures bridges the executable result to Verus’s structural equality, so the send-on-change body can branch on on_off_eq(currentCmd, self.lastCmd) and the prover still connects the branch condition to the self.lastCmd != old(self).lastCmd antecedents in the contract. (Why the helper is needed at all is a Verus limitation — next-but-one section.)

The Verification Workflow

The rhythm of contract-driven development with Verus, assembled from the pieces above:

1. Author or evolve GUMBO contracts in the model, and type-check (sireum hamr sysml tipe).
2. Run code generation. Contracts are woven into the marker regions of <component>_app.rs and into a fresh <component>_api.rs; your code outside the markers is preserved.
3. Implement (or adjust) the entry-point bodies, adding helper functions with their own contracts as needed.
4. Verify: from the component crate, make verus — the fastest check, running cargo-verus verify without producing build artifacts. make verus-json emits machine-readable results to verus_results.json; from hamr/microkit/, a top-level make verus verifies every component crate.
5. When a proof fails, Verus names the entry point and the specific requires/ensures clause that could not be established. Then:
   • if the body is wrong, fix the logic (the clause comment’s requirement text tells you what behavior is expected — and a GUMBOX probe can demonstrate the failure concretely, below);
   • if the proof needs help, add assert(...) hints restating key facts in contract vocabulary, or strengthen a helper’s contract;
   • if the contract is wrong or incomplete, fix it in the model and return to step 1 — never by editing inside the marker regions.
6. Keep testing. make test runs the crate’s unit and property-based suites without requiring verification; the two evidence streams are complementary.

Verification is also wired into the build: the top-level make all builds component crates with cargo-verus, so a system image is only produced from code that verifies (set RUST_MAKE_TARGET=build-release to bypass during exploratory work). None of the verification targets require the seL4/Microkit SDK — make verus runs anywhere Rust and cargo-verus are installed.

Verus Limitations You Will Encounter

Verus verifies a subset of Rust, and HAMR developers meet its edges in predictable places. The three most common, with their standard workarounds:

String formatting and logging. The log:: macros perform formatting that Verus cannot reason about, so every logging helper is marked #[verifier::external_body]:

#[verifier::external_body]
pub fn log_info(msg: &str)
{
  log::info!("{0}", msg);
}

HAMR generates the basic helpers this way, and any logging function you add (e.g., one formatting a data value with {0:?}) needs the same attribute. This is the single most frequent reason for external_body in HAMR components.

Equality on data-model enums in executable code. Types in the data crate derive PartialEq outside any verus! block, so their == operator is an external function Verus refuses to call in executable positions (spec positions are fine — there == is Verus’s structural equality). The error reads like:

error: cannot use function `data::..::impl&%11::eq` which is ignored because it is
       either declared outside the verus! macro or it is marked as `external`

The workaround is pattern matching, packaged once in a small helper with a bridging contract — exactly the on_off_eq function shown above.

Runtime logic Verus cannot digest. Occasionally a body needs an operation outside Verus’s supported subset (complex slice manipulation, third-party library calls). The escape hatch is again #[verifier::external_body] on a helper that isolates the operation behind a contract. Use it sparingly and deliberately: everything so marked joins the trusted base — the prover believes its contract without proof — which is precisely why such helpers should carry unit tests, and why testing retains a permanent role alongside verification.

Explaining Verus Failures with Executable Contracts

A failing Verus proof names a clause; it does not hand you a concrete scenario. For the developer that is often enough, but for code review, issue reports, and regression protection, a runnable demonstration of the failure is far more useful — and the GUMBOX rendering of the same contract provides exactly that, as developed in the GUMBOX chapter’s Interrogating a Contract section.

The DP thermostat ships with a worked instance: the seeded bug kept in its body as a comment,

     // REQ-THERM-2
     //currentCmd = On_Off::Off; // seeded bug/error
     currentCmd = On_Off::Onn;

Re-introducing the bug (uncomment the first line, remove the second) and running make verus produces a failure on the timeTriggered ensures clause labeled case REQ_THERM_2 — the verifier has determined that some dispatch violates the requirement, but reports it in proof terms. The GUMBOX clause function compute_case_REQ_THERM_2 restates the finding as a test anyone can run and read:

use crate::bridge::thermostat_thermostat_GUMBOX as GUMBOX;

#[test]
fn explain_verus_failure_REQ_THERM_2() {
  // Below range (96 < 98) the buggy body emits Off; REQ_THERM_2 requires Onn.
  assert!(!GUMBOX::compute_case_REQ_THERM_2(
    temp(96), set_points(98, 101),
    On_Off::Off));   // what the buggy implementation emits
}

(The temp/set_points constructors and the full probing technique are in the GUMBOX chapter.) Once the bug is fixed, invert the assertion — the clause holds on the corrected output — and keep it as a regression test. The same move works in the other direction: when a proof fails and you suspect the contract rather than the code, probing the GUMBOX oracles with scenarios you believe should be accepted or rejected tells you what the specification actually says — turning “the prover won’t accept my code” into a concrete conversation about either the code or the model, whichever is actually wrong.

What Comes Next

This chapter covered the logical rendering of GUMBO contracts and the practice of discharging them with Verus. Building on it:

• Manual GUMBOX Unit Testing — the Manual GUMBOX Testing chapter covers driving the generated contract-checked test harnesses with chosen inputs.
• GUMBOX Property-Based Testing — the Property-Based Testing chapter covers automated exploration of the input space against the same contract oracles.
• The GUMBOX translation chapter is the standing companion: one specification, proved here, executed there.

For hands-on practice, Part 3 of the tutorial series Adding GUMBO Thread Component Contracts to an Existing System takes the Simple Isolette through Verus verification of the thermostat — see Part 3 or follow the Recommended Reading Order.