The Staff Engineer Correctness Testing Interview: Invariants, Histories, and Fault Injection

Imagine your reservation service passes every test, then promises the last available unit to two customers. The interview follow-up is simple: which assertion would have caught that before launch? A list of testing tools cannot answer it; a precise definition of correct behavior can.

Use that question to structure your next senior or staff engineer practice session. Start with a contract, choose an oracle that can reject violations, and explain what each experiment leaves unproven. This guide develops that approach through a hypothetical inventory service. The examples and practice rubric are illustrative, not a description of any employer's hiring criteria or a guarantee of interview results.

1. Write the oracle before choosing the tools

An oracle is the rule that decides whether an observed result is acceptable. Coverage answers a different question. Google's explanation of coverage data distinguishes executing statements from exercising all paths and notes that coverage cannot reveal missing behavior by itself. For this interview, propose coverage as a way to find gaps, then identify the assertions that protect customers.

Define a small service with reserve, confirm, and cancel operations. Assume a fixed initial stock, no replenishment, no expiration, and whole-unit quantities. Confirmation converts a held reservation into a completed sale; cancellation releases only a held reservation. Those constraints keep the example focused. Ask the interviewer before adding expiration or cancellation of completed sales, because either changes the specification.

Write properties against logical operations and authoritative state:

• Conservation: available units plus units in held reservations plus completed sales always equal initial stock; none of those quantities is negative.
• Unique effect: retrying an identical request with the same idempotency key returns its original result without consuming stock again. Reusing that key with a different payload is rejected.
• Valid transitions: a reservation can move from held to confirmed or canceled once; repeating cancellation cannot release additional units.

Separate these safety requirements from progress. The AWS formal-methods experience paper distinguishes properties about permitted behavior from properties about what must eventually happen. For our service, eventual completion needs environmental assumptions: storage recovers, communication resumes, and work gets scheduled. A test deadline can expose failure to meet an operational target; it cannot establish eventual progress under every future schedule.

Also define how the oracle obtains a consistent view. Reading each counter independently during concurrent updates could produce a combination that never existed. Use a transactional snapshot, an operation history, or a deliberately quiescent verification phase. Specify the read's guarantees so the checker does not manufacture a failure.

Challenge the checker before trusting it. Feed it an intentionally invalid history containing two successful reservations for the final unit and confirm that it rejects the history. Then feed it a legal overlap and confirm that it accepts. For state assertions, introduce a controlled double-release defect in a test fixture. Explain which check fails and why. These are proposed checks of your harness, not evidence that the production service has that defect.

2. Generate operations that challenge the contract

Make the reference model simpler than the implementation

Begin with a sequential in-memory model: stock, reservations, and an idempotency-key map. Run the same commands against that model and the service, comparing results and state at defined checkpoints. Keep it independent of the production transition code. Copying the implementation into the oracle risks giving both the same mistake.

Hypothesis stateful testing generates sequences of actions as well as inputs. Its rules can reuse values produced by previous operations, and invariants can run after each step. For our example, retain reservation identifiers and request keys so later actions can confirm, cancel, or retry earlier work. This is more targeted than generating unrelated random requests.

Include deliberate invalid operations: confirm an unknown identifier, cancel twice, reserve beyond available stock, and retry a key with altered quantity. Give every rejected request an expected state effect: none. Avoid preconditions that filter out all invalid transitions, because that would exclude the behavior you intended to check. Save the short failing action sequence as a regression example.

Use fuzzing and race detection for their actual scope

Go's native fuzzer uses coverage guidance to explore inputs and retains failing inputs for subsequent regression runs. Apply it to a request decoder, identifier parser, or compact encoding of model commands. Assert round-trip preservation where the format promises it, rejection of invalid quantities, and unchanged state after rejected commands. A no-panic assertion alone would miss a decoder that silently changes a quantity.

Keep each fuzz invocation isolated and reproducible; Go's documentation recommends deterministic targets without persistent state across calls. For concurrent Go code, add go test -race. The race-detector documentation explicitly limits detection to races exercised at runtime. A race-free handler can still perform a logically incorrect read-check-write transaction. Treat memory-race detection and business-invariant checking as separate evidence.

Choose concurrency deliberately too. In a controlled test, pause two distinct reservation requests after their availability reads, then release both toward the update boundary. Ask whether the storage transaction rejects one or permits an invalid result. Describe the synchronization hook as part of the test harness. If your generated workload only invokes requests sequentially, its success provides no evidence about this overlap, regardless of how many input values it explored.

3. Check concurrent histories and unknown outcomes

A sequential state-machine test does not establish that overlapping requests obey the same contract. Record operation invocations and completions with client identity, request key, arguments, returned values, and outcome classification. Then ask whether the observed history admits a legal explanation under the chosen consistency model.

Herlihy and Wing's linearizability paper formalizes the idea that each operation appears to take effect at one point between invocation and response. If operation A completes before B begins, their explanation must preserve that order. Overlapping operations may be ordered either way, provided their return values fit the sequential specification.

Suppose one unit remains and two distinct reservation requests overlap. If both return success, neither possible ordering is legal: the second reservation in either order should fail. By contrast, one success and one rejection can be legal. Final stock alone is insufficient evidence; a later compensation might restore the count after two customers already received success.

