Vérification déductive de programmes Rust

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

scope and contribution

The dissertation (Xavier Denis, Université Paris-Saclay, 2023, written in English despite the French title) presents Creusot, a deductive verifier for Rust, its translation from Rust MIR to Why3 MLCFG, the RustHornBelt semantic account of the translation, iterator specifications, and Sprout, an SMT solver whose verification is partly finished (the proof for the linear-real-arithmetic theory is unfinished, Section 7.2.2, p. 122). It states the central engineering problem directly: “the programs we want to verify are too large and complex to verify.” (Introduction, p. 11, end of the third paragraph). Rust’s ownership discipline is used as a verification resource: “If a verifier can trust and leverage the borrow checker, it could avoid the need to prove memory safety entirely.” (Section 1.2, p. 13). Per Section 1.3 (p. 13) “Creusot can verify safe Rust code using the majority of available language features”; the thesis says of the MIR-to-MLCFG translation: “This translation is the core of Creusot and is the most significant contribution of this thesis.” (Section 1.3, p. 14). Specifications for libraries implemented with unsafe code are justified by RustHornBelt (Section 1.3, p. 14), not verified by Creusot itself: “Creusot is a verifier for safe Rust” (Section 3.8.2, p. 47).

technique 1: write executable Rust contracts and loop invariants

what it is and when to use it. Creusot separates executable Rust from Pearlite specifications. Use requires for a call precondition, ensures for a postcondition, variant for termination (attachable to loops and functions), predicates for reusable mathematical facts, and ghost values for pre-state snapshots. The thesis defines Pearlite as “a non-executable, ownership-free specification language for Rust” (Section 3.2, p. 32). A mutable borrow has a current value *x and a final prophetic value ^x; the example #[ensures(^x == *x)] fn drop_mut_bor(x: &mut T) { } is described as “stating that the final value of x equals its initial value” (Section 3.2, p. 32).

how to apply it. Start by running the unannotated function: Creusot first checks panic safety such as arithmetic overflow and slice bounds (Section 3.1, pp. 31–32). Add a contract describing the desired result. For gnome sort, define a mathematical sequence predicate sorted_range(s, l, u) with a quantified index relation, define sorted(s) as the range from zero to s.len(), and state that the final slice (^v)@ is sorted and is a permutation of the initial v@ (Section 3.3, pp. 35–36). Save the initial value as let old_v = ghost! { v };. Add a loop invariant for the sorted prefix and a second invariant relating the current sequence to old_v; the thesis’s code uses #[invariant(sorted_range(v, 0, i@))] and #[invariant(v@.permutation_of(old_v@))] (Section 3.3, p. 36). Prove initialization at the loop entry (trivial at i = 0 because the interval is empty) and preservation for both the already ordered and swap cases (Section 3.3, pp. 36–37). Add a variant when the loop needs an explicit termination measure.

evidence and limits. The thesis reports that the unannotated gnome-sort body is proved panic-safe from Rust’s type guarantees and the loop guard, while the functional proof requires the two invariants (Section 3.1, pp. 31–32; Section 3.3, pp. 36–37). Table 3.1 (p. 45) lists Gnome Sort at 11 lines of code, 17 specification lines, 31 verification conditions and 2.06 s (macOS laptop, Alt-Ergo, Z3, CVC4; Section 3.8, p. 44). Ghost code must erase without changing behavior: “Ghost code and ghost values must satisfy an erasure property: the program’s behavior with the ghost code removed must be identical to the program with ghost code.” (Section 3.3, p. 37). A contract proves the written predicate, not that it expresses the intended requirement; the thesis’s trusted clause “Indicates that a contract should be assumed, and that Creusot should not generate any proof obligations.” (Section 3.2, p. 34).

Verus form. Inference: express the same executable contract with Verus requires and ensures, use a while loop with invariant(...) clauses and a decreases clause, and store the initial sequence in a ghost variable. Inference: Creusot’s @ model operator and ^ prophecy operator do not carry over as Verus syntax; use the Verus model type and explicit pre-state ghost value documented for the target data structure. Inference: preserve the two proof obligations (sortedness and permutation) rather than copying Pearlite syntax.

