Manual GUMBOX Contract-Based Unit Testing of Thread Components

This chapter provides an overview of manual GUMBOX testing — unit tests in which the developer supplies hand-chosen inputs for a thread component and HAMR-generated contract-based test harnesses automatically judge the component’s outputs against the executable (GUMBOX) form of its GUMBO contracts. In this sense, the GUMBOX contracts form an oracle for component tests that determines if the component application code satisfies the model-declared component contracts for particular developer-selected input values.

The chapter continues with the same running examples as the preceding chapters: the Simple Isolette from the HAMR tutorials repository, in its data-port (P-DP) and event-data-port (P-EDP) variants, centered on the Thermostat thread.

We assume you have read the GUMBO Component Contracts chapter (the contracts being tested), the GUMBOX translation chapter (the executable oracles the harnesses call), and the Manual Unit Testing chapter (the base testing infrastructure — test folder layout, put_/get_ helpers, #[serial], running tests, coverage — all of which this chapter builds on). The Verus translation chapter is a companion: the harnesses here check dynamically the very clauses Verus proves statically, and the closing section develops that connection.

This chapter addresses manual GUMBOX testing only — the developer chooses each test vector. The third testing style, automated property-based GUMBOX testing (random test vectors from HAMR-generated value generators, judged by the same oracles), is covered in the Property-Based Testing chapter.

Why Manual GUMBOX Tests?

The Manual Unit Testing chapter introduced HAMR’s three styles of component testing as a ladder of increasing automation: manual unit tests (the developer supplies both the inputs and the expected-result assertions), manual GUMBOX tests (the developer supplies only the inputs), and automated property-based GUMBOX tests (a generator supplies the inputs too). This chapter is about the middle rung, and its value is easiest to see against its two neighbors.

Compared to manual unit tests, a manual GUMBOX test replaces the hand-written expected-result assertions with the component’s entire contract:

• Nothing to hand-code, nothing to get wrong. The harness evaluates the generated postcondition oracle on the observed outputs — every guarantee, every case, every integration constraint, on every run. In contrast, a hand-written assertion in a manual unit test only checks the one property its author thought of; the oracle checks all of them.
• The oracle cannot drift. When the model’s contracts evolve and code generation reruns, the GUMBOX oracles are regenerated in lock-step (GUMBOX translation); hand-written assertions must be found and updated by hand.
• Failures are contract violations by construction. A failed GUMBOX test means the implementation disagreed with the model-level specification — the same disagreement Verus would report — not merely with one engineer’s expectation.

Compared to property-based tests, a manual GUMBOX test contributes what randomness cannot:

• Chosen scenarios. Requirement-linked cases (one test per REQ_THERM_*), exact boundary values, the specific input that once exposed a bug — deterministic, repeatable, and citable in reviews and assurance arguments.
• Readable intent. A named test with a five-line input test vector documents a use case in a way a generator configuration does not; the example project’s test suites double as worked examples of each requirement.
• Specification validation. A passing manual GUMBOX test records “the contract accepts this concrete scenario I believe is correct” — evidence about the contract’s fidelity to intent, the one thing neither proof nor random testing can supply (see the GUMBOX chapter’s auditing discussion).

The three styles share one specification and one infrastructure, so using all three costs no additional contract-writing effort — and in practice they are used together: manual tests for the scenarios that matter, property-based tests for breadth, plain manual tests where no contract (yet) exists or when a developer wants to indicate the desired output beyond the level of precision provided by the contract.

Where the Support Is Generated

Everything manual GUMBOX testing needs is generated into the component crate alongside the base test infrastructure:

hamr/microkit/crates/<component>/
  src/
    bridge/
      <component>_GUMBOX.rs     <- the executable contract oracles (GUMBOX chapter)
    test/
      tests.rs                  <- your tests (developer-edited)
      util/
        cb_apis.rs              <- the contract-based test harnesses (this chapter)
        test_apis.rs            <- put_/get_ helpers and input containers
        generators.rs           <- PropTest value generators (property-based chapter)

The harnesses live in cb_apis.rs (cb = contract-based) and orchestrate the full cycle of a contract-checked execution; test_apis.rs supplies the primitive helpers they (and you) use to move values in and out of the component. As with all component testing, everything runs without seL4 libraries — in test mode the port infrastructure is Mutex-guarded statics — so the tests run anywhere cargo runs. (Reference: Manual Unit Testing — infrastructure files.)

For the DP thermostat the key files are cb_apis.rs and tests.rs; the EDP example has files of the same names.

The Harness Family

Every harness returns one of three outcomes:

pub enum HarnessResult {
  RejectedPrecondition,
  FailedPostcondition(TestCaseError),
  Passed,
}

whose meanings deserve care:

• Passed — the input vector satisfied the contract’s preconditions, the entry point ran, and the outputs (with the inputs and pre-state) satisfied the postcondition oracle: every general guarantee and every case, with cases whose antecedents did not hold counting vacuously (exactly the semantics of the GUMBOX postcondition oracle).
• RejectedPrecondition — the input vector violated the precondition oracle (an integration assume or compute assume), so the entry point was never run. The test vector is outside the component’s specified envelope: the test is inapplicable, not failed. Whether that is a mistake or the point of the test depends on what you assert (below).
• FailedPostcondition — the entry point ran on an admissible vector and its outputs violated some contract clause. This is the genuine failure outcome: the implementation disagrees with the specification.

Five harness functions cover the two entry points and the ways of supplying a vector:

The first function tests the Initialize entry point application code against the GUMBO contract for that entry point. There is only a single function for the Initialize entry because there are no input values to Initialize entry points. The many variations that follow for Compute entry point test arise due to the various approaches for providing inputs to test. Regardless, all of them enter the contracts through the same two doors: compute_CEP_Pre as the admissibility filter and compute_CEP_Post (or initialize_IEP_Post) as the oracle — see How the Test Harnesses Enter the Contracts in the GUMBOX chapter.

Anatomy of a Harness Run

The DP thermostat’s testComputeCB shows the full pipeline (generated code, verbatim):

pub fn testComputeCB(
  api_current_temp: Isolette_Data_Model::Temp,
  api_desired_temp: Isolette_Data_Model::Set_Points) -> HarnessResult
{
  // Initialize the app
  crate::thermostat_thermostat_initialize();

  // [SaveInLocal]: retrieve and save the current (input) values of GUMBO-declared local state variables
  let In_lastCmd: Isolette_Data_Model::On_Off = get_lastCmd();

  // [CheckPre]: check/filter based on pre-condition.
  if !GUMBOX::compute_CEP_Pre (In_lastCmd, api_current_temp, api_desired_temp) {
    return HarnessResult::RejectedPrecondition;
  }

  // [PutInPorts]: Set values on the input ports
  put_current_temp(api_current_temp);
  put_desired_temp(api_desired_temp);

  // [InvokeEntryPoint]: Invoke the entry point
  crate::thermostat_thermostat_timeTriggered();

  // [RetrieveOutState]: retrieve values of the output ports via get operations and GUMBO declared local state variable
  let lastCmd = get_lastCmd();
  let api_heat_control = get_heat_control();

  // [CheckPost]: invoke the oracle function
  if !GUMBOX::compute_CEP_Post(In_lastCmd, lastCmd, api_current_temp, api_desired_temp, api_heat_control) {
    return HarnessResult::FailedPostcondition(TestCaseError::Fail("Postcondition failed: incorrect output behavior".into()));
  }

  return HarnessResult::Passed
}

The bracketed step names are the harness’s fixed choreography: capture the pre-state ([SaveInLocal]), filter ([CheckPre]), stage the inputs ([PutInPorts]), dispatch ([InvokeEntryPoint]), collect the post-state ([RetrieveOutState]), judge ([CheckPost]). Note two design points. First, the harness begins by running the initialize entry point, so each test executes against a freshly initialized component — tests are independent of each other. Second, the pre-state used in the contract check is whatever initialization established (here, lastCmd == Off); testComputeCB cannot exercise other pre-states — that is the wGSV variants’ job.

Choosing the Pre-State: the wGSV Variants

Contracts that reference In(...) — like REQ_THERM_4’s “the value of the Heat Control shall not be changed” — relate the outcome to the pre-dispatch values of state variables. Testing such clauses from only the post-initialization state would leave most of their behavior unexercised. The example’s own test-design note (in the DP tests.rs) states the methodology:

The _CB based tests re-initialize the internal state of the component (including the GUMBO state variables) during each call. Therefore, we cannot use them to implement the testing approach in which we “inherit” the values of GSV from previous invocations. Instead, we follow the approach in which we explicitly force the GSV pre-state variable values to specific values on each test invocation.

testComputeCBwGSV implements exactly that: it takes the pre-state values as leading arguments and adds one step to the pipeline — after [PutInPorts] it performs

  // [SetInStateVars]: set the pre-state values of state variables
  put_lastCmd(In_lastCmd);

before invoking the entry point, and it passes the supplied In_lastCmd to both oracles. A wGSV test therefore examines one dispatch from an arbitrary, explicitly chosen state — which is also how the contract itself is stated.

Bundling Vectors: the Container Variants

Both compute harnesses have _container forms that take the HAMR-generated input-aggregation structs from test_apis.rs:

/// container for component's incoming port values
pub struct PreStateContainer {
  pub api_current_temp: Isolette_Data_Model::Temp,
  pub api_desired_temp: Isolette_Data_Model::Set_Points
}

/// container for component's incoming port values and GUMBO state variables
pub struct PreStateContainer_wGSV {
  pub In_lastCmd: Isolette_Data_Model::On_Off,
  pub api_current_temp: Isolette_Data_Model::Temp,
  pub api_desired_temp: Isolette_Data_Model::Set_Points
}

The container forms are one-line wrappers (testComputeCB_container(c) simply calls testComputeCB(c.api_current_temp, c.api_desired_temp)). One benefit of using the containers is that building a test vector utilizes Rust struct constructor, in which the name of each field is supplied. Thus, an input value for a port or state variable is directly associated with the name of the port or state variable represented in the associated struct field name. The choice of using containers vs. non-container methods is stylistic — but a named container value makes a test vector a first-class, reusable, requirement-traceable artifact, the same benefits discussed for plain manual tests in the Test Vectors section of the Manual Unit Testing chapter. The field names (api_<port>, In_<stateVar>) follow the GUMBOX parameter conventions, so a container literal reads directly against the contract.

Examining Results: the test_apis Helpers

In a pure GUMBOX test you often need no result-examination code at all — [RetrieveOutState] and [CheckPost] do it, against the whole contract. The test_apis.rs helpers matter for two situations: adding assertions beyond the contract (checking a property the contract deliberately leaves open, or pinning an exact value where the contract gives a range), and writing plain manual tests alongside the GUMBOX ones.

For output ports, get_<port>() retrieves what the component emitted. A data port always has a value:

/// getter for OUT DataPort
pub fn get_heat_control() -> Isolette_Data_Model::On_Off
{
  return extern_api::OUT_heat_control.lock().unwrap_or_else(|e| e.into_inner()).expect("Not expecting None")
}

while an event data port (EDP variant) yields an Option — None meaning no message was sent this dispatch:

/// getter for OUT EventDataPort
pub fn get_heat_control() -> Option<Isolette_Data_Model::On_Off>
{
  return extern_api::OUT_heat_control.lock().unwrap_or_else(|e| e.into_inner()).clone()
}

For GUMBO state variables, get_<var>()/put_<var>() read and write the field directly on the live component instance:

/// getter for GUMBO State Variable
pub fn get_lastCmd() -> Isolette_Data_Model::On_Off
{
  unsafe {
    match &crate::app {
      Some(inner) => inner.lastCmd,
      None => panic!("The app is None")
    }
  }
}

(and symmetrically put_lastCmd(value); the EDP variant adds get_currentSetPoints()/put_currentSetPoints(...) for its second state variable). After a harness run, get_<var>() lets a test additionally inspect the post-state — for example, confirming not just that the contract passed but that lastCmd landed on the specific value a scenario narrative calls for.

For input ports, put_<port>() stages values — a data port takes the value, an event data port takes an Option (pass None to model “no message arrived”):

/// setter for IN EventDataPort
pub fn put_temp_changed(value: Option<Isolette_Data_Model::Temp>)
{
  *extern_api::IN_temp_changed.lock().unwrap_or_else(|e| e.into_inner()) = value
}

You rarely call the input setters yourself in GUMBOX tests (the harness’s [PutInPorts] does), but they are the bridge for mixed-style suites. (Reference: Manual Unit Testing — entry point tests for the plain-manual usage of these helpers.)

Writing Manual GUMBOX Tests: the DP Thermostat

The example’s tests.rs organizes tests into modules by style (mod tests for plain manual, mod GUMBOX_manual_tests, mod GUMBOX_tests for property-based). Here is the manual GUMBOX test for REQ_THERM_2 — “If Current Temperature is less than the Lower Desired Temperature, the Heat Control shall be set to On” — verbatim:

#[test]
#[serial]
fn test_compute_GUMBOX_manual_REQ_THERM_2() {
  // generate values for the incoming data ports
  let current_temp = Temp { degrees: 95 };
  let lower_desired_temp = Temp { degrees: 98 };
  let upper_desired_temp = Temp { degrees: 100 };
  let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};

  let harness_result = 
     cb_apis::testComputeCB(current_temp, desired_temp);

  assert!(matches!(harness_result, cb_apis::HarnessResult::Passed));
}

