One common way to check the alignment between the program and its spec is to turn them together into a collection of mathematical propositions, called verification conditions, or VCs. Each proposition captures something that must hold at a particular point in the program: an addition must not overflow, a function call must satisfy its precondition, or a returned value must satisfy the promised postcondition. If we can prove all these propositions, and the translation produced the right propositions, we have established that the program satisfies its specification.

Verifiers such as Dafny, Verus, and F* use SMT solvers to discharge many of these obligations automatically. SMT stands for *satisfiability modulo theories*: a solver searches for an assignment of values that makes a formula true, using built-in reasoning about domains such as integers, arrays, and bit vectors. To prove a VC proposition, a verifier asks whether its negation is satisfiable. If the answer is no, the VC holds. Z3 and cvc5 are two widely used solvers; both Dafny and Verus normally use Z3.

This style of verification is commonly called auto-active. The programmer provides specifications and proof guidance in the source of the program, including assertions, auxiliary lemmas, and loop invariants. The verifier then attempts the proofs automatically. The division of labour is quite compelling: humans state the intended properties, while the solver takes care of much of the logical bookkeeping.1

There is a separate question about the verifier itself: why should proving its VCs establish anything about the original program? A foundational verifier answers this question with a machine-checked soundness proof, connecting the generated obligations to a formal semantics of the program. For instance, Velvet, which we discussed earlier on this blog, derives its verification machinery from a semantics embedded in the Lean theorem prover. A conventional, non-foundational verifier leaves this connection in its trusted implementation (which might have bugs). It can be carefully designed and extensively tested, but a bug in the translation may still produce an incorrect verification result.

Building a foundational verifier for a realistic language is a daunting task. Before proving anything about verification conditions, we need a mathematical account of what programs in that language mean, including their memory operations and exceptional behaviours. Rust makes this especially interesting with its ownership discipline, lifetimes, and unsafe interfaces. Existing foundational Rust verifiers, such as RefinedRust, cover restricted fragments of the language. Extending these foundations to the breadth of Rust used in practice remains a substantial research problem.

Our experiment dubbed Vermilion (“Verified Rust Meets Lean”) starts with a more modest question: how much can we gain by keeping an existing Rust verifier’s translation and changing the means by which its verification conditions are proved?

When Automated Proofs Need Help

SMT solvers are amazing at the kinds of reasoning that arise repeatedly in program verification. Given suitable bounds, they can prove that an array access is valid, establish a simple arithmetic fact, and combine facts from several branches. This automation is a large part of what makes Verus pleasant to use.

Unfortunately, it is also incomplete. A true statement may require induction, a carefully chosen existential witness, or a mathematical lemma that the solver has never been told about. Even a statement within the solver’s usual reach can fail because the relevant quantified fact was not instantiated at the right argument. Verus exposes some control over this process through triggers. Consider a specification fragment saying that every element of a sequence is bounded:

forall|i: int| 0 <= i < s.len() ==> #[trigger] s.index(i) <= bound

The annotation tells the solver to use occurrences of s.index(...) as candidates for instantiating i. If the proof context contains s.index(3), this gives the solver a reason to consider the quantified statement at i = 3. Choosing triggers well can make a proof succeed; choosing them poorly can leave useful facts unused or cause an explosion of instantiations. The Verus guide explains the rules. The mathematical meaning of the assertion is unchanged. Programming with triggers is manageable when the missing step is obvious. It becomes frustrating when we already know a proof but must work out how to communicate it through the solver’s instantiation strategy. Verus provides proof functions and assertion blocks for doing so, yet the final step still goes through its automated proving machinery.

A verifier embedded in Lean would have another route available. We can inspect a goal, introduce a witness, perform induction, or apply a library theorem directly. We used this combination of automatic and interactive reasoning in the Velvet post. The recent paper on building Veil in Lean discusses the broader design: making verification conditions ordinary Lean goals gives the verifier access to the proof assistant’s existing proof mode, UI, and toolchain.

The same observation applies to mathematical libraries. An SMT-based verifier needs a library of definitions and lemmas expressed in its own specification language. Verus already has a substantial one, called vstd, so users certainly do not start from nothing. Still, if an algorithm needs matrix algebra, somebody must supply the relevant definitions and laws in that ecosystem. A theorem in a Lean library cannot simply be invoked by a Verus proof.

