{"article":{"slug":"the-vermilion-experiment-implementing-a-lean-backend-for-verus","title":"The Vermilion Experiment: Implementing a Lean Backend for Verus","subtitle":null,"summary":"Proofs and Intuitions describes the Vermilion experiment: implementing a Lean back end for Verus to explore verified software tooling across proof assistants.","content_type":"blog_post","language":"en","canonical_url":"https://proofsandintuitions.net/2026/10/18/vermilion-experiment-lean-backend-verus/","author":{"name":"Proofs and Intuitions","url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"Proofs and Intuitions","url":"https://proofsandintuitions.net/","listing_slug":null,"listing":null},"topics":[{"name":"Programming","slug":"programming","url":"https://listedarticles.com/topics/programming"},{"name":"Research","slug":"research","url":"https://listedarticles.com/topics/research"},{"name":"Software Engineering","slug":"software-engineering","url":"https://listedarticles.com/topics/software-engineering"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":4538,"reading_minutes":20,"published_at":"2026-10-18T12:00:00.000Z","added_at":"2026-10-19T02:18:52.613Z","updated_at":"2026-10-19T02:18:52.613Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/the-vermilion-experiment-implementing-a-lean-backend-for-verus","markdown_url":"https://listedarticles.com/articles/the-vermilion-experiment-implementing-a-lean-backend-for-verus.md","example":false,"citation":"Proofs and Intuitions, Proofs and Intuitions. \"The Vermilion Experiment: Implementing a Lean Backend for Verus.\" 18 Oct 2026. https://proofsandintuitions.net/2026/10/18/vermilion-experiment-lean-backend-verus/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://proofsandintuitions.net/2026/10/18/vermilion-experiment-lean-backend-verus/"},"body_markdown":"# The Vermilion Experiment: Implementing a Lean Backend for Verus\n\nIn this post, we discuss [Vermilion](https://github.com/ilyasergey/vermilion),\nan experimental Lean backend for the [Verus](https://github.com/verus-lang/verus)\nverifier for Rust, bringing\ninteractive proofs and Lean’s mathematical libraries to programs with\nordinary Verus specifications.\n\nThe Rust examples and Lean proofs in this post, together with instructions for\nchecking them, are collected in the [open source\nrepository](https://github.com/ilyasergey/vermilion/tree/main/examples/vermilion-blog).\n\n## What a Program Verifier Does\n\nA program verifier connects two descriptions of the same computation: a program,\nwhich tells the machine how to calculate the result, and a *specification*,\nwhich says what the result should satisfy. For example, a sorting function’s\nspecification might require that the output is ordered and contains exactly the\nelements of the input. The specification leaves open the choice of the exact\nalgorithm to do so.\n\nOne common way to check the alignment between the program and its spec is to\nturn them together into a collection of mathematical propositions, called\n*verification conditions*, or VCs. Each proposition captures something that must\nhold at a particular point in the program: an addition must not overflow, a\nfunction call must satisfy its precondition, or a returned value must satisfy\nthe promised postcondition. If we can prove all these propositions, and the\ntranslation produced the right propositions, we have established that the\nprogram satisfies its specification.\n\nVerifiers such as [Dafny](https://dafny.org/),\n[Verus](https://github.com/verus-lang/verus), and [F\\*](https://fstar-lang.org/)\nuse *SMT solvers* to discharge many of these obligations automatically. SMT\nstands for [*satisfiability modulo\ntheories*](https://en.wikipedia.org/wiki/SMT_solver): a solver searches for an\nassignment of values that makes a formula true, using built-in reasoning about\ndomains such as integers, arrays, and bit vectors. To prove a VC proposition, a\nverifier asks whether its *negation* is satisfiable. If the answer is no, the VC\nholds. [Z3](https://github.com/Z3Prover/z3) and\n[cvc5](https://cvc5.github.io/) are two widely used solvers; both Dafny\nand Verus normally use Z3.\n\nThis style of verification is commonly called *auto-active*. The programmer\nprovides specifications and proof guidance in the source of the program,\nincluding assertions, auxiliary lemmas, and loop invariants. The verifier then\nattempts the proofs automatically. The division of labour is quite compelling:\nhumans state the intended properties, while the solver takes care of much of the\nlogical bookkeeping.[1](#fn:fstar)\n\nThere is a separate question about the verifier itself: why should proving its\nVCs establish anything about the original program? A *foundational* verifier\nanswers this question with a machine-checked soundness proof, connecting the\ngenerated obligations to a formal semantics of the program. For instance,\n[Velvet](https://proofsandintuitions.net/2026/01/21/multi-modal-verification-velvet/), which we\ndiscussed earlier on this blog, derives its verification machinery from a\nsemantics embedded in the Lean theorem prover. A conventional, non-foundational\nverifier leaves this connection in its trusted implementation (which might have\nbugs). It can be carefully designed and extensively tested, but a bug in the\ntranslation may still produce an incorrect verification result.\n\nBuilding a foundational verifier for a realistic language is a daunting\ntask. Before proving anything about verification conditions, we need a\nmathematical account of what programs in that language *mean*, including\ntheir memory operations and exceptional behaviours. Rust makes this\nespecially interesting with its ownership discipline, lifetimes, and unsafe\ninterfaces. Existing foundational Rust verifiers, such as\n[RefinedRust](https://iris-project.org/pdfs/2024-pldi-refinedrust.pdf), cover\nrestricted fragments of the language.\nExtending these foundations to the breadth of Rust used in practice remains\na substantial research problem.\n\nOur experiment dubbed [Vermilion](https://github.com/ilyasergey/vermilion)\n(“Verified Rust Meets Lean”) starts with a more modest question: how much can we gain by\nkeeping an existing Rust verifier’s translation and changing the means by which\nits verification conditions are proved?\n\n## When Automated Proofs Need Help\n\nSMT solvers are amazing at the kinds of reasoning that arise repeatedly in\nprogram verification. Given suitable bounds, they can prove that an array access\nis valid, establish a simple arithmetic fact, and combine facts from several\nbranches. This automation is a large part of what makes Verus pleasant to use.\n\nUnfortunately, it is also incomplete. A true statement may require induction, a\ncarefully chosen existential witness, or a mathematical lemma that the solver\nhas never been told about. Even a statement within the solver’s usual reach can\nfail because the relevant quantified fact was not instantiated at the right\nargument. Verus exposes some control over this process through *triggers*.\nConsider a specification fragment saying that every element of a sequence is\nbounded:\n\n```\nforall|i: int| 0 <= i < s.len() ==> #[trigger] s.index(i) <= bound\n```\n\nThe annotation tells the solver to use occurrences of `s.index(...)` as\ncandidates for instantiating `i`. If the proof context contains `s.index(3)`,\nthis gives the solver a reason to consider the quantified statement at `i = 3`.\nChoosing triggers well can make a proof succeed; choosing them poorly can leave\nuseful facts unused or cause an explosion of instantiations. The [Verus\nguide](https://verus-lang.github.io/verus/guide/trigger-annotations.html)\nexplains the rules. The mathematical meaning of the assertion is unchanged.\nProgramming with triggers is manageable when the missing step is obvious. It\nbecomes frustrating when we already know a proof but must work out how to\ncommunicate it through the solver’s instantiation strategy. Verus provides proof\nfunctions and assertion blocks for doing so, yet the final step still goes\nthrough its automated proving machinery.\n\nA verifier embedded in Lean would have another route available. We can inspect a\ngoal, introduce a witness, perform induction, or apply a library theorem\ndirectly. We used this combination of automatic and interactive reasoning in the\n[Velvet post](https://proofsandintuitions.net/2026/01/21/multi-modal-verification-velvet/). The\nrecent paper on [building Veil in\nLean](https://verse-lab.org/papers/veil-dafny26.pdf) discusses the broader\ndesign: making verification conditions ordinary Lean goals gives the verifier\naccess to the proof assistant’s existing proof mode, UI, and toolchain.\n\nThe same observation applies to mathematical libraries. An SMT-based\nverifier needs a library of definitions and lemmas expressed in its own\nspecification language. Verus already has a substantial one, called `vstd`,\nso users certainly do not start from nothing. Still, if an algorithm needs\nmatrix algebra, somebody must supply the relevant definitions and laws in\nthat ecosystem. A theorem in a Lean library cannot simply be invoked by a\nVerus proof.\n\nLean and Rocq have extensive mathematical libraries built over years of\nformalisation. Lean’s [Mathlib](https://leanprover-community.github.io/mathlib-overview.html)\nincludes linear algebra, number theory, and much more. If our verification\nconditions use its mathematical objects, we can reuse theorems about them.\nThis suggests the experiment: combine Verus’s ability to handle realistic\nRust with Lean’s proof mode and mathematical vocabulary.\n\n## Connecting Verus to Lean\n\nTo see where a Lean backend belongs, let us look briefly at Verus’s translation\npipeline. Verus starts with Rust extended by specification and proof constructs,\nusually written inside a `verus!` macro. Its frontend uses the Rust compiler\ninfrastructure and performs the additional checks that separate executable code,\nspecifications, and proofs. The frontend produces *VIR*, Verus’s intermediate\nrepresentation. Subsequent passes simplify VIR into *SST*, a representation that\nseparates statements from expressions and makes the verification-relevant\noperations explicit. The usual backend translates SST into AIR, a\nsolver-oriented representation, and eventually sends SMT queries to Z3.\n\nVermilion branches off at SST, before the SMT-specific encoding:\n\n```\n Rust + Verus specifications\n |\n Verus frontend and VIR\n |\n Verus simplification\n |\n SST\n / \\\n / \\\n Verus backend Vermilion adapter\n | |\n AIR Small textual IR\n | |\n SMT queries Lean VC generator\n | |\n Z3 Lean theorems\n |\n Automation or proof scripts\n |\n Lean kernel\n```\n\n*Both routes reuse Verus’s frontend and SST construction. Vermilion’s\nverification runs use the Lean route; the Z3 route is used separately for\ncomparisons.*\n\nSST is a convenient place to make this change because much of the difficult\nwork has already happened. Names and types have been resolved, complex\nsource expressions have been decomposed, and checks for operations such as\nbounded integer addition have been inserted. Function contracts and loop\ninvariants are available explicitly. So we can focus on turning this\nrepresentation into mathematical obligations.\n\nFor example, suppose the source computes `let y = x + 1` on `u32` values\nand then asserts that `y > 0`. An abbreviated, readable version of the SST\nlooks like this:\n\n```\nAssert 0 (HasType u32 (x + 1))\nAssume (HasType u32 (x + 1))\nAssign y (Clip u32 (x + 1))\nAssert 1 (y > 0)\nAssume (y > 0)\nReturn y\n```\n\nThis is pseudocode for the SST nodes, with temporary names and source locations\nremoved. The [full\nrepresentation](https://github.com/ilyasergey/vermilion/blob/main/docs/pipeline/artifacts/simple-sst.vir)\nis available in the Vermilion repository. `HasType u32` expresses the range\ncheck that prevents overflow. `Clip` converts the mathematical result back to\nthe machine integer range. Once the range check is proved, clipping preserves\nthe result. The `Assume` following an `Assert` makes an established fact\navailable to later checks; the assertion itself must still be proved.\n\nVC generation then follows familiar logical rules. An assignment substitutes\nthe assigned expression for the variable’s subsequent uses. An assertion\nbecomes a goal under the facts available at that point. A conditional adds\nits condition to one branch and its negation to the other. A function call\nrequires proving the callee’s precondition, after which the callee’s\npostcondition describes the result. This is modular reasoning: callers can\nuse a contract without expanding the callee’s implementation.\n\nThese rules can be described using [*weakest\nprecondition*](https://en.wikipedia.org/wiki/Predicate_transformer_semantics#Weakest_preconditions)\ncalculus: the conditions that must hold before a command for a desired property\nto hold afterwards. Weakest-precondition reasoning works backwards from the\ndesired result. Vermilion’s implementation instead traverses the statements\nforwards, accumulating hypotheses and emitting obligations at each check.\nThese are ordinary logical transformations; the resulting propositions do not\nrequire SMT-LIB as their output language.\n\nThe implementation keeps the Rust and Lean sides separate. A Rust adapter\nlowers SST to a small textual IR; Lean parses that IR and constructs the\ntheorem statements. It also retains source locations, so a failed theorem\ncan be reported at the corresponding Rust expression. The\n[Vermilion design document](https://github.com/ilyasergey/vermilion/blob/main/DESIGN.md)\ndescribes these stages in more detail.\n\n## From a Rust Function to Lean Goals\n\nLet us follow a simple [example](https://github.com/ilyasergey/vermilion/blob/main/examples/vermilion-blog/vermilion_blog.rs#L18-L25) from the Vermilion test suite:\n\n```\nfn increment(x: u32) -> (y: u32)\n requires x < 100,\n ensures y == x + 1,\n{\n let y = x + 1;\n assert(y > 0);\n y\n}\n```\n\nHere, `requires` states the precondition, and `ensures` states the\npostcondition. The return value is named `y` so that the specification can\nrefer to it. As in the rest of the Rust snippets below, the surrounding\nimports and `verus!` wrapper are omitted.\n\nVermilion represents a `u32` value as a Lean integer together with an\nexplicit range hypothesis. The predicate `Vermilion.inUnsignedRange 32 x`\nmeans $0 \\leq x < 2^{32}$. This representation lets arithmetic tactics\nreason about ordinary integers while keeping the machine bounds visible.\n\nThe first generated obligation in Lean is the inserted overflow check:\n\n```\ntheorem assert_0\n (x : Int)\n (requires_0 : Vermilion.inUnsignedRange 32 x)\n (requires_1 : x < 100) :\n Vermilion.inUnsignedRange 32 (x + 1) := by\n vrml\n```\n\nThe theorem says exactly what we expect: adding one to a nonnegative integer\nsmaller than 100 produces a value that fits in 32 bits. `vrml` is\nVermilion’s default proof tactic; we will return to it shortly.\n\nThe next obligation comes from our explicit assertion:\n\n```\ntheorem assert_1\n (x : Int)\n (requires_0 : Vermilion.inUnsignedRange 32 x)\n (requires_1 : x < 100)\n (assert_0 : Vermilion.inUnsignedRange 32 (x + 1)) :\n ((x + 1) % 4294967296) > 0 := by\n vrml\n```\n\nNotice two details. First, the earlier overflow check is now a hypothesis.\nSecond, the remainder operation is still present: $4294967296 = 2^{32}$,\nand unsigned clipping is represented by reduction modulo this number. The\nrange hypothesis makes the remainder equal to `x + 1`, so the assertion\nfollows. Preserving this operation also matters for programs that use\nwrapping arithmetic explicitly.\n\nFinally, the postcondition asks us to establish\n`((x + 1) % 4294967296) = x + 1` under the accumulated hypotheses. All\nthree obligations are proved automatically. The complete generated statements\nand their proofs are available in the respective\n[Lean file](https://github.com/ilyasergey/vermilion/blob/main/examples/vermilion-blog/proofs/vermilion_blog/increment.lean).\n\n### Verification Conditions for Loops\n\nNow consider a function that counts from zero up to its input:\n\n```\n#[verifier::exec_allows_no_decreases_clause]\nfn count_to(n: u32) -> (c: u32)\n requires n < 1000,\n ensures n == c,\n{\n let mut c: u32 = 0;\n while c < n\n invariant c <= n,\n {\n c = c + 1;\n }\n c\n}\n```\n\nThe loop invariant says that the counter never exceeds `n`. To use it, the\nverifier must first prove it holds when entering the loop and then prove\nthat one iteration preserves it. This is an induction argument: the initial\nstate supplies the base case, and the loop body supplies the induction step.\nAt loop exit, the invariant and the negated loop condition together imply\nthe postcondition.\n\nThis example produces [four\nobligations](https://github.com/ilyasergey/vermilion/blob/main/examples/vermilion-blog/proofs/vermilion_blog/count_to.lean).\nFor brevity, let us retain only the range hypotheses needed for each check and\nsimplify the checked clipping operation. Their mathematical content becomes:\n\n```\nEntry: 0 ≤ n\nOverflow: 0 ≤ c, c < n, n < 2^32 ⊢ 0 ≤ c + 1 < 2^32\nPreservation: c ≤ n, c < n ⊢ c + 1 ≤ n\nExit: c ≤ n, ¬(c < n) ⊢ n = c\n```\n\nThe symbol `⊢` separates the assumptions from the goal. The preservation\ncheck considers an *arbitrary* iteration, so it cannot assume that `c` is\nstill zero. The counter is constrained by its machine range, the invariant,\nand the loop condition. This is what makes the finite collection of obligations\nsufficient to cover arbitrarily many loop iterations.\n\nThe actual exit theorem is still quite readable:\n\n```\ntheorem ensures_1\n (n c : Int)\n (requires_0 : Vermilion.inUnsignedRange 32 n)\n (requires_1 : n < 1000)\n (loop_0_exit_0 : Vermilion.inUnsignedRange 32 c)\n (loop_0_exit_1 : c ≤ n)\n (loop_0_exit_2 : ¬(c < n)) :\n n = c := by\n vrml\n```\n\nThe attribute above the Rust function allows us to drop the need to prove\ntermination. This example proves *partial correctness*: if the function returns,\nits result satisfies the postcondition. The loop does terminate, but proving\ntermination is a separate obligation. A `decreases` annotation supplies a\nmeasure for that purpose; it is supported by Vermilion, and other examples in the repository exercise those\nchecks.\n\nConceptually, we have made a fairly small change: the obligations that would\nhave gone to an SMT solver are now expressed as Lean theorems, ready to be\nproved in Lean. The engineering includes many details about types and\ncontracts, but the overall idea is simple.\n\nIt is important to note that this translation is not yet foundational: Vermilion\ndoes not prove that its VCs correctly describe Rust’s semantics, SST’s\nsemantics, or even the semantics of its own textual IR. The translation and VC\ngenerator remain trusted. Lean checks proofs of the statements we emit; it\ncannot tell us that we emitted the right statements. The Vermilion [trust\ndocument](https://github.com/ilyasergey/vermilion/blob/main/docs/trust.md)\nrecords these boundaries, including the responsibility of the surrounding\ntooling to check every obligation and report failures correctly.\n\nA foundational generator for the IR is a plausible next step. We could give the\nIR a semantics in Lean and prove that its verification conditions imply the\ndesired property of executions, following the approach developed in\n[Loom](https://verse-lab.org/papers/loom-popl26.pdf) and later integrated into\n[Lean’s `vcgen`](https://lean-lang.org/doc/reference/latest/The--vcgen--tactic/),\nwhich generates verification conditions for programs with a weakest-precondition\nsemantics, including monadic computations. Proving our generator sound would\nremove one part of the trusted translation.\nConnecting the result back through SST to Rust would remain a further theorem to\nprove.\n\n## Taking Over with Interactive Proofs When Automation Stops\n\nWe can now use the part of Lean that motivated the experiment: its\ninteractive proof mode.\n\nVermilion first tries to prove each obligation automatically. Its `vrml`\ntactic combines Lean tactics such as `grind`, `omega`, and `simp` with\nspecialised procedures, including nonlinear arithmetic reasoning. It also\nhas an SMT fallback that reconstructs a Lean proof. In each case, proof\nsearch produces a term for the kernel to check. A failed attempt leaves an\nopen obligation that we can prove ourselves.\n\nHere is a deliberately small\n[example](https://github.com/ilyasergey/vermilion/blob/main/examples/vermilion-blog/vermilion_blog.rs#L43-L49)\nfrom the Vermilion repository:\n\n```\nproof fn witness_shift(y: int)\n requires\n exists|x: int| #[trigger] (x + x) == y,\n ensures\n exists|x: int| #[trigger] (x + x) == y + 2,\n{\n}\n```\n\nThis is a *proof function*: it expresses a lemma and is erased from the\nexecutable program. The lemma says that if `y` is twice an integer, then\n`y + 2` is also twice an integer. The source body is empty because we will\nprovide the proof on the Lean side.\n\nThe mathematical argument behind it is trivial: take the witness `x` from the\nprecondition and choose `x + 1` for the postcondition. The remaining equality\nis linear arithmetic. Yet the solver still has to discover that witness\nthrough its quantified encoding; the trigger does not instruct it to\nconstruct `x + 1`. The repository uses this example to demonstrate an\ninteractive proof beyond the default automation. It is perfectly possible\nto supply the missing guidance in Verus too; we are comparing ways of\nexpressing the proof, rather than claiming an impossibility result about SMT.\n\nOn the Lean side, the whole proof is two lines:\n\n```\ntheorem ensures_0\n (y : Int)\n (requires_0 : ∃ x : Int, x + x = y) :\n (∃ x : Int, x + x = y + 2) := by\n obtain ⟨x, hx⟩ := requires_0\n exact ⟨x + 1, by omega⟩\n```\n\nThe first line extracts the witness and its defining equality. The second\nsupplies the new witness and asks `omega` to check the arithmetic. In the\nLean InfoView, we can inspect the context after each step: the proof state\nshows `x`, the hypothesis `hx : x + x = y`, and the remaining goal.\n\nThis little proof illustrates the workflow for much larger obligations as\nwell. We can introduce an intermediate lemma, use induction, or search\nMathlib for an applicable theorem. We can also ask a favourite coding agent\nto complete the proof in the same file, using Lean’s feedback. The agent’s\noutput goes through the same proof checking as a handwritten script.\n\n### Jumping from Rust to the Proof\n\nVermilion’s VS Code extension connects the two views of a program. Placing\nthe cursor on a Rust assertion, postcondition, or loop invariant and pressing\n**⌘⇧J** on macOS, or **Ctrl+Shift+J** elsewhere, opens the corresponding\nLean obligation. If one annotation generates several VCs, such as an\ninvariant’s entry and preservation checks, a picker lets us choose which one\nto inspect. The shortcut also works in reverse, returning from a Lean\nobligation to its Rust source.\n\n![Vermilion in VS Code: navigating between binary search in Rust and its Lean proof obligations](https://github.com/ilyasergey/vermilion/raw/main/docs/assets/vermilion-demo.gif)\n*The demo shows Rust verification alongside the generated Lean obligations and the\nLean InfoView.*\n\nThis navigation feature is useful even when automation succeeds. We can look at\nexactly what the VC generator produced: which hypotheses are available, how the\nmachine bounds were represented, and what the postcondition became after\nsubstitution. When a proof fails, the same view helps distinguish a missing\ninvariant from a missing mathematical argument. That is a much more concrete\nstarting point than an unexplained failure at a source line.\n\nThe Lean proofs can be edited alongside the Rust source. When we check the\nprogram again, Vermilion keeps proofs of obligations that have not changed.\nIf an obligation changes, its proof needs to be checked against the new\nstatement. This lets source programs and Lean proofs evolve together while\npreserving the user’s work. Vermilion comes with a [tutorial](https://github.com/ilyasergey/vermilion/blob/main/docs/TUTORIAL.md) that\nwalks through this process, including deliberately breaking a postcondition\nand seeing Lean’s failure reported back at the Rust location.\n\n## Doing the Mathematics in Lean\n\nThe second benefit appears when we choose the mathematical objects used by\nthe embedding. Vermilion represents a Verus `Seq` as a Lean `List`, and\na Verus `Multiset` as Mathlib’s `Multiset`. Consequently, many facts about\nthe translated specifications are already library theorems.\n\nFor a small executable example, consider this helper used in [merge sort](https://github.com/ilyasergey/vermilion/blob/main/examples/vermilion-blog/vermilion_blog.rs#L52-L64):\n\n```\nfn extend_from_idx(r: &mut Vec, v: &Vec, start: usize)\n requires\n start < v.len(),\n ensures\n final(r)@ == old(r)@ + v@.subrange(start as int, v.len() as int),\n{\n for i in start..v.len()\n invariant\n r@ == old(r)@ + v@.subrange(start as int, i as int),\n {\n r.push(v[i]);\n }\n}\n```\n\nThe helper appends a suffix of `v` to `r`. The notation `v@` denotes the\nvector’s mathematical sequence of elements; `old(r)` and `final(r)` refer\nto the values before and after the mutable borrow. The postcondition\ndescribes exactly which suffix was appended, and the invariant describes\nthe prefix of that work completed so far.\n\nA caller implementing a sorting algorithm often needs a further consequence:\nappending these elements preserves their multiplicities. A *multiset*\nforgets the order of a sequence while remembering how often each element\noccurs. We therefore want the identity\n\n\\[\\operatorname{multiset}(s\\_1 \\mathbin{+\\!+} s\\_2)\n= \\operatorname{multiset}(s\\_1) + \\operatorname{multiset}(s\\_2).\\]\n\nHere, $++$ denotes sequence concatenation, while the addition on the right adds\nmultiplicities. The equation says that concatenating two sequences does not lose\nor invent any of their elements.[2](#fn:multiset-lemma) The merge sort example\ncontains the following [explicit recursive\nproof](https://github.com/ilyasergey/vermilion/blob/main/examples/vermilion-blog/vermilion_blog.rs#L67-L91).\nIt illustrates how the mathematical argument can be expressed within Verus:\n\n```\npub broadcast proof fn lemma_to_multiset_distributes_over_add(\n s1: Seq, s2: Seq,\n)\n ensures\n #[trigger] (s1 + s2).to_multiset()\n =~= s1.to_multiset().add(s2.to_multiset()),\n decreases s2.len(),\n{\n s2.to_multiset_ensures();\n if s2.len() == 0 {\n assert((s1 + s2).to_multiset() =~= s1.to_multiset());\n assert(s2.to_multiset() =~= Multiset::::empty());\n } else {\n lemma_to_multiset_distributes_over_add(s1, s2.drop_last());\n vstd::seq::Seq::drop_last_distributes_over_add(s1, s2);\n assert(s2.drop_last() =~= s2.remove(s2.len() - 1));\n assert(s1 + s2 =~=\n (s1 + s2).drop_last().push(s2[(s2.len() - 1) as int]));\n assert((s1 + s2).to_multiset() =~=\n ((s1 + s2).drop_last().push(\n s2[(s2.len() - 1) as int],\n )).to_multiset());\n (s1 + s2).drop_last().to_multiset_ensures();\n }\n}\n```\n\nThe proof proceeds by induction on the second sequence, expressed as\nrecursion with a decreasing length. It exposes the relevant collection\nproperties and intermediate equalities for the solver. This example\nlets us compare how an explicitly written mathematical argument changes when\nwe move it into Lean and use Mathlib’s definitions and theorems.\n\nThe corresponding [Lean proof](https://github.com/ilyasergey/vermilion/blob/main/lean/Vermilion/Vstd/SeqLib.lean)\nis much shorter:\n\n```\n@[simp, grind =] theorem toMultiset_add (s1 s2 : Seq α) :\n (s1.add s2).toMultiset = s1.toMultiset + s2.toMultiset := by\n simp [toMultiset, add]\n```\n\nUnfolding `toMultiset` and `add` exposes the standard conversion from lists\nto multisets and ordinary list append. Mathlib already knows how that\nconversion interacts with append. The two attributes make the proved fact\navailable to simplification and `grind`, so later obligations can use it\nautomatically.\n\nFor example, the mathematical consequence needed by the caller above can\nbe written independently of any Rust loop:\n\n```\ntheorem appended_elements\n (result before suffix : Vermilion.Seq Int)\n (h : result = Vermilion.Seq.add before suffix) :\n Vermilion.Seq.toMultiset result =\n Vermilion.Seq.toMultiset before +\n Vermilion.Seq.toMultiset suffix := by\n rw [h]\n exact Vermilion.Seq.toMultiset_add before suffix\n```\n\nThis theorem consumes precisely the sequence equality established by an\nappend operation. The program proof determines the resulting sequence; the\nlibrary supplies its mathematical consequences. We still need to justify the\nloop invariant and check the indexing operations, but we can reuse the\nlibrary of facts about collections across different programs. Verus supports\nsuch reuse within its own library too. The gain here is access to the broader\nbody of mathematics already formalised in Mathlib.\n\nThe full [merge sort example](https://github.com/ilyasergey/vermilion/tree/main/case-studies/merge-sort)\nfollows this separation. The\nrepository contains both a version with Verus proof blocks and a\nversion retaining just the algorithm, contracts, invariants, and termination\nmeasures. The latter moves the auxiliary proofs into Lean. Its recorded\nverification has 40 obligations, with 31 discharged automatically and nine\nproved interactively. Some of those interactive proofs need\nnew lemmas, since Mathlib does not contain a ready-to-use correctness\nproof for this Rust implementation.\n\nThe benefit of Lean embedding grows with the mathematical content of the\nspecification. A number-theoretic lemma can use Mathlib’s divisibility theory,\nand a matrix algorithm can use its linear algebra, once the program’s\nrepresentation has been connected to the appropriate mathematical model.\nEstablishing that connection takes work. After it is established, we (or your\nfavourite AI agent) can do the mathematics in a language designed for writing\nmathematics rather than in Verus.\n\n## Next Steps\n\n[Vermilion is available on GitHub](https://github.com/ilyasergey/vermilion). It\naccepts ordinary Verus source, including existing specifications, for the\nconstructs it supports. There is no separate specification dialect to learn or\nmigration pass to run. The current support includes a substantial sequential\n[fragment](https://github.com/ilyasergey/vermilion/blob/main/docs/support.md):\nloops, recursive specifications, collections, mutable references, and several\nforms of generic programming.\n\nVermilion remains a strict subset of Verus in language and library support,\neven though its proof backend can discharge some obligations that Verus’s\ndefault automation does not. In particular, it does not improve on what I\nconsider one of Verus’s main contributions: its clever use of Rust’s\nownership and typing disciplines to lower safe Rust into a representation\nwell suited to verification. Vermilion benefits enormously from that work.\nBy the time we reach SST, many of the complications of the source language\nhave already been dealt with.\n\nThe experiment does not yet cover Verus’s support for unsafe memory operations\nor concurrency. These features do pass through the Verus pipeline: SST has an\n`OpenInvariant` statement for invariant opening, and Verus’s libraries provide\ncontracts for permission-carrying pointers and atomic operations. However,\nextending Vermilion requires meaningful Lean models for those permissions,\ninvariants, and operations.\n\nAn important direction is to make VC generation foundational. We could start\nwith a semantics for Vermilion’s small IR and a soundness proof for its\ngenerator, then work backwards towards SST. Another possibility is to translate\ninto an existing semantic framework, such as Velvet’s Lean computations built\nfrom monads, and reuse its verified program logic. Either approach would need a\ncorrectness argument for the incoming translation. Reusing a sound target\nverifier does not automatically prove the frontend sound.\n\nPerformance is another limitation. Native SMT verification is currently\nconsiderably faster on the routine obligations in this experiment. An [early\ncomparison](https://github.com/ilyasergey/vermilion/blob/main/docs/reports/vermilion-vs-verus-timing.md)\nmeasured a 4.2× median end-to-end slowdown on five small shared examples. A\nlater run of the test suite comparing Verus and Vermilion measured a median of\nabout 16×. That suite contained 180 cases checking agreement between the two\nverifiers, including expected failures. An order-of-magnitude overhead is a\nuseful characterisation of the prototype’s cost, but these measurements include\nprocess startup and library loading. They do not establish a universal speed\nratio between Lean proof automation and SMT solving.\n\nThis suggests combining the two backends in one framework: let Verus handle\nthe obligations its SMT machinery solves efficiently, and use Lean where\ninteractive reasoning or mathematical libraries make a difference. Such a\nsystem would need to state clearly which results rely on a solver verdict\nand which come with kernel-checked proofs. If every result must have a Lean\nproof, SMT proof reconstruction is an option, with its own performance cost.\nKeeping a Lean process alive and reusing its imported libraries should also\nreduce the prototype’s repeated startup overhead.\n\n## Concluding Remarks\n\nVermilion is an experiment I initially put together in a few days, working alone\nwith the help of GPT Astra and Claude Fable, and subsequently extended through case\nstudies. It would benefit from a more carefully distilled design. The current\nimplementation has rough edges, and its larger verification claims need the same\nscrutiny as any research prototype’s.\n\nNevertheless, I believe the experiment demonstrates a useful way to build\nverifiers for realistic languages. We can retain the engineering that makes\nSMT-based verification effective while giving users access to an interactive\nproof assistant when they need it. It also helps to shape up important follow-up\nresearch directions: a sufficiently broad Rust semantics, correctness of Verus’s\nlowering, and a proved connection from that representation to the verification\nconditions. Having Lean check those conditions is already useful. Proving that\nthey are the right conditions is the next step.\n\n1. These systems differ considerably in their proof facilities. In\n particular, F\\* also supports tactics and user-defined proof automation.\n Here, I am describing their SMT-based verification workflow; the\n comparison below concerns Verus’s usual workflow specifically. [↩](#fnref:fstar)\n2. Verus’s standard library already provides this identity as\n [`lemma_multiset_commutative`](https://github.com/verus-lang/verus/blob/48600836424a79420589c56d86e720236a029811/source/vstd/seq_lib.rs#L3203-L3218),\n with a shorter proof. A Verus client can use that lemma directly without\n writing either proof body. [↩](#fnref:multiset-lemma)\n","body_html":"

The Vermilion Experiment: Implementing a Lean Backend for Verus

\n

In this post, we discuss Vermilion,\nan experimental Lean backend for the Verus\nverifier for Rust, bringing\ninteractive proofs and Lean’s mathematical libraries to programs with\nordinary Verus specifications.

\n

The Rust examples and Lean proofs in this post, together with instructions for\nchecking them, are collected in the open source\nrepository.

\n

What a Program Verifier Does

\n

A program verifier connects two descriptions of the same computation: a program,\nwhich tells the machine how to calculate the result, and a specification,\nwhich says what the result should satisfy. For example, a sorting function’s\nspecification might require that the output is ordered and contains exactly the\nelements of the input. The specification leaves open the choice of the exact\nalgorithm to do so.

\n

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

\n

Verifiers such as Dafny,\nVerus, and F*\nuse SMT solvers to discharge many of these obligations automatically. SMT\nstands for *satisfiability modulo\ntheories*: a solver searches for an\nassignment of values that makes a formula true, using built-in reasoning about\ndomains such as integers, arrays, and bit vectors. To prove a VC proposition, a\nverifier asks whether its negation is satisfiable. If the answer is no, the VC\nholds. Z3 and\ncvc5 are two widely used solvers; both Dafny\nand Verus normally use Z3.

\n

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

\n

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

\n

Building a foundational verifier for a realistic language is a daunting\ntask. Before proving anything about verification conditions, we need a\nmathematical account of what programs in that language mean, including\ntheir memory operations and exceptional behaviours. Rust makes this\nespecially interesting with its ownership discipline, lifetimes, and unsafe\ninterfaces. Existing foundational Rust verifiers, such as\nRefinedRust, cover\nrestricted fragments of the language.\nExtending these foundations to the breadth of Rust used in practice remains\na substantial research problem.

\n

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

\n

When Automated Proofs Need Help

\n

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

\n

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

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

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

\n

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

\n

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

\n

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

\n

Connecting Verus to Lean

\n

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

\n

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

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

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

\n

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

\n

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

\n
Assert 0 (HasType u32 (x + 1))\nAssume   (HasType u32 (x + 1))\nAssign y (Clip u32 (x + 1))\nAssert 1 (y > 0)\nAssume   (y > 0)\nReturn y
\n

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

\n

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

\n

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

\n

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

\n

From a Rust Function to Lean Goals

\n

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

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

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

\n

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

\n

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

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

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

\n

The next obligation comes from our explicit assertion:

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

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

\n

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

\n

Verification Conditions for Loops

\n

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

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

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

\n

This example produces four\nobligations.\nFor brevity, let us retain only the range hypotheses needed for each check and\nsimplify the checked clipping operation. Their mathematical content becomes:

\n
Entry:         0 ≤ n\nOverflow:      0 ≤ c, c < n, n < 2^32  ⊢  0 ≤ c + 1 < 2^32\nPreservation:  c ≤ n, c < n            ⊢  c + 1 ≤ n\nExit:          c ≤ n, ¬(c < n)         ⊢  n = c
\n

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

\n

The actual exit theorem is still quite readable:

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

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

\n

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

\n

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

\n

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

\n

Taking Over with Interactive Proofs When Automation Stops

\n

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

\n

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

\n

Here is a deliberately small\nexample\nfrom the Vermilion repository:

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

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

\n

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

\n

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

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

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

\n

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

\n

Jumping from Rust to the Proof

\n

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

\n
\"Vermilion
\n

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

\n

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

\n

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

\n

Doing the Mathematics in Lean

\n

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

\n

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

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

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

\n

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

\n

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

\n

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

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

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

\n

The corresponding Lean proof\nis much shorter:

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

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

\n

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

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

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

\n

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

\n

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

\n

Next Steps

\n

Vermilion is available on GitHub. It\naccepts ordinary Verus source, including existing specifications, for the\nconstructs it supports. There is no separate specification dialect to learn or\nmigration pass to run. The current support includes a substantial sequential\nfragment:\nloops, recursive specifications, collections, mutable references, and several\nforms of generic programming.

\n

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

\n

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

\n

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

\n

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

\n

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

\n

Concluding Remarks

\n

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

\n

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

\n

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

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

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

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

","headings":[{"level":1,"text":"The Vermilion Experiment: Implementing a Lean Backend for Verus","id":"the-vermilion-experiment-implementing-a-lean-backend-for-verus"},{"level":2,"text":"What a Program Verifier Does","id":"what-a-program-verifier-does"},{"level":2,"text":"When Automated Proofs Need Help","id":"when-automated-proofs-need-help"},{"level":2,"text":"Connecting Verus to Lean","id":"connecting-verus-to-lean"},{"level":2,"text":"From a Rust Function to Lean Goals","id":"from-a-rust-function-to-lean-goals"},{"level":3,"text":"Verification Conditions for Loops","id":"verification-conditions-for-loops"},{"level":2,"text":"Taking Over with Interactive Proofs When Automation Stops","id":"taking-over-with-interactive-proofs-when-automation-stops"},{"level":3,"text":"Jumping from Rust to the Proof","id":"jumping-from-rust-to-the-proof"},{"level":2,"text":"Doing the Mathematics in Lean","id":"doing-the-mathematics-in-lean"},{"level":2,"text":"Next Steps","id":"next-steps"},{"level":2,"text":"Concluding Remarks","id":"concluding-remarks"}]}}