Specify the checker's scope. Jepsen's linearizability guide describes it as a single-object model and distinguishes it from strict serializability across multiple objects. For this exercise, model one inventory pool with all reservation transitions together. Independently checking an inventory counter and a reservation map would miss contradictions between them. If the design promises multi-object transactions, select a checker for that transactional contract.

A timeout is an observation, not a rollback

Consider a server that commits a reservation, then loses the response. Marking that attempt as definitely unapplied would make the history inaccurate. The Jepsen client tutorial distinguishes known failures from indeterminate operations that might have taken effect. Preserve that uncertainty and allow the checker to consider legal completions of incomplete operations.

Retry with the original key, then query durable reservation state when the contract supports reconciliation. Record each attempt while keeping their shared logical identity. If a key lookup is unavailable, retain the unknown outcome. Likewise, report a checker that exhausts its computation budget as inconclusive; a checker timeout does not establish either a valid history or a counterexample.

Preserve the history recorder's assumptions as well. Prefer recording invocation and completion events through one controlled harness rather than inferring their order from server wall-clock timestamps. Include setup operations and the initial stock in the evidence bundle. If the harness crashes and loses completions, describe the affected operations as incomplete instead of silently deleting them. The checker should evaluate the evidence you have, with its uncertainty visible.

4. Connect models, simulation, and implementation evidence

Explore a finite protocol model

Use TLA+ when a protocol decision needs systematic exploration before implementation. Model the state, initial conditions, and allowed transitions, including crashes and delayed messages. For our example, a small configuration might contain two clients, one stock unit, and a bounded message collection. Those are proposed exploration limits, not published recommendations.

Yu, Manolios, and Lamport's TLC paper explains choosing a finite model and exploring reachable states for invariant violations. Report which model and bounds completed checking. Do not turn that into a claim that arbitrary cluster sizes or production code have been proved correct. In particular, making a reserve transition atomic in the model can hide the read-check-write race present in an implementation.

Map each counterexample back to an implementation test. A trace where a crash loses the idempotency record but preserves the stock decrement suggests a specific durability test. Conversely, an implementation failure may reveal that the model omitted an intermediate state. Let evidence improve both artifacts.

Make difficult executions replayable

The FoundationDB SIGMOD paper describes running real database software with workloads and faults in a deterministic discrete-event simulator. It abstracts sources such as network, disk, time, and randomness, and uses workload assertions as test oracles. The important interview lesson is architectural: reproducible exploration requires control over nondeterminism, alongside meaningful checks.

For a smaller service, propose injectable clocks, a controllable transport, and explicit storage-failure points around reservation commits. Preserve the seed, workload, build, and configuration for replay. If thread scheduling or an external dependency remains uncontrolled, state that limitation. A seed alone does not define an entire execution.

Keep a separate validation path against real storage and deployment components. Simulation can challenge implementation behavior in modeled environments; a formal model can challenge protocol logic. Neither automatically verifies assumptions about actual disk persistence, network behavior, or adapters. Choose the next experiment by identifying which assumption remains unsupported.

5. Design a bounded experiment and rehearse the argument

Choose a fault because it can expose a specific contract violation. For our service, interrupt the response path after durable reservation commit, then retry the identical request through another instance. Check that only one logical reservation exists, its returned identity is stable, and stock conservation holds. State how the harness establishes that the fault occurred at the intended boundary; random packet loss alone does not prove it exercised that case.

Define targets, duration, cleanup, and stop conditions before running an infrastructure experiment. AWS Fault Injection Service stop conditions use CloudWatch alarms to stop experiments when defined thresholds are reached. That mechanism bounds an experiment; the alarm is not your correctness oracle. An acceptable latency graph cannot establish that reservations were unique.

After stopping fault injection, verify resource recovery and run reconciliation. Stopping the experiment does not undo an incorrect business transition. Keep both the observed history and the final authoritative-state checks, and explain any gap between them. Start with controlled test environments and expand only when the question requires deployment-specific evidence.

Write an outcome statement that another engineer could assess: the intended fault was observed, these operations were recorded, these invariants were checked, and these outcomes remain unresolved. If the response interruption never happened, label the experiment as missing its target. A healthy run that skipped the failure boundary should send you back to the harness before you claim confidence in retry correctness.

An illustrative practice rubric

Give yourself a short mock interview and score these dimensions from zero to two: zero means absent, one means named, and two means demonstrated with the reservation example. This is an exercise for improving explanations, not a validated hiring score:

• Contract: define legal transitions and a customer-visible violation.
• Oracle: show the exact assertion or history that rejects it.
• Exploration: explain why the generated operations or faults reach the risky boundary.
• Reproduction: preserve enough execution evidence to investigate the failure.
• Limits: name what passed, what remains unknown, and the next useful check.

Finish your answer with a concrete disproof: two successful reservations for the final unit, duplicate stock consumption after a timeout, or a canceled reservation releasing stock twice. Then explain the evidence that would catch it. In your next practice session, follow one request through each testing layer and make every claimed guarantee earn its oracle.