Compare this with the corresponding plain manual test in the Manual Unit Testing chapter: the input construction is identical, but the explicit assert!(api_heat_control == On_Off::Onn) / assert!(lastCmd == On_Off::Onn) conclusions are gone. The single matches!(..., Passed) assertion is stronger than both: Passed certifies that the outputs satisfied every clause of compute_CEP_Post — the general guarantee lastCmd == heat_control, REQ_THERM_2’s case (whose antecedent 95 < 98 holds, so its consequent heat_control == Onn was genuinely checked), and REQ_THERM_3/REQ_THERM_4 (vacuously, since their antecedents do not hold on this vector). When you want to see precisely which boolean obligations that one assertion covered, read the vector against the oracles in the GUMBOX chapter’s DP walkthrough — the executable rendering is the test’s oracle.

The container form of the same test bundles the vector first:

#[test]
#[serial]
fn test_compute_GUMBOX_manual_REQ_THERM_2_container() {
  crate::thermostat_thermostat_initialize();

  // Inputs can be "bundled" into a container. 
  let preStateContainer = test_apis::PreStateContainer {
    api_current_temp : Temp { degrees: 95},
    api_desired_temp : Set_Points {
      lower: Temp { degrees:  98 },
      upper: Temp { degrees: 100 }
    }    
  };

  let harness_result = 
     cb_apis::testComputeCB_container(preStateContainer);
  assert!(matches!(harness_result, cb_apis::HarnessResult::Passed));
}

