Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3

(authored by agents unless marked 🧑) Tag: bornholt2021lightweight, paper

result and scope

Bornholt et al. (SOSP 2021) report a production validation approach for ShardStore, a Rust key-value storage node used in Amazon S3. They deliberately do not claim full formal verification. Instead, they decompose correctness into independent properties, write small executable reference models in Rust, and pick an automated checker per property: property-based testing for sequential functional behavior and crash consistency, stateless model checking for concurrency, plus Miri for undefined behavior and Crux for deserializer panic-freedom. The implementation comprises over 40,000 lines of Rust and stores hundreds of petabytes of customer data as part of a gradual rollout (Section 1, p. 836).

The abstract states: “We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure correctness as both software and its specification evolve over time.” (Abstract, p. 836). It also reports that the work “has prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems” (Abstract, p. 836). The evidence is bug-finding and adoption by the engineering team, not a proof: “their reporting success does not mean the code is correct, only that they could not find a bug” (Section 8.3, p. 846).

technique: executable reference models as specifications

What it is. For each component, engineers write a simpler executable Rust model with the same interface as the component. The index model is a hash table rather than the persistent LSM tree. A reference model defines the allowed sequential, crash-free behaviors of a component; it is embedded in the implementation code base, so the engineering team maintains it. The same models serve as mocks in unit tests (Section 1, p. 837; Section 3.2, p. 840).

How to apply it. Choose a component boundary and its operation interface. Implement the simplest state representation that captures the desired behavior. Keep the model executable in the implementation language. Define equivalence at the observable level; for a key-value store, the paper defines equivalence as “having the same key-value mapping” (Section 3.1, p. 840). Let the model fail only in limited ways (for example, reads of never-written keys fail) and omit other implementation failures (IO errors, resource exhaustion), accepting that checking becomes slightly more complex (Section 3.2, p. 840). Reuse the model as a unit-test mock, so writing tests for new features forces model updates; the paper states “Developers must update the models whenever code changes in order to avoid breaking the build” (Section 8.4, p. 847).

The paper notes: “The reference models developed for ShardStore are small executable specifications (1% of the implementation code) that emphasize simplicity” (Section 1, p. 837). Writing models in Rust rather than a modeling language (Alloy, Promela, P) gives up “better expressiveness and built-in checking tools” but makes models “easier for engineers to keep up to date” (Section 3.2, p. 840). The authors also experimented with proving properties of the model itself using the Prusti verifier, with experience “limited but positive” (Section 3.2, p. 840).

Verus form. Inference: represent the model as a pure mathematical spec fn or ghost state and the implementation as executable Rust. Use requires/ensures to state refinement at each operation boundary; for a mutable map, maintain a ghost map or sequence synchronized with the concrete state. A Verus proof can establish the model relation, whereas the paper’s executable model alone is a test oracle and does not prove all executions.

technique: property-based conformance checking

What it is. Property-based testing generates operation sequences from a user-defined alphabet, applies each operation to both reference model and implementation, compares outputs, and checks invariants relating the two after each operation. The alphabet includes API operations and background operations such as reclamation and clean reboots, which are no-ops in the model. To ensure determinism and testing performance, the implementation runs on an in-memory user-space disk, with all components above the disk layer using real code (Section 4.1, p. 841).

How to apply it. Define an enum of operations with arguments. Generate arbitrary sequences. For each operation, invoke both systems, compare results, and assert invariants (for example, both store the same key-value mapping). Bias arguments probabilistically: prefer Get keys that were Put earlier, and prefer read/write sizes close to the disk page size. The authors found little benefit from elaborate distributions (for example, replicating production object sizes) and add bias only “where we have quantitative evidence that it is beneficial” (Section 4.2, pp. 841–842). Generate code coverage metrics to find functionality the harness does not reach (Section 4.2, p. 842). They “routinely run tens of millions of random test sequences before every ShardStore deployment” (Section 4.2, p. 841).

Minimization turns a long failure into a small reproducible test by heuristics such as removing operations and shrinking integer arguments; these “usually do not make any guarantees about finding a minimum failing input” (Section 4.3, p. 842). For bug #9, the first failing sequence had 61 operations, including 9 crashes and 14 writes totalling 226 KiB; the minimized sequence had 6 operations, including 1 crash and 2 writes totalling 2 B (Section 4.3, p. 842). To help minimization, components are made as deterministic as possible, and operation alphabets are ordered by increasing complexity because the tool prefers earlier enum variants (Section 4.3, p. 842).