Lean and Rocq have extensive mathematical libraries built over years of formalisation. Lean’s Mathlib includes linear algebra, number theory, and much more. If our verification conditions use its mathematical objects, we can reuse theorems about them. This suggests the experiment: combine Verus’s ability to handle realistic Rust with Lean’s proof mode and mathematical vocabulary.

Connecting Verus to Lean

To see where a Lean backend belongs, let us look briefly at Verus’s translation pipeline. Verus starts with Rust extended by specification and proof constructs, usually written inside a verus! macro. Its frontend uses the Rust compiler infrastructure and performs the additional checks that separate executable code, specifications, and proofs. The frontend produces VIR, Verus’s intermediate representation. Subsequent passes simplify VIR into SST, a representation that separates statements from expressions and makes the verification-relevant operations explicit. The usual backend translates SST into AIR, a solver-oriented representation, and eventually sends SMT queries to Z3.

Vermilion branches off at SST, before the SMT-specific encoding:

            Rust + Verus specifications
                         |
               Verus frontend and VIR
                         |
                Verus simplification
                         |
                        SST
                       /   \
                      /     \
             Verus backend   Vermilion adapter
                    |                |
                   AIR        Small textual IR
                    |                |
                SMT queries    Lean VC generator
                    |                |
                    Z3         Lean theorems
                                     |
                             Automation or proof scripts
                                     |
                                Lean kernel

*Both routes reuse Verus’s frontend and SST construction. Vermilion’s verification runs use the Lean route; the Z3 route is used separately for comparisons.*

SST is a convenient place to make this change because much of the difficult work has already happened. Names and types have been resolved, complex source expressions have been decomposed, and checks for operations such as bounded integer addition have been inserted. Function contracts and loop invariants are available explicitly. So we can focus on turning this representation into mathematical obligations.

For example, suppose the source computes let y = x + 1 on u32 values and then asserts that y > 0. An abbreviated, readable version of the SST looks like this:

Assert 0 (HasType u32 (x + 1))
Assume   (HasType u32 (x + 1))
Assign y (Clip u32 (x + 1))
Assert 1 (y > 0)
Assume   (y > 0)
Return y

This is pseudocode for the SST nodes, with temporary names and source locations removed. The full representation is available in the Vermilion repository. HasType u32 expresses the range check that prevents overflow. Clip converts the mathematical result back to the machine integer range. Once the range check is proved, clipping preserves the result. The Assume following an Assert makes an established fact available to later checks; the assertion itself must still be proved.

VC generation then follows familiar logical rules. An assignment substitutes the assigned expression for the variable’s subsequent uses. An assertion becomes a goal under the facts available at that point. A conditional adds its condition to one branch and its negation to the other. A function call requires proving the callee’s precondition, after which the callee’s postcondition describes the result. This is modular reasoning: callers can use a contract without expanding the callee’s implementation.

These rules can be described using *weakest precondition* calculus: the conditions that must hold before a command for a desired property to hold afterwards. Weakest-precondition reasoning works backwards from the desired result. Vermilion’s implementation instead traverses the statements forwards, accumulating hypotheses and emitting obligations at each check. These are ordinary logical transformations; the resulting propositions do not require SMT-LIB as their output language.

The implementation keeps the Rust and Lean sides separate. A Rust adapter lowers SST to a small textual IR; Lean parses that IR and constructs the theorem statements. It also retains source locations, so a failed theorem can be reported at the corresponding Rust expression. The Vermilion design document describes these stages in more detail.

From a Rust Function to Lean Goals

Let us follow a simple example from the Vermilion test suite:

fn increment(x: u32) -> (y: u32)
    requires x < 100,
    ensures y == x + 1,
{
    let y = x + 1;
    assert(y > 0);
    y
}

Here, requires states the precondition, and ensures states the postcondition. The return value is named y so that the specification can refer to it. As in the rest of the Rust snippets below, the surrounding imports and verus! wrapper are omitted.