Testing In()-Clauses from Chosen Pre-States

REQ_THERM_4 ("…the value of the Heat Control shall not be changed") constrains the output relative to In(lastCmd). Its interesting scenarios start from lastCmd == Onn — a state that plain testComputeCB (which always tests from the freshly initialized Off) can never reach. The wGSV harness supplies it directly:

#[test]
#[serial]
fn test_compute_GUMBOX_manual_1_a() {
  // [InvokeEntryPoint]: invoke the entry point test method
  crate::thermostat_thermostat_initialize();

  // generate values for the incoming data ports
  let current_temp = Temp { degrees: 98 };
  let lower_desired_temp = Temp { degrees: 98 };
  let upper_desired_temp = Temp { degrees: 100 };
  let desired_temp = Set_Points {lower: lower_desired_temp, upper: upper_desired_temp};
  let last_cmd = On_Off::Onn;

  let harness_result = 
     cb_apis::testComputeCBwGSV(last_cmd, current_temp, desired_temp);

  assert!(matches!(harness_result, cb_apis::HarnessResult::Passed));
}

The temperature sits exactly on the lower bound (98 in [98, 100]), so REQ_THERM_4’s case is the one whose consequent is checked: the heat command must equal the supplied pre-state Onn. Boundary placement plus chosen pre-state is the signature move of manual GUMBOX testing — each compute_cases case gets at least one test that makes its antecedent true, at the values where off-by-one errors live.