technique 2: compile MIR through a prophetic borrow encoding

what it is and when to use it. Creusot takes MIR, not source Rust, because MIR is a control-flow graph where borrow checking has already been performed. The thesis says, “Despite being a Rust verifier, Creusot does not start its work from the source Rust code. Instead, it uses the Mid-Level Intermediate Representation (MIR) as the source language for our translation.” (Section 4.1, p. 49). The pipeline is Rust → MIR (rustc) → MLCFG (Creusot) → WhyML (Why3, which then calls the backend solvers) (Figure 4.4 and Section 4.3, p. 53).

how to apply it. First represent each MIR function as locals and basic blocks containing assignments and a terminator; the simplified syntax includes places, move/copy, borrows, calls, switches, assertions, and returns (Figure 4.1, p. 50). Then run a dataflow analysis to locate the resolution point of every mutable borrow; resolution points are where Is-Resolved(G) = ¬Live(G) ∧ Initialized(G) changes from false to true (Section 4.3.2, p. 57). The translator’s two phases are explicit: “the first is a dataflow analysis used to identify the resolution points of every borrow, and the second is a syntax-directed translation of MIR to MLCFG, which uses the dataflow analysis to insert resolutions at the appropriate positions.” (Section 4.3, p. 53). Interpret a mutable borrow &mut T as a pair (T,T): the first component is current and the second is a prophecy for the final value; boxes and shared borrows use the underlying type (Section 4.3.1, pp. 53–54). At borrow creation, use any to choose a fresh prophecy (rule R-Ref-Mut, Figure 4.6, p. 55); at the resolution point insert assume { p.0 = p.1 } (Section 4.3.2, p. 57). The thesis states: “any is used to create a prophecy, and assume is used to resolve it.” (Section 4.3, p. 53). Translate places, operands, rvalues, statements and terminators with the five MIR-to-MLCFG rule families (Section 4.3.2, p. 54, Figures 4.5–4.7), then emit MLCFG contracts, assert, assume, and cycle invariant statements for Why3 (Section 4.2, pp. 51–52). The thesis explains why lifetimes alone do not suffice: for if b { z = x } else { z = y } the lifetime ends after the if but which borrow to resolve depends on execution (Section 4.3.2, p. 58). Worked example: clear_max (Figure 4.8, p. 59).

why it works. Rust’s unique mutable borrow means only the borrower can mutate the resource, so when it ends the lender must observe the borrow’s final value (Section 4.3, p. 53). “The interpretation of pointers is how Creusot avoids the need for an explicit heap model.” (Section 4.3.1, p. 53). Its key assumption is that the Rust compiler’s liveness and initialization analyses and MIR semantics are right; the thesis notes that official MIR semantics still had open questions (Section 4.1, p. 49, footnote 1) and that “Creusot relies on the soundness of Rust’s type system and its implementation” (Section 4.6, p. 68).

Verus form. The thesis says of Verus: “Verus does not fully account for mutable borrows; instead, specific support is provided for mutable borrows in the argument position and functions like index_mut cannot be handled in the Verus approach.” (Section 4.6, p. 67; a 2023 statement, not checked against current Verus). Inference: a Verus user normally writes source Rust and lets Verus lower it; the implementable proof shape is an explicit ghost model of the borrowed resource plus contracts connecting the borrow’s pre-state and post-state. Inference: do not write any or assume as executable proof shortcuts; in Verus, use ghost state, assert, assert forall, and proof functions to establish the relation, and keep any trusted external-body boundary explicit. Inference: the unique-borrow premise is supplied by Rust/Verus typing, but the final-value relation still needs a Verus contract or lemma when a borrow is returned or stored.

technique 3: give traits, closures, and iterators compositional specifications

