KRust: A Formal Executable Semantics of Rust

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

scope and result

Wang et al. define KRust, an executable operational semantics for a realistic subset of Rust in the K rewriting framework. The paper targets the language mechanisms that make Rust difficult to model: ownership, moves, borrows, lifetimes, mutability, arrays, vectors, structs, control flow, and functions. Its abstract states, “In this paper, we present a formal executable operational semantics of a realistic subset of Rust, called KRust.” (Abstract, p. 1) The semantics is intended to produce an interpreter and formal-analysis tools from one definition.

The authors report validation against 182 programs: 157 supported tests selected from the official Rust run-pass suite and 25 hand-crafted tests written according to the syntax in Table I and covering all primitive constructs (Section IV-A, pp. 6–7). They state that “KRust successfully parsed all of them and the results produced by the interpreter are same as the one produced by the compiled programs using the Rust compiler.” (Section IV-A, p. 7) The denominator is 182 tests, not all Rust programs or all 3,119 run-pass tests.

technique: executable rewrite semantics in K

Inference: when to use it: use a rewrite-based executable semantics when one formal definition should support interpretation, debugging, symbolic execution, model checking, and deductive verification. K represents an executing program as nested cells and defines each atomic statement by a rewrite rule.

Steps from the paper:

1. Define the language syntax in BNF with semantic attributes. KRust covers primitive types and operations, structs, arrays, vectors, control flow, function definitions/calls, and Rust-specific ownership, borrowing, and lifetime features (Sections III-A–III-D, pp. 3–6; Conclusion, p. 8).
2. Define a nested configuration (13 main cells, Figure 1). The k cell stores computations; env maps variables to locations; store maps locations to values; typeEnv stores types; mutType records mutability; ref and refType encode references; borrow records borrow status; moved records moved values; fstack stores function-call frames; and nextLoc allocates fresh locations (Section III-C, p. 4).
3. For each statement, write a K rewrite rule that updates only the relevant cells. The paper explains that X ⇒ L inserts a variable-to-location pair and that A 7→ (B ⇒ C) replaces a cell pair, making state transitions explicit (Section III-D, pp. 5–6).
4. Give the K definition to K, which automatically generates an interpreter and exposes generic analysis tools. The paper says, “The executable semantics yields automatically a formal interpreter and verification tools for Rust programs.” (Abstract, p. 1)
5. Validate the generated interpreter against compiled Rust and then use the same semantics for debugging and verification applications (Section IV, pp. 6–7).

The K framework’s lookup example illustrates the shape: a lookup rule finds X 7→ L in env, then L 7→ V in store, and returns V in k (Section III-A, pp. 3–4). Inference: a Verus-oriented semantic model could similarly expose executable ghost state for ownership or abstract resources, but Verus source itself is checked by Verus and its solver rather than by K rewrite execution.

Verus form: Inference: model executable state with ordinary Rust data and specifications, and model abstract resources with ghost state and proof functions. State transitions should be stated with requires and ensures; loop preservation belongs in loop invariant declarations; intermediate semantic facts can use assert. Inference: a K-style interpreter can validate a reference model, but it cannot replace Verus’s checking of the actual Rust implementation unless a proven refinement relation connects the two.

technique: explicit ownership, move, borrow, and lifetime cells

Inference: when to use it: use separate state components when a language property depends on more than variable values. Rust’s ownership safety requires tracking whether a location is moved, which references exist, whether a borrow is mutable, and whether a lifetime relation permits it.

The paper’s operational encoding proceeds as follows:

1. On immutable or mutable variable declaration, allocate a fresh location in env, initialize store, record the type in typeEnv, record mutability in mutType, and advance nextLoc; the rule shown is for let X : T; with a primitive type (Section III-D.1, p. 5).
2. For a mutable reference X = &mut Y, require that X and Y are mutable and not moved, that Y is not already borrowed, and that the declaration order gives X a lifetime included in Y’s. Update ref from X’s location to Y’s location, mark the reference type mutable in refType, and mark Y as mutably borrowed in borrow (Section III-D.2, p. 6).
3. For an immutable reference X = &Y, the rule sets the reference type of X to immutable (0) in refType and the borrow entry of Y to 0 in borrow, with the same L1 > L2 condition. Dereference follows the ref relation to the target location (Section III-D.2, p. 6). That several immutable references may coexist and that mutation through an immutable reference is an error come from the Section II-D examples (p. 3), not from the rule description.
4. For an ownership move X = Y; between struct instances, require that X and Y have the same type and X is immutable; helper functions F3 and F4 copy the fields from Y to X and update the moved cell (Section III-D.4, p. 6). Inference: the moved update marks Y as moved so it is no longer usable.
5. For function calls, save the caller environment, return type, and remaining computation in fstack, create a fresh local environment, bind parameters, run the body, and restore the caller frame on return (Section III-D.3, p. 6).