The initialize entry point has the simplest harness of all — no inputs, so the test is one call:

#[test]
#[serial]
fn test_GUMBOX_initialize() {
  let result = cb_apis::testInitializeCB();
  assert!(matches!(result, cb_apis::HarnessResult::Passed));
}

which checks the full initialize contract (initialize_IEP_Post) — every state variable pinned, every output data port initialized.

RejectedPrecondition: Probing the Contract Envelope

What if a test vector violates the contract’s assumptions? The DP example keeps a commented-out example: supplying inverted set points (lower = 102, upper = 100) violates the compute assume ASSM_LDT_LE_UDT, so testComputeCB returns RejectedPrecondition at [CheckPre] — the entry point never runs, and an assert!(matches!(..., Passed)) fails. As the example’s commentary puts it, such an outcome “represents a failed development process step: the developer has not followed the methodology to design an appropriate test input OR the pre-condition has not been specified appropriately.”

But the same outcome, asserted deliberately, is a useful test in its own right: it documents the contract’s envelope as executable fact. The EDP suite does exactly this (below) — one test per assumption, each asserting RejectedPrecondition for a vector that violates precisely that assumption. Read the pair of idioms as: assert Passed for vectors inside the envelope (the contract judges the behavior), assert RejectedPrecondition for vectors just outside it (the test pins where the envelope’s edge is).