what it is and when to use it. Traits carry contracts and laws. A trait implementation must refine the trait’s contract: implementations “weaken preconditions and strengthen the postconditions”, with refinement obligations generated per implementation (Section 4.3.5, p. 62; also Section 3.4, p. 37). Use this when generic code relies on algebraic behavior such as transitivity of Ord. Closures are specified with #[requires] and #[ensures] attributes, with old for pre-call captures; client code uses the precondition and postcondition_* predicates and the unnest predicate added to the FnOnce/FnMut/Fn traits (Section 3.6, pp. 39–43). Iterators are specified as state machines through the predicates produces and completed (Section 6.1.1, pp. 99–100).

how to apply it. Put an abstract operation and its law in the trait, for example a transitivity lemma whose requires says a.cmp(b) == o && b.cmp(c) == o and whose ensures says a.cmp(c) == o (Section 3.4, p. 37). A plain lemma function is only included in a verified function’s context if it is called there, to avoid increasing context size; a #[law] is instead “auto-loaded by Creusot when a trait is used”, so that facts like transitivity are always available in generic code (Section 3.4, p. 37). For iterators, add produces_refl and produces_trans laws, and specify next with None => self.completed() and Some(v) => (*self).produces(Seq::singleton(v), ^self) (Figure 6.1, p. 100). Every for loop then gets the structural invariant init_iter.produces(produced, iter) through ghost variables init_iter and produced (Section 6.1.2, pp. 100–101). For IterMut, define tr, which turns a mutable reference to a slice into a sequence of mutable references, and set it produces v into it' as tr(it.inner) = v · tr(it'.inner) (Section 6.2.2, p. 102). Combinators Take, Skip, Fuse and the higher-order Map reuse the same predicates (Sections 6.2.3–6.3, pp. 103–106). The thesis lists in its contributions that the scheme “can be trivially instantiated for basic iterators”, gives full functional specification to mutating iterators, and “is composable” (Chapter 6, pp. 98–99).

evidence and limits. Figure 6.3 (Section 6.4, p. 107) gives lines of code, specification lines and time per iterator (for example Range: 13 lines, 39 spec lines, 0.40 s; Map: 23, 46, 0.89 s) and marks Range, IterMut and Take as fully automatic but Map, MapExt, Skip and Fuse as needing manual Why3 tactics. So the dissertation does not claim that all iterator specifications prove automatically. Map needs a closure-history-free precondition or the MapExt ghost-history variant (Section 6.3, pp. 104–106). Closure contracts must state the precondition needed at each call; the thesis states for Map that “the postcondition at iteration n must be able to establish the precondition for iteration n + 1” (Section 6.3, p. 104). Inference: Verus analogues use trait requires/ensures, spec fn/proof fn laws, and loop invariants over a mathematical sequence; iterator state that contains borrows must be represented with a Verus-supported model rather than assuming Creusot’s ^ operator.

technique 4: prove the verifier’s Rust semantics with RustHornBelt

what it is and when to use it. RustHornBelt supplies a semantic soundness argument for a core of Creusot’s approach, including clients of unsafe libraries. The thesis says this work “extends the prior RustBelt project to reason about the correctness of Rust programs when equipped with with specifications” (Section 1.3, p. 14; “with with” is as printed). Section 5.5 (p. 94) claims “RustHornBelt (this chapter) provides strong evidence for the soundness of the approach used in Creusot (Chapter 4)” while naming a remaining formalization gap between the two (Section 5.5, pp. 94–95). Its λRust type-spec system (Section 5.1.2, pp. 71–73) is proved sound in Iris with parametric prophecies, which keep a prophecy abstract by working in a “clairvoyant monad” over all possible futures (Section 5.2.1, pp. 82–83).