Vermilion represents a u32 value as a Lean integer together with an explicit range hypothesis. The predicate Vermilion.inUnsignedRange 32 x means $0 \leq x < 2^{32}$. This representation lets arithmetic tactics reason about ordinary integers while keeping the machine bounds visible.

The first generated obligation in Lean is the inserted overflow check:

theorem assert_0
    (x : Int)
    (requires_0 : Vermilion.inUnsignedRange 32 x)
    (requires_1 : x < 100) :
    Vermilion.inUnsignedRange 32 (x + 1) := by
  vrml

The theorem says exactly what we expect: adding one to a nonnegative integer smaller than 100 produces a value that fits in 32 bits. vrml is Vermilion’s default proof tactic; we will return to it shortly.

The next obligation comes from our explicit assertion:

theorem assert_1
    (x : Int)
    (requires_0 : Vermilion.inUnsignedRange 32 x)
    (requires_1 : x < 100)
    (assert_0 : Vermilion.inUnsignedRange 32 (x + 1)) :
    ((x + 1) % 4294967296) > 0 := by
  vrml

Notice two details. First, the earlier overflow check is now a hypothesis. Second, the remainder operation is still present: $4294967296 = 2^{32}$, and unsigned clipping is represented by reduction modulo this number. The range hypothesis makes the remainder equal to x + 1, so the assertion follows. Preserving this operation also matters for programs that use wrapping arithmetic explicitly.

Finally, the postcondition asks us to establish ((x + 1) % 4294967296) = x + 1 under the accumulated hypotheses. All three obligations are proved automatically. The complete generated statements and their proofs are available in the respective Lean file.

Verification Conditions for Loops

Now consider a function that counts from zero up to its input:

#[verifier::exec_allows_no_decreases_clause]
fn count_to(n: u32) -> (c: u32)
    requires n < 1000,
    ensures n == c,
{
    let mut c: u32 = 0;
    while c < n
        invariant c <= n,
    {
        c = c + 1;
    }
    c
}

The loop invariant says that the counter never exceeds n. To use it, the verifier must first prove it holds when entering the loop and then prove that one iteration preserves it. This is an induction argument: the initial state supplies the base case, and the loop body supplies the induction step. At loop exit, the invariant and the negated loop condition together imply the postcondition.

This example produces four obligations. For brevity, let us retain only the range hypotheses needed for each check and simplify the checked clipping operation. Their mathematical content becomes:

Entry:         0 ≤ n
Overflow:      0 ≤ c, c < n, n < 2^32  ⊢  0 ≤ c + 1 < 2^32
Preservation:  c ≤ n, c < n            ⊢  c + 1 ≤ n
Exit:          c ≤ n, ¬(c < n)         ⊢  n = c

The symbol ⊢ separates the assumptions from the goal. The preservation check considers an arbitrary iteration, so it cannot assume that c is still zero. The counter is constrained by its machine range, the invariant, and the loop condition. This is what makes the finite collection of obligations sufficient to cover arbitrarily many loop iterations.

The actual exit theorem is still quite readable:

theorem ensures_1
    (n c : Int)
    (requires_0 : Vermilion.inUnsignedRange 32 n)
    (requires_1 : n < 1000)
    (loop_0_exit_0 : Vermilion.inUnsignedRange 32 c)
    (loop_0_exit_1 : c ≤ n)
    (loop_0_exit_2 : ¬(c < n)) :
    n = c := by
  vrml

The attribute above the Rust function allows us to drop the need to prove termination. This example proves partial correctness: if the function returns, its result satisfies the postcondition. The loop does terminate, but proving termination is a separate obligation. A decreases annotation supplies a measure for that purpose; it is supported by Vermilion, and other examples in the repository exercise those checks.

Conceptually, we have made a fairly small change: the obligations that would have gone to an SMT solver are now expressed as Lean theorems, ready to be proved in Lean. The engineering includes many details about types and contracts, but the overall idea is simple.

It is important to note that this translation is not yet foundational: Vermilion does not prove that its VCs correctly describe Rust’s semantics, SST’s semantics, or even the semantics of its own textual IR. The translation and VC generator remain trusted. Lean checks proofs of the statements we emit; it cannot tell us that we emitted the right statements. The Vermilion trust document records these boundaries, including the responsibility of the surrounding tooling to check every obligation and report failures correctly.