The EDP Variant: Choosing Events and Pre-State

In the event-data-port variant, messages may or may not be present at a dispatch — so the harness parameters for event data ports are Option-typed, and the test vector chooses the message pattern: None for “no message this dispatch,” Some(v) for “a message carrying v.” The EDP testComputeCBwGSV signature is

pub fn testComputeCBwGSV(
  In_currentSetPoints: Isolette_Data_Model::Set_Points,
  In_lastCmd: Isolette_Data_Model::On_Off,
  api_desired_temp: Option<Isolette_Data_Model::Set_Points>,
  api_temp_changed: Option<Isolette_Data_Model::Temp>,
  api_current_temp: Isolette_Data_Model::Temp) -> HarnessResult

— two pre-state variables (the latched set points and the last command), two optional event inputs, one sampled data port. The wGSV form earns its keep even more here than in the DP variant: the control law is judged against the latched currentSetPoints, so nearly every interesting scenario begins by choosing it. The EDP suite defines a small constructor to keep vectors readable:

fn sp(lower: i32, upper: i32) -> Set_Points {
  Set_Points { lower: Temp { degrees: lower }, upper: Temp { degrees: upper } }
}

A triggered control-law scenario — temperature change event, temperature below the latched range:

#[test]
#[serial]
fn test_GUMBOX_REQ_THERM_2_low_temp() {
  // (In_currentSetPoints, In_lastCmd, api_desired_temp, api_temp_changed, api_current_temp)
  let result = cb_apis::testComputeCBwGSV(
    sp(98, 101), On_Off::Off, None, Some(Temp { degrees: 96 }), Temp { degrees: 96 });
  assert!(matches!(result, cb_apis::HarnessResult::Passed));
}