how to apply it. Model a mutable borrow as a pair of current and final values, where the final value is a prophecy variable; its ownership predicate carries a value observer VO and a prophecy controller PC that make the current state referable inside and outside the borrow (Section 5.2.2, pp. 85–86). Creating a borrow creates a fresh prophecy and its VO/PC (Section 5.2.4, p. 88); resolving it when the borrow is dropped uses mut-resolve and consumes the value observer so resolution happens once (Section 5.2.4, p. 89). For dependent resolutions, a prophecy equalizer â :≈ b̂ delays full resolution until the dependency tokens are available (Section 5.2.1, pp. 83–84; used for frozen values at the end of a lifetime, p. 86). Prove each typing rule semantically (Section 5.2.4, pp. 87–89). Then give specifications for APIs with unsafe code, for example Vec::index_mut, whose spec 0 ≤ i < |v.1| ∧ ∀a'. v.2 = v.1{i := a'} → Ψ [(v.1[i], a')] partially resolves the old vector’s prophecy in terms of the output borrow’s prophecy a’ (Section 5.3, p. 90); the worked proof sketch in the thesis is for iter_mut (Section 5.3.1, p. 92). Inference: this lets a client of an unsafe library use the proved specification instead of the implementation.

evidence and limits. Section 5.4 (pp. 92–94) reports a Coq mechanization of about 19kLOC (extending RustBelt; about 7kLOC added, two implementors, about six months) covering Vec, SmallVec, slices and iterators, Cell, Mutex, JoinHandle and MaybeUninit (Figure 5.8, p. 93). It states a concrete limitation: for Cell, invariants are restricted to non-prophesied values: “we cannot choose an invariant that depends on the prophecy of a mutable borrow. To this day, we do not know if extending our approach to allow such invariants is possible.” (Section 5.3, pp. 91–92). The conclusions also say the interior mutability model “in practice, this has been insufficient and cumbersome to use” (Section 8.1, p. 130). Inference: this is a foundation for trusting Verus proof APIs, not a substitute for proving each Verus library contract; Verus’s own trusted compiler, solver, erasure, and external-code boundaries remain outside the dissertation.

technique 5: verify a non-trivial algorithm by refinement (Sprout CDSAT)

what it is and when to use it. Chapter 7 mechanizes a theory of conflict-driven satisfaction (CDSAT) in Pearlite and refines it to Sprout, a Rust SMT solver for the Bool and linear-real-arithmetic (LRA) theories. The abstract CDSAT transition system has eight rules (Section 7.1.3, pp. 113–114, Figure 7.1); only soundness is mechanized: “In this work, we only consider soundness; the remaining properties rely on complex arguments about theory modules that we have not mechanized.” (Section 7.1.4, p. 116). The concrete deterministic implementation keeps a trail and saturation state, and resolves conflicts with four rules (Section 7.2.2, pp. 117–121).

how to apply it. Define first-order theories and modules as mathematical structures, formalize the abstract CDSAT transition rules as Pearlite logic functions with preconditions, and prove soundness by instrumenting each transition with #[ensures(inp.entails(result))] (Section 7.1.4, p. 116). Define a concrete trail (a vector of vectors of assignments) with a ghost abstract trail and an abs-conc correspondence predicate, simulated as a type invariant through pre- and postconditions (Section 7.2.1, pp. 116–117). Implement the deterministic loop (Algorithm 1, pp. 117–118) and conflict resolution (Algorithm 2, p. 120), and give theory solvers a trait Theory::extend whose contract requires returned decisions to be acceptable and returned conflicts to be unsatisfiable (Section 7.2.2, p. 119). The Bool theory is a verified interpreter (Section 7.2.2, p. 121). Test the executable solver against generated formulas (Section 7.3.1, pp. 123–124). The thesis reports, “We presented the implementation and verification of an SMT solver based on a modern SMT algorithm” (Conclusions, p. 129).

evidence and limits. Figure 7.3 (p. 124) reports 1414 lines of code, 1701 specification lines and 68.5 s total verification time, with no time given for the LRA component; the text says “Excluding the unverified LRA module, we obtained a proof overhead of roughly 1.2:1” (Section 7.3, p. 123). The LRA theory “is implemented and has been informally demonstrated both sound and complete, the proof is unfinished” (Section 7.2.2, p. 122), and the testing prose says “the LRA theory is incomplete” (Section 7.3.1, p. 124); Figure 7.4 nonetheless shows 50 solved of each of three benchmark kinds with no failures or timeouts, with problems of up to 50 constraints and a 1 s timeout. The experience report (Section 7.3.2, pp. 124–126) estimates six person-months, and lists interface issues (Why3 IDE, transformations on generated symbols) and implementation issues (no opacity or triggers yet, quantifier matching loops). Inference: for Verus, use an abstract state-machine/specification model, executable Rust state, requires/ensures, loop invariants, and proof lemmas connecting every concrete transition to an abstract transition; solver soundness does not prove that a product’s specifications are appropriate.

what is proved, measured, and trusted

The thesis proves contracts for selected Rust programs (Table 3.1, p. 45), gives a mechanized semantic account of a core of the translation (Chapter 5), verifies iterator case studies (Chapter 6, Figures 6.3 and 6.4), and verifies parts of the Sprout solver (Chapter 7), without the LRA proof. It lists unsupported features in Section 3.8.2 (pp. 46–47): Drop, mutually recursive functions, trait objects that carry specifications, async, and unsafe code (“Creusot is a verifier for safe Rust”). Pearlite functions are total and the == symbol has a different meaning than in Rust (Section 4.4.3, p. 65). Inference: the use of trusted specifications and extern_spec! models for standard-library functions (Section 3.7, p. 43) enlarges the trusted base, because those contracts are assumed rather than proved; the thesis states that #[trusted] “indicates that the implementation of a trait may violate logical soundness” (Section 4.3.2, p. 60). The dissertation’s motivating cost comparison is that seL4 “estimated the cost of verification at 11 person-years compared to approximately 2.2 person-years for the writing of the kernel itself”, in roughly 200,000 lines of proofs for 8,700 lines of C (Section 1.1, p. 12); those are cited historical figures, not an experiment performed by this thesis.

Inference: for VeruLaw, the highest product threat is specification and model error, followed by unsupported Rust features and trusted library boundaries. The reusable engineering pattern is to make ownership invariants do work, keep contracts short, put loop facts beside loops, and isolate unsafe or external behavior behind proved specifications. What VL should not redo is the general prophecy encoding, MIR lowering, and iterator/SMT refinement ideas already developed here; it should measure whether its own generated contracts match product requirements and whether dependency upgrades invalidate trusted models.

techniques for the catalog

• pearlite contracts and loop invariants: specify executable Rust with preconditions, postconditions, termination measures, mathematical predicates, and ghost snapshots
• MIR-to-MLCFG prophetic translation: lower borrow-checked MIR through dataflow-located prophecy creation and resolution into Why3 verification conditions
• compositional trait and iterator specifications: attach laws and sequence/borrow relations to generic traits, closures, and iterator combinators
• RustHornBelt semantic soundness: model current/final borrows with parametric prophecies and prove type-spec rules and unsafe API contracts
• refinement-verified SMT solver: mechanize the soundness of abstract CDSAT, refine it to executable Sprout Rust (LRA proof unfinished), and test the resulting implementation Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Because resolve consumes the borrow being resolved, it cannot be placed too early: if the borrow was needed later in the program this would lead to a typing error.”): read the whole extracted text (lines 1 to 6769, including the bibliography) and compared every quotation, page and section number, figure and number, and technique step in the study against it; changed the link to the HAL page printed in the paper (the earlier DOI is not in the paper text), corrected the RustHornBelt quote (the paper prints “with with”), the section-5 page references (5.2.1 equalizer pp. 83-84, 5.3 pp. 89-92, 5.4 pp. 92-94, the Cell prophecy limitation is in 5.3 not 5.2.4), Figure 6.3 to p. 107, the Chapter 6 contribution pages to 98-99, the claim that the law is invoked only where needed (the paper says laws are auto-loaded and plain lemmas are included only when called), the claim that completeness and termination of CDSAT are proved (only soundness is mechanized, and the LRA proof is unfinished), the seL4 sentence, and added sourced facts (Table 3.1, Figure 7.3, Section 3.8.2, Verus remark in Section 4.6) and “Inference:” marks; did not check the figure artwork or the equation typesetting beyond the extracted text, the claims about current Verus, or any cited paper outside this thesis.

Last edited: 2026-10-17