A foundational generator for the IR is a plausible next step. We could give the IR a semantics in Lean and prove that its verification conditions imply the desired property of executions, following the approach developed in Loom and later integrated into Lean’s vcgen, which generates verification conditions for programs with a weakest-precondition semantics, including monadic computations. Proving our generator sound would remove one part of the trusted translation. Connecting the result back through SST to Rust would remain a further theorem to prove.

Taking Over with Interactive Proofs When Automation Stops

We can now use the part of Lean that motivated the experiment: its interactive proof mode.

Vermilion first tries to prove each obligation automatically. Its vrml tactic combines Lean tactics such as grind, omega, and simp with specialised procedures, including nonlinear arithmetic reasoning. It also has an SMT fallback that reconstructs a Lean proof. In each case, proof search produces a term for the kernel to check. A failed attempt leaves an open obligation that we can prove ourselves.

Here is a deliberately small example from the Vermilion repository:

proof fn witness_shift(y: int)
    requires
        exists|x: int| #[trigger] (x + x) == y,
    ensures
        exists|x: int| #[trigger] (x + x) == y + 2,
{
}

This is a proof function: it expresses a lemma and is erased from the executable program. The lemma says that if y is twice an integer, then y + 2 is also twice an integer. The source body is empty because we will provide the proof on the Lean side.

The mathematical argument behind it is trivial: take the witness x from the precondition and choose x + 1 for the postcondition. The remaining equality is linear arithmetic. Yet the solver still has to discover that witness through its quantified encoding; the trigger does not instruct it to construct x + 1. The repository uses this example to demonstrate an interactive proof beyond the default automation. It is perfectly possible to supply the missing guidance in Verus too; we are comparing ways of expressing the proof, rather than claiming an impossibility result about SMT.

On the Lean side, the whole proof is two lines:

theorem ensures_0
    (y : Int)
    (requires_0 : ∃ x : Int, x + x = y) :
    (∃ x : Int, x + x = y + 2) := by
  obtain ⟨x, hx⟩ := requires_0
  exact ⟨x + 1, by omega⟩

The first line extracts the witness and its defining equality. The second supplies the new witness and asks omega to check the arithmetic. In the Lean InfoView, we can inspect the context after each step: the proof state shows x, the hypothesis hx : x + x = y, and the remaining goal.

This little proof illustrates the workflow for much larger obligations as well. We can introduce an intermediate lemma, use induction, or search Mathlib for an applicable theorem. We can also ask a favourite coding agent to complete the proof in the same file, using Lean’s feedback. The agent’s output goes through the same proof checking as a handwritten script.

Jumping from Rust to the Proof

Vermilion’s VS Code extension connects the two views of a program. Placing the cursor on a Rust assertion, postcondition, or loop invariant and pressing ⌘⇧J on macOS, or Ctrl+Shift+J elsewhere, opens the corresponding Lean obligation. If one annotation generates several VCs, such as an invariant’s entry and preservation checks, a picker lets us choose which one to inspect. The shortcut also works in reverse, returning from a Lean obligation to its Rust source.

*The demo shows Rust verification alongside the generated Lean obligations and the Lean InfoView.*

This navigation feature is useful even when automation succeeds. We can look at exactly what the VC generator produced: which hypotheses are available, how the machine bounds were represented, and what the postcondition became after substitution. When a proof fails, the same view helps distinguish a missing invariant from a missing mathematical argument. That is a much more concrete starting point than an unexplained failure at a source line.

The Lean proofs can be edited alongside the Rust source. When we check the program again, Vermilion keeps proofs of obligations that have not changed. If an obligation changes, its proof needs to be checked against the new statement. This lets source programs and Lean proofs evolve together while preserving the user’s work. Vermilion comes with a tutorial that walks through this process, including deliberately breaking a postcondition and seeing Lean’s failure reported back at the Rust location.

Doing the Mathematics in Lean

The second benefit appears when we choose the mathematical objects used by the embedding. Vermilion represents a Verus Seq<T> as a Lean List, and a Verus Multiset<T> as Mathlib’s Multiset. Consequently, many facts about the translated specifications are already library theorems.