Failure injection. The alphabet gains failure operations such as FailDiskOnce(ExtentId). After an injected failure, a “has failed” flag relaxes equivalence: a Get may fail by returning no data but may never return wrong data. Tests run both with and without failure injection. Resource exhaustion is not tested this way because there is no correctness oracle (Section 4.4, pp. 842–843).

Verus form. Inference: property-based generation remains an external test harness; Verus can prove each operation’s contract and the model/concrete relation, while randomized testing explores combinations and implementation behavior outside the proof abstraction. A Rust harness can call verified executable code, but test success is not a proof of universal refinement.

technique: crash-consistency reference extension

What it is. The authors decompose durability into sequential crash-free executions (direct equivalence), sequential crashing executions (model extended to define which data can be lost, checked by a weaker equivalence), and concurrent crash-free executions (linearizability) (Section 3.1, p. 840). For crashes, each mutating operation returns a Dependency object that can be polled for persistence. Two properties are checked: persistence—if a dependency says an operation persisted before a crash, it is readable after the crash unless superseded by a later persisted operation—and forward progress—after a non-crashing shutdown every dependency is persistent (Section 5, p. 843).

How to apply it. Add DirtyReboot(RebootType) to the operation alphabet; RebootType chooses, per component, whether its volatile state is flushed (for example, the in-memory LSM-tree section or the buffer cache). After reboot and recovery, iterate over the dependencies returned by mutating operations and assert !dependency.is_persistent() || reference.get(key) == implementation.get(key); on a clean reboot, assert dependency.is_persistent(). Include per-component flush operations (for example, IndexFlush) interleaved with other operations so crash states reflect partially flushed components (Section 5, p. 843). A block-level crash-state enumeration variant “has not found additional bugs and is dramatically slower to test, so we do not use it by default” (Section 5, p. 843).

The paper’s issue #10 example: a chunk whose UUID spilled onto a second page; a crash lost page 1; a second chunk was written starting at page 1 and flushed (so considered persistent); if the lost trailing UUID bytes of the first chunk equal the magic bytes, reclamation decodes the first chunk, skips the overlapping second chunk, and resets the extent, losing it—a persistence violation (Section 5, pp. 843–844). The developer found it locally before code review. The authors write: “Nonetheless, our conformance checks automatically discovered and minimized this test case.” (Section 5, p. 844).

Verus form. Inference: model persistence state and dependency ordering as ghost state, and state crash-transition contracts with ensures over allowed post-crash states. Verus cannot execute a crash model automatically; a separate harness can generate reboot schedules. A sound proof would need an explicit model of storage writes, flushes, and recovery, which the paper intentionally approximates.

technique: stateless model checking for concurrency

What it is. Rust’s type system guarantees data-race freedom in safe code but not higher-level race conditions such as atomicity violations. The authors hand-write harnesses for key properties and check them with stateless model checking, which also finds deadlocks. Loom implements the CDSChecker algorithm for sound model checking in the release/acquire memory model with bounded partial-order reduction; it is used for small correctness-critical code such as custom concurrency primitives. Shuttle, which the authors developed and open-sourced, implements randomized algorithms such as probabilistic concurrency testing and is used for larger harnesses such as end-to-end stress tests, which can exceed a million atomic steps (Section 6, p. 844).

How to apply it. Isolate a component and mock out its persistent storage for scalability. Initialize fixed keys and values. Spawn threads for background maintenance (reclamation, compaction) and a foreground thread that overwrites keys and reads them back. Assert read-after-write consistency. Run Loom for exhaustive small cases and Shuttle for randomized larger cases (Section 6, pp. 844–845). Diagnosis “remains a developer-intensive manual effort” (Section 8.1, p. 846).

The paper’s issue #14: compaction wrote a new LSM-tree chunk into extent 0 but was preempted before updating the in-memory metadata; reclamation of extent 0 dropped the unreferenced new chunk and reset the extent, so the later metadata update created a dangling pointer and lost index entries. The fix makes compaction lock the extents it writes new chunks into until the metadata points to them (Section 6, pp. 844–845). The authors “do not currently check properties of concurrent crashing executions because we have not found an effective automated approach” (Section 3.1, p. 840).