One call, and Passed certifies all nine EDP guarantees at once: the latch pair (no set-point message, so the latch must be unchanged), the trigger condition (an event is present, so the control law applies), REQ_THERM_2 (96 < 98, so the command must become Onn), and the send policy (the command changed from Off to Onn, so a message carrying Onn must be on heat_control). The executable statements of all of these are in the GUMBOX chapter’s EDP section — reading a vector against them is how to understand exactly what a Passed covers.

Manual sweeps extend the same shape across boundaries and pre-states with a few lines of ordinary Rust:

#[test]
#[serial]
fn test_GUMBOX_boundary_temp_sweep() {
  // sweep the sensed temperature across the boundaries of the default
  // latched range [98, 101] (and the sensor range [95, 104]), for both
  // command pre-states
  for pre in [On_Off::Off, On_Off::Onn] {
    for t in [95, 96, 97, 98, 99, 100, 101, 102, 103, 104] {
      let result = cb_apis::testComputeCBwGSV(
        sp(98, 101), pre, None, Some(Temp { degrees: t }), Temp { degrees: t });
      assert!(matches!(result, cb_apis::HarnessResult::Passed),
        "failed for pre-state {:?}, temp {}", pre, t);
    }
  }
}

Twenty contract-checked dispatches, every boundary of the control law, both pre-states — with the context message identifying the failing combination if one ever fails. This is the deterministic middle ground between a single hand-picked vector and the property-based chapter’s randomized exploration.

Finally, the envelope-probing idiom, one test per assumption. The EDP thermostat has three kinds of assumptions (GUMBO chapter), and the suite pins each edge:

#[test]
#[serial]
fn test_GUMBOX_rejected_ill_formed_latched_set_points() {
  // the pre-state violates the INV_CSP compute assume (lower > upper),
  // so the harness rejects the vector instead of running the entry point
  let result = cb_apis::testComputeCBwGSV(
    sp(101, 98), On_Off::Off, None, Some(Temp { degrees: 96 }), Temp { degrees: 96 });
  assert!(matches!(result, cb_apis::HarnessResult::RejectedPrecondition));
}

#[test]
#[serial]
fn test_GUMBOX_rejected_out_of_range_temp() {
  // the sensed temperature violates the ASSM_CT_Range integration assume
  let result = cb_apis::testComputeCB(None, None, Temp { degrees: 200 });
  assert!(matches!(result, cb_apis::HarnessResult::RejectedPrecondition));
}

#[test]
#[serial]
fn test_GUMBOX_rejected_ill_formed_set_point_message() {
  // the incoming set point message violates the ASSM_LDT_LE_UDT
  // integration assume (lower > upper)
  let result = cb_apis::testComputeCB(Some(sp(102, 97)), None, Temp { degrees: 100 });
  assert!(matches!(result, cb_apis::HarnessResult::RejectedPrecondition));
}

Note the middle test: an out-of-range temperature is rejected by the integration assume woven into the precondition oracle — the same constraint that, on the deployed system, is discharged by the TempSensor’s verified output guarantee. The rejection tests collectively answer, in executable form, “for exactly which inputs is this component specified?”

Running the Tests

Manual GUMBOX tests are ordinary cargo tests, so everything from the Running Tests section of the Manual Unit Testing chapter applies unchanged. The essentials, GUMBOX-flavored:

• One test: click the Run Test annotation in the CodeIVE/VSCode editor, or cargo test test_compute_GUMBOX_manual_REQ_THERM_2 from the crate directory.
• One crate: from crates/<component>/, make test (or cargo test).
• Filtered subsets: the Makefile forwards a substring filter — make test args=GUMBOX_manual runs just the manual GUMBOX module, make test args=GUMBOX runs manual and property-based GUMBOX tests, cargo test REQ_THERM_2 runs every test (any style) whose name mentions that requirement. Organizing tests into modules by style, as the DP and EDP examples do, is what makes these filters precise.
• Seeing output: cargo test -- --nocapture streams the component’s log output (the log_info lines from the entry points) and any println! diagnostics — often the fastest way to see what a failing dispatch actually did.
• All crates: from hamr/microkit/, the top-level make test runs every component crate’s test suite.
• #[serial] is required on every test, GUMBOX or otherwise — component state and the port statics are shared, so tests must not run concurrently (Manual Unit Testing chapter).