For a small executable example, consider this helper used in merge sort:

fn extend_from_idx(r: &mut Vec<u64>, v: &Vec<u64>, start: usize)
    requires
        start < v.len(),
    ensures
        final(r)@ == old(r)@ + v@.subrange(start as int, v.len() as int),
{
    for i in start..v.len()
        invariant
            r@ == old(r)@ + v@.subrange(start as int, i as int),
    {
        r.push(v[i]);
    }
}

The helper appends a suffix of v to r. The notation v@ denotes the vector’s mathematical sequence of elements; old(r) and final(r) refer to the values before and after the mutable borrow. The postcondition describes exactly which suffix was appended, and the invariant describes the prefix of that work completed so far.

A caller implementing a sorting algorithm often needs a further consequence: appending these elements preserves their multiplicities. A multiset forgets the order of a sequence while remembering how often each element occurs. We therefore want the identity

[\operatorname{multiset}(s_1 \mathbin{+!+} s_2) = \operatorname{multiset}(s_1) + \operatorname{multiset}(s_2).]

Here, $++$ denotes sequence concatenation, while the addition on the right adds multiplicities. The equation says that concatenating two sequences does not lose or invent any of their elements.2 The merge sort example contains the following explicit recursive proof. It illustrates how the mathematical argument can be expressed within Verus:

pub broadcast proof fn lemma_to_multiset_distributes_over_add(
    s1: Seq<u64>, s2: Seq<u64>,
)
    ensures
        #[trigger] (s1 + s2).to_multiset()
            =~= s1.to_multiset().add(s2.to_multiset()),
    decreases s2.len(),
{
    s2.to_multiset_ensures();
    if s2.len() == 0 {
        assert((s1 + s2).to_multiset() =~= s1.to_multiset());
        assert(s2.to_multiset() =~= Multiset::<u64>::empty());
    } else {
        lemma_to_multiset_distributes_over_add(s1, s2.drop_last());
        vstd::seq::Seq::drop_last_distributes_over_add(s1, s2);
        assert(s2.drop_last() =~= s2.remove(s2.len() - 1));
        assert(s1 + s2 =~=
            (s1 + s2).drop_last().push(s2[(s2.len() - 1) as int]));
        assert((s1 + s2).to_multiset() =~=
            ((s1 + s2).drop_last().push(
                s2[(s2.len() - 1) as int],
            )).to_multiset());
        (s1 + s2).drop_last().to_multiset_ensures();
    }
}

The proof proceeds by induction on the second sequence, expressed as recursion with a decreasing length. It exposes the relevant collection properties and intermediate equalities for the solver. This example lets us compare how an explicitly written mathematical argument changes when we move it into Lean and use Mathlib’s definitions and theorems.

The corresponding Lean proof is much shorter:

@[simp, grind =] theorem toMultiset_add (s1 s2 : Seq α) :
    (s1.add s2).toMultiset = s1.toMultiset + s2.toMultiset := by
  simp [toMultiset, add]

Unfolding toMultiset and add exposes the standard conversion from lists to multisets and ordinary list append. Mathlib already knows how that conversion interacts with append. The two attributes make the proved fact available to simplification and grind, so later obligations can use it automatically.

For example, the mathematical consequence needed by the caller above can be written independently of any Rust loop:

theorem appended_elements
    (result before suffix : Vermilion.Seq Int)
    (h : result = Vermilion.Seq.add before suffix) :
    Vermilion.Seq.toMultiset result =
      Vermilion.Seq.toMultiset before +
      Vermilion.Seq.toMultiset suffix := by
  rw [h]
  exact Vermilion.Seq.toMultiset_add before suffix

This theorem consumes precisely the sequence equality established by an append operation. The program proof determines the resulting sequence; the library supplies its mathematical consequences. We still need to justify the loop invariant and check the indexing operations, but we can reuse the library of facts about collections across different programs. Verus supports such reuse within its own library too. The gain here is access to the broader body of mathematics already formalised in Mathlib.