The paper’s examples show the intended errors: after let mut q = p, using p.x is rejected because ownership moved, and using q.x after q’s scope is rejected because q’s object was destroyed (Section II-C, p. 2). For borrowing, two immutable references may coexist, but mutation through them and a simultaneous mutable borrow are rejected (Section II-D, p. 3).

Verus form: Inference: preserve Rust’s ownership and borrow checking in executable code, then state functional properties over the owned values and ghost representations. Use requires to state valid ownership preconditions and ensures to relate pre- and post-state values. Inference: Verus does not expose KRust’s env, borrow, or moved cells as a universal runtime API; a Verus proof must use supported Rust/Verus constructs and explicit ghost state where an abstract ownership invariant is needed.

technique: contract verification of functional and resource properties

KRust’s generated verifier handles reachability and Hoare-style claims, including a resource counter for time complexity. The paper’s example is Euclid’s subtraction algorithm:

1. implement gcd(a,b) with positive integer preconditions and recursive subtraction until a == b (Section IV-B, p. 7)
2. add a time configuration cell whose counter increases on each gcd call
3. state requires X > 0, Y > 0
4. state ensures T2 − T1 <= maxInt(X,Y), where T1 and T2 are the counter values before and after the call
5. run the generated verifier; it outputs true for the bound, establishing O(max(a,b)) under the modeled semantics (Section IV-B, p. 7)

The paper states: “The verifier outputs true which proves that T2 - T1 <= maxInt(X,Y) holds, i.e., the time complexity is O(max(a, b)).” (Section IV-B, p. 7). Inference: for Verus, the direct form is a Rust function with requires and ensures, plus a ghost or specification counter and loop invariant for the recursive or iterative bound. The paper’s counter is a semantic instrumentation mechanism; a Verus implementation must connect any cost model to the actual code path and environment.

The semantics also supports automatically derived reachability, model checking, symbolic execution, and theorem proving through K’s language-independent tools (Section III-A, p. 3; Section I, p. 2). Inference: these analyses can find behavior or proof obligations, but only a sound refinement argument and a checked Verus proof establish that the deployed implementation meets its stated contract.

technique: conformance testing and differential validation

Inference: when to use it: use differential testing when an executable semantics claims to model an existing language. Compare the generated interpreter against a trusted compiler or reference implementation on a broad, explicitly counted test set.

The paper’s procedure is:

1. parse all 3,119 official run-pass tests
2. retain 195 tests supported by KRust’s syntax
3. remove 38 tests that “either do not have a main function or call some standard library functions”, leaving 157 official tests
4. add 25 hand-crafted tests covering all primitive constructs in Table I
5. run all 182 tests through KRust and compare outputs with compiled Rust (Section IV-A, pp. 6–7)

All 182 selected tests parsed successfully and produced the same results as compiled programs. The authors explicitly caution that “the semantic coverage of the test suite has not been well-studied” (Section IV-A, p. 7). Inference: passing 182/182 is evidence for these selected cases, not evidence of complete language coverage; the 38 excluded tests and unsupported features are part of the denominator story.

Verus form: Inference: maintain differential tests between reference Rust behavior and verified Rust behavior, and run the Verus verifier on each test’s contract. Record which tests exercise ownership, borrows, lifetimes, loops, and external calls. A passing differential test cannot replace a proof, and a passing proof cannot reveal behavior absent from the test or contract.

technique: executable debugging from semantic states

The same K configuration can drive a debugger. The paper runs krun test.rs --debugger on a loop that decrements a mutable integer and lets a user step through semantic rules and print state. After one iteration it displays env, typeEnv, mutType, and store cells (Section IV-B, p. 7).

evidence, limitations, and trusted boundary

KRust captures the listed subset and its generated interpreter, but it omits structs with reference fields, pattern matching, trait objects, explicit lifetime annotations, complex closures capturing outside variables, concurrency, crates/modules calling external libraries, and unsafe (Section VI, p. 8). The authors say, “KRust does not cover the full features of Rust, as Rust is being actively developed and some of these features are not stable so far.” (Section VI, p. 8) The 182-test result therefore supports the subset and test settings only.

Inference: the trusted parts are the K framework and its generated interpreter/verifier, the compiler used for differential comparison, the modeled language rules, and the stated properties. Inference: for Verus, the trusted boundary additionally includes Verus, its solver, Rust compilation, external-library specifications, and the correctness of the written contracts. The semantics does not prove that a contract expresses product intent.

techniques for the catalog

• executable rewrite semantics: define language statements as K rules over nested state cells and generate an interpreter
• ownership-state modeling: track locations, mutability, moves, references, borrow status, and lifetimes in explicit configuration cells
• generated formal analysis: derive debugging and verification tools from the executable semantics (demonstrated in Section IV-B); the paper also lists state-space exploration, model checking and symbolic execution as available through K but does not demonstrate them
• contract instrumentation: add a resource or time cell and prove a Hoare-style bound with pre- and postconditions
• differential conformance testing: compare the generated interpreter with compiled Rust over counted official and hand-crafted tests
• semantic-state debugging: step rewrite rules and inspect configuration cells to explain program behavior

Last edited: 2026-10-31