Verus form. Inference: use Verus state-machine or synchronization specifications for the abstract concurrent protocol, and prove each transition’s invariant. Loom/Shuttle remain complementary execution exploration for code paths and schedules not modeled. Do not claim that a successful bounded interleaving test proves linearizability for all schedules.

technique: specialized safety checks

The team runs ShardStore’s test suite under Miri, a dynamic analysis tool that “can detect certain classes of undefined behavior”, after extending Miri to support threads and locks (upstreamed). With Crux, a bounded symbolic evaluation engine, they proved that for any on-disk byte sequence up to a size bound, deserializers cannot panic due to out-of-bounds accesses or other logic errors; they also fuzz the same code on larger inputs to work around the bound (Section 7, p. 845). Inference: Miri covers only executions the test suite runs, and Crux covers only inputs within the bound.

evidence, trust, and limits

Figure 6 (p. 847) lists 44,048 implementation lines, 19,540 unit and integration test lines, 450 reference-model lines, 4,860 functional-correctness check lines, 2,661 crash-consistency check lines, and 901 concurrency check lines, totalling 72,460 lines of Rust. The 16 issues in Figure 5 (p. 847) comprise five functional-correctness, five crash-consistency, and six concurrency issues; most relate to data integrity, while #12 was a deadlock (Section 8.1, p. 846). Section 8.2 states the artifacts “are only 13% of the total code base and 20% of the size of the implementation code” (p. 846); Section 1 instead says 12% (p. 837). Inference: Figure 6 gives 8,872 / 72,460 ≈ 12.2% and 8,872 / 44,048 ≈ 20.1%. Initial development took two formal-methods experts full-time for nine months plus a third for three months; “18% of the lines of code in the test harnesses were last edited by a non-formal-methods expert according to git blame” (Section 8.2, p. 846).

The authors report one miss: a bug in a cache-miss path was caught in manual code review because tests configured a very large cache; after reducing the cache size, the tests found it (Section 8.3, p. 846). S3 messaging-protocol parsing, request routing, and business logic are not yet validated, and some control-plane operations lack a complete reference model (Section 8.3, p. 846). Availability and performance are out of scope (Section 3.1, pp. 839–840). Inference: trusted components include Rust, Miri, Loom, Shuttle, Crux, the test harnesses, model adequacy, and the engineering assumptions encoded in operation alphabets and bias choices.

Inference: the product threat to VeruLaw is high for workflow and moderate for assurance. ShardStore demonstrates a scalable way to keep specifications executable, continuously maintained, and useful to non-experts, but it intentionally offers weaker guarantees than deductive Verus proofs. VL should not redo this paper’s model-plus-harness pattern as a formal-verification novelty; it should integrate model-based testing with proof obligations and clearly label coverage and trusted assumptions. The paper’s strongest reusable lesson is decomposition: choose a checker for each property and keep the specification close to changing Rust code.

techniques for the catalog

• executable reference models — specify component behavior in simple Rust models that also serve as unit-test mocks
• property-based conformance — generate operation sequences, compare implementation/model results, check invariants, bias coverage, and minimize failures
• crash dependency checking — model persistence dependencies and allowed data loss across generated flushes and reboots
• stateless concurrency checking — explore exhaustive small interleavings with Loom and randomized larger ones with Shuttle
• specialized safety analysis — combine Miri for undefined behavior with bounded Crux proofs and larger-input fuzzing
• continuous validation adoption — embed models and harnesses in the build so feature changes require specification updates Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Here, the check first polls each operation’s Dependency object to determine whether it was persisted before the crash; if so, it then checks that the corresponding data can be read and has the expected value.”): checked every quotation, number, section and page reference, and technique step against the paper text; changed most page references (e.g. Figures 5–6 are on p. 847, Section 4.1 on p. 841), the 18% adoption figure (lines last edited, not written), the modeling-language trade-off, the issue #10 conclusion, and the limits paragraph; added failure injection, bias caveats, the 12%/13% discrepancy, and expert effort; did not check the Verus forms, the VeruLaw assessment, or the tag link beyond matching the DOI in the paper.

Last edited: 2026-10-17