Adding Velvet to your Project

Add Velvet to your lakefile.toml:

[[require]]
name = "velvet"
git = "https://github.com/verse-lab/velvet.git"
rev = "main"

Your First Velvet Method

Here is a minimal, complete example:

import Velvet

method isqrt (n : Nat) returns (r : Nat)
  requires True
  ensures r * r ≤ n ∧ n < (r + 1) * (r + 1)
do
  let mut x : Nat := 0
  while loop_cond: (x + 1) * (x + 1) ≤ n
    invariant inv_lower: x * x ≤ n
    decreasing by_remaining: n - x * x
    done_with done: n < (x + 1) * (x + 1)
  do
    x := x + 1
  return x

prove_correct isqrt by
  velvet_vcgen [isqrt] with finish

This example demonstrates:

• Method signature: Typed input parameters and named return value (returns (r : Nat)).

• Contracts: Preconditions (requires) and postconditions (ensures).

• Loop annotations: Inductive invariant (invariant), termination measure (decreasing), and exit condition (done_with).

• Verification: Automatic proof of the generated theorem isqrt.spec via prove_correct isqrt by velvet_vcgen [isqrt] with finish.

NOTE: A prove_correct block is one of two ways to verify a method. The other is to write set_option velvet.verifyOnDefinition true in directly above method: Velvet then attempts the proof with velvet_vcgen [<method_name>] with finish as soon as the method is defined, so no prove_correct block is needed. If automation cannot discharge every obligation, it reports an error at the unproven assertion. The examples in Loop Verification use this style.

Logical Variables (given Clause)

The given clause introduces logical (ghost) variables scoped exclusively to the specification (requires, signals, and ensures). They do not exist at runtime and cannot be referenced inside the executable do body.

method incrementBy (x : Nat) returns (res : PUnit) in StateM Nat
  given (s₀ : Nat)
  requires (s : Nat) => s = s₀
  ensures (s : Nat) => s = s₀ + x
do
  let s ← get
  set (s + x)

prove_correct incrementBy by
  velvet_vcgen [incrementBy] with finish

#check @incrementBy.spec
-- incrementBy.spec : ∀ (x s₀ : Nat),
--   ⦃ fun s => s = s₀ ⦄ incrementBy x ⦃ fun res s => s = s₀ + x ⦄

Recursive Methods (method rec)

Use method rec when a method calls itself. In inductive proofs, pass the induction hypothesis to velvet_vcgen [ih] to handle the recursive call:

method rec countUp (n : Nat)
  returns (res : Nat)
  ensures res_eq: res = n
do
  match n with
  | .zero => pure 0
  | .succ k =>
    let b ← countUp k
    pure (Nat.succ b)

prove_correct countUp by
  intro n
  induction n with
  | zero => unfold countUp; velvet_vcgen with finish
  | succ k ih => unfold countUp; velvet_vcgen with finish

Automatic ExceptT Inference

When in <Monad> is omitted, typed exception binders automatically infer nested ExceptT layers over Option:

method maybeFail (b : Bool) returns (res : Nat)
  requires True
  signals boom : (e : String) => e = "boom"
  ensures res = 0
do
  if b then throw "boom"
  return 0

#check maybeFail  -- maybeFail (b : Bool) : ExceptT String Option Nat

Pure State Invariants (No done_with needed)

If an invariant only mentions outer mutable state variables (e.g., let mut x := 0), Velvet automatically uses the invariant as both the inductive step invariant and the loop-exit condition:

set_option velvet.verifyOnDefinition true in
method twoVarPureState (n : Nat) returns (r : Nat)
  ensures r % 2 = 0
do
  let mut x := 0
  let mut y := 0
  for i in List.range n
    invariant xy_even: (x + y) % 2 = 0  -- Mentions only outer state
  do
    x := x + 1
    y := y + 1
  return x + y

Iteration-Local Variables and done_with

Variables tied to loop iteration (i, __pref, __rest) go out of scope upon loop exit. When an invariant references iteration-local variables, an explicit done_with clause specifies what holds on termination:

set_option velvet.verifyOnDefinition true in
method twoVar (n : Nat) returns (r : Nat)
  ensures r = n
do
  let mut x := 0
  let mut y := 0
  for i in List.range n
    invariant xy: x = i ∧ y = i
    done_with d: x = n ∧ y = n
  do
    x := x + 1
    y := y + 1
  return x

In-Scope Membership Proof (for h : x in xs)

You can bind a proof that the current element belongs to the collection:

set_option velvet.verifyOnDefinition true in
method memberBound (xs : List Nat) (bound : Nat) returns (sum : Nat)
  requires ∀ x ∈ xs, x ≤ bound
  ensures sum ≥ 0
do
  let mut s := 0
  for h : x in xs
    invariant nonneg: s ≥ 0
  do
    assert h_in: x ∈ xs  -- `h : x ∈ xs` is directly in scope!
    s := s + x
  return s

Control Flow: break, continue, and Early return

Velvet supports standard imperative control flow inside loops:

• continue: Skips the rest of the current iteration while preserving the loop invariant.

• break: Exits the loop early (done_with specifies the early exit condition).