The full merge sort example follows this separation. The repository contains both a version with Verus proof blocks and a version retaining just the algorithm, contracts, invariants, and termination measures. The latter moves the auxiliary proofs into Lean. Its recorded verification has 40 obligations, with 31 discharged automatically and nine proved interactively. Some of those interactive proofs need new lemmas, since Mathlib does not contain a ready-to-use correctness proof for this Rust implementation.

The benefit of Lean embedding grows with the mathematical content of the specification. A number-theoretic lemma can use Mathlib’s divisibility theory, and a matrix algorithm can use its linear algebra, once the program’s representation has been connected to the appropriate mathematical model. Establishing that connection takes work. After it is established, we (or your favourite AI agent) can do the mathematics in a language designed for writing mathematics rather than in Verus.

Next Steps

Vermilion is available on GitHub. It accepts ordinary Verus source, including existing specifications, for the constructs it supports. There is no separate specification dialect to learn or migration pass to run. The current support includes a substantial sequential fragment: loops, recursive specifications, collections, mutable references, and several forms of generic programming.

Vermilion remains a strict subset of Verus in language and library support, even though its proof backend can discharge some obligations that Verus’s default automation does not. In particular, it does not improve on what I consider one of Verus’s main contributions: its clever use of Rust’s ownership and typing disciplines to lower safe Rust into a representation well suited to verification. Vermilion benefits enormously from that work. By the time we reach SST, many of the complications of the source language have already been dealt with.

The experiment does not yet cover Verus’s support for unsafe memory operations or concurrency. These features do pass through the Verus pipeline: SST has an OpenInvariant statement for invariant opening, and Verus’s libraries provide contracts for permission-carrying pointers and atomic operations. However, extending Vermilion requires meaningful Lean models for those permissions, invariants, and operations.

An important direction is to make VC generation foundational. We could start with a semantics for Vermilion’s small IR and a soundness proof for its generator, then work backwards towards SST. Another possibility is to translate into an existing semantic framework, such as Velvet’s Lean computations built from monads, and reuse its verified program logic. Either approach would need a correctness argument for the incoming translation. Reusing a sound target verifier does not automatically prove the frontend sound.

Performance is another limitation. Native SMT verification is currently considerably faster on the routine obligations in this experiment. An early comparison measured a 4.2× median end-to-end slowdown on five small shared examples. A later run of the test suite comparing Verus and Vermilion measured a median of about 16×. That suite contained 180 cases checking agreement between the two verifiers, including expected failures. An order-of-magnitude overhead is a useful characterisation of the prototype’s cost, but these measurements include process startup and library loading. They do not establish a universal speed ratio between Lean proof automation and SMT solving.

This suggests combining the two backends in one framework: let Verus handle the obligations its SMT machinery solves efficiently, and use Lean where interactive reasoning or mathematical libraries make a difference. Such a system would need to state clearly which results rely on a solver verdict and which come with kernel-checked proofs. If every result must have a Lean proof, SMT proof reconstruction is an option, with its own performance cost. Keeping a Lean process alive and reusing its imported libraries should also reduce the prototype’s repeated startup overhead.

Concluding Remarks

Vermilion is an experiment I initially put together in a few days, working alone with the help of GPT Astra and Claude Fable, and subsequently extended through case studies. It would benefit from a more carefully distilled design. The current implementation has rough edges, and its larger verification claims need the same scrutiny as any research prototype’s.

Nevertheless, I believe the experiment demonstrates a useful way to build verifiers for realistic languages. We can retain the engineering that makes SMT-based verification effective while giving users access to an interactive proof assistant when they need it. It also helps to shape up important follow-up research directions: a sufficiently broad Rust semantics, correctness of Verus’s lowering, and a proved connection from that representation to the verification conditions. Having Lean check those conditions is already useful. Proving that they are the right conditions is the next step.

1. These systems differ considerably in their proof facilities. In

   particular, F* also supports tactics and user-defined proof automation. Here, I am describing their SMT-based verification workflow; the comparison below concerns Verus’s usual workflow specifically. ↩

2. Verus’s standard library already provides this identity as

   lemma_multiset_commutative, with a shorter proof. A Verus client can use that lemma directly without writing either proof body. ↩