None of these require the seL4/Microkit SDK or Verus — make test runs on a plain Rust toolchain.

Are Your Vectors Exercising the Contract? Coverage of the Oracles

make coverage (optionally make coverage args=GUMBOX_manual) produces the HTML coverage report described in the coverage section of the Manual Unit Testing chapter — and for GUMBOX testing, the file to study is src/bridge/<component>_GUMBOX.rs itself. Because each compute_case_* oracle is an implies!, its consequent line executes only when your vector makes the antecedent true; the Gap 2 discussion shows a reduced suite in which the REQ_THERM_2 and REQ_THERM_3 consequents have zero hits — those requirements were being checked only vacuously. The working rule from that chapter bears repeating: high coverage of the *_GUMBOX.rs consequent lines tells you your chosen vectors are actually driving each contract case; it does not by itself say the contract is correct — that is what the scenarios themselves, and contract review, are for.

Supporting Verus Verification

The harnesses evaluate, dynamically and per-vector, the same clauses that the Verus translation states as requires/ensures and proves for all vectors. That identity — one GUMBO source, one semantics, two checkers — makes manual GUMBOX testing a working companion to verification rather than a separate activity:

• Cheap bug-finding before (and alongside) proving. A GUMBOX test run takes seconds and reports failures on concrete data. Re-introduce the DP thermostat’s seeded REQ_THERM_2 bug (Rust implementation chapter) and test_compute_GUMBOX_manual_REQ_THERM_2 returns FailedPostcondition — the very violation make verus reports abstractly, demonstrated on current_temp = 95 against [98, 100]. Running the GUMBOX suite before attempting proofs clears out the ordinary bugs so verification effort goes to the genuinely hard residue.
• Understanding a puzzling clause. When it is unclear what a woven Verus clause demands in some situation, construct the situation as a harness vector and see whether it Passed — or drop below the harness and call the individual clause oracles directly on constructed values (Interrogating a Contract). The harness answers “does the whole contract accept this dispatch?”; the direct calls answer “which clause, exactly, and why?”
• Turning proof failures into regression tests. When a Verus proof fails, encode the suspect scenario as a manual GUMBOX test: if it returns FailedPostcondition, you have a runnable, reviewable demonstration of the failure — and after the fix, the same test (now asserting Passed) guards against regression. This is the harness-level counterpart of the clause-level probe developed in Explaining Verus Failures.
• Probing the assumed envelope. The RejectedPrecondition idiom makes the woven requires tangible: each rejection test documents an input the entry point is not obligated to handle — exactly the vectors Verus excludes from the proof. When a Verus proof succeeds suspiciously easily, rejection probes help check whether the preconditions are quietly excluding more than intended.
• A consistency check on the trusted base. Once a component’s Verus proof discharges, every admissible manual GUMBOX vector must return Passed — the proof covers all of them. A FailedPostcondition on verified code therefore points not at the proved logic but at the trusted base: an external_body helper, or an environment discrepancy. Keeping the GUMBOX suite running after verification is a cheap, continuous audit of exactly the parts the proof takes on trust.

What Comes Next

This chapter covered choosing test vectors by hand and letting the contract judge them. Building on it:

• GUMBOX Property-Based Testing — the Property-Based Testing chapter covers the third rung of the ladder: HAMR-generated PropTest value generators drive the same testComputeCB/testComputeCBwGSV harnesses with hundreds of random vectors, with configurable strategies for ranges, enum biases, and message-presence ratios.
• The GUMBOX translation chapter remains the reference for what each Passed actually certified, and the Verus translation chapter for the proof-side of the same contracts.

For hands-on practice, Part 2 of the tutorial series Adding GUMBO Thread Component Contracts to an Existing System walks the Simple Isolette through exactly the tests shown here — see Part 2 or follow the Recommended Reading Order.