• return: Returns immediately from the enclosing method.

assert

Emits a named proof obligation at that program point and adds the assertion to the hypothesis context thereafter:

assert <name> : <Predicate>

Assertions are checked during verification but erased at execution time as they provably hold.

Ghost State (let ghost and *:=)

Ghost variables exist purely for specification and proof purposes:

• Declaration: let ghost <name> := <value>

• Reassignment: <name> *:= <new_value>

• Reading in specifications: <name>.reveal

open scoped GhostSyntax

method tickWithGhost returns (res : Nat)
  requires True
  ensures True
do
  let mut i := 0
  let ghost ctr := 0
  while loop_cond: i < 10
    invariant ghost_ctr: ctr.reveal = i
    decreasing rem: 10 - i
  do
    i := i + 1
    ctr *:= ctr + 1
  return i

Ghost gives us almost-zero overhead at runtime, and can be really useful to do logical computations in a monad, that would affect the proof but have no effects during execution.

Ghost in Velvet is inspired from Mathlib's Erased.lean

Automated Proofs (with finish)

When all verification conditions can be discharged automatically with Lean's grind tactic and arithmetic simplification:

prove_correct <method_name> by
  velvet_vcgen [<method_name>] with finish

Generally if you expect your proof to be discharged with finish, we recommend having set_option velvet.verifyOnDefinition true, which would remove the need to write out prove_correct block, and in case verification fails, it'll generally highlight the error at the offending assertion location.

Interactive Proofs (with try finish)

When some goals require interactive tactics, use with try finish to automatically discharge routine goals and solve remaining subgoals with case <tag> => ...:

prove_correct <method_name> by
  velvet_vcgen [<method_name>] with try finish
  case <tag> => <interactive_tactic>

Simplifying Assumptions

Supply definitions to unfold, specification theorems, or hypothesis simplification lemmas:

velvet_vcgen [definitions_or_specs]
  simplifying_assumptions [lemma₁, lemma₂]
  with finish

Verification Condition Reports

Enable set_option velvet_vcgen.showVCReport true to inspect live VC status:

[vcgen:isqrt] 2/3 VCs solved
  ✔ inv_lower: solved by velvet_vcgen
  ✔ by_remaining: solved afterward
  ○ done: 1 remaining

Deriving Executable Checkers

open Velvet.Testing

method increment (x : Nat) returns (result : Nat) in StateM Nat
  given (initial : Nat)
  requires (s : Nat) => s = initial ∧ s + x ≤ 100
  ensures (s : Nat) => result = initial ∧ s = initial + x
do
  let old ← get
  set (old + x)
  return old

#derive_tester_for increment

-- Checker arguments: method arguments, given arguments, initial states/environments:
#eval increment.check 5 20 20  -- TestVerdict.pass
#eval increment.check 5 99 99  -- TestVerdict.discard

The checker takes the method's arguments, then its given variables, then the initial state (for stacked monads, one initial state or environment per layer, in monad-stack order). So increment.check 5 20 20 runs increment with x = 5, initial = 20 and starting state 20. The precondition holds (20 + 5 ≤ 100) and the result satisfies ensures, so the verdict is pass. With starting state 99, 99 + 5 ≤ 100 is false, so the input is discarded.

The Three-Way Verdict (TestVerdict)

• TestVerdict.pass: Preconditions held, the method executed to completion, and all postconditions (or expected signals) were satisfied.

• TestVerdict.discard: Preconditions were false (requires failed); the input was discarded without executing the method.

• TestVerdict.fail: Preconditions held, but the method returned an unexpected result or failed its postconditions/signals.

Automated Property-Based Testing with Plausible

Because #derive_tester_for generates a pure, generator-independent checker function <method>.check, you can hook it directly into Plausible to generate hundreds of random test cases at elaboration time using run_elab do:

public import Plausible

run_elab do
  let numTests := 100
  let input : Plausible.Gen (Nat × Nat) := do
    let x ← Plausible.SampleableExt.interpSample Nat
    let s ← Plausible.SampleableExt.interpSample Nat
    return (x, s)
  let mut passed := 0
  let mut discarded := 0
  for _ in [0:numTests] do
    let (x, s) ← Plausible.Gen.run input 100
    match increment.check x s s with
    | .pass => passed := passed + 1
    | .discard => discarded := discarded + 1
    | .fail => throwError "increment failed for x = {x}, initial state = {s}"
  IO.println s!"PBT: out of {numTests} tests, {discarded} discarded, {passed} passed"

When evaluated, Lean outputs live test metrics: PBT: out of 100 tests, 78 discarded, 22 passed

If an input triggers a contract bug (.fail), throwError halts Lean elaboration and points directly to the failing inputs!

Decidability & Custom Decision Procedures

The checker requires an executable way to evaluate whether each condition holds. Velvet automatically handles many common conditions (including equalities, orderings, and bounded Nat/Int quantifiers).

If a custom contract condition cannot be automatically decided, provide a decision proof before #derive_tester_for:

• prove_precondition_decidable_for <method> by ...

• prove_postcondition_decidable_for <method> by ...

• prove_signals_decidable_for <method> by ...