RavenConcurrency reasoning, built in

What Raven is ​

Raven is an intermediate verification language (IVL) and an SMT-based deductive verifier for it. It occupies the same layer as Boogie, Why3, and Viper — a target that front-end tools compile to, rather than a language you ship production code in — but it treats concurrency as a first-class concern rather than something layered on afterwards.

It is also usable directly, and is designed to be teachable: the tutorial takes a single running example from a plain integer to a lock-protected object shared across threads.

Raven's metatheory is based on the Iris separation logic framework. Iris' more expressive features — higher-order quantification, impredicativity, step-indexing — are deliberately left out, and complementary features such as a higher-order module system are added to recover expressivity. The result is a logic strong enough for realistic concurrent algorithms while remaining amenable to SMT automation.

A first look ​

Two threads increment a shared counter, in an interleaving neither of them controls. A shared invariant is what makes that tractable: a fact about the counter that every thread agrees to restore after each atomic step, and that any of them may rely on:

field count: Int

// A shared invariant: a fact about `c.count` that has to hold after every
// atomic step, whichever thread just took it. Any thread that knows about `c`
// may open it, for exactly one atomic step at a time.
inv evenCount(c: Ref) {
  exists v: Int :: own(c.count, v) && v % 2 == 0
}

// `faa` (fetch-and-add) is a single indivisible step, which is what makes it
// legal to perform while the invariant is open.
proc bumpTwice(c: Ref)
  requires evenCount(c)
{
  unfold evenCount(c);
  val _ := faa(c.count, 2);
  fold evenCount(c);
}

proc client(c: Ref)
  requires evenCount(c)
{
  spawn bumpTwice(c);
  spawn bumpTwice(c);

  unfold evenCount(c);
  val x := c.count;
  assert x % 2 == 0;
  fold evenCount(c);
}

The final assert holds under every interleaving of the two spawned threads with this one, and nothing in the proof mentions interleavings at all. Note also what the invariant is not: unlike a predicate, it is ambient and freely duplicable — both threads and the client hold it at once — and it may be opened for exactly one atomic step, which is why faa is allowed inside and an ordinary read would not be.

Underneath this sits ownership: own(c.count, v) is a resource, not a fact, and the separating conjunction between two such assertions means disjoint ownership, ruling out aliasing by construction. The tutorial builds all of it up from a single-threaded counter.

For researchers ​

Raven's design, metatheory, and empirical evaluation are described in:

Raven: An SMT-Based Concurrency Verifier Ekanshdeep Gupta, Nisarg Patel, and Thomas Wies. Computer Aided Verification (CAV), 2025.10.1007/978-3-031-98668-0_4

The repository carries a growing collection of verified concurrent data structures — spin and ticket locks, a Treiber stack, atomic counters, and B+-tree templates among them — most drawn from the literature or from real systems. These double as a regression suite and as worked examples of the proof patterns Raven is meant to support.

If you are building a verification tool of your own, the extension API is the intended entry point: it lets you add syntax and proof constructs without forking the pipeline, and ships with several extensions — termination checking via decreases, Iris-style prophecy variables, and Eris-style error credits for probabilistic reasoning — as worked references.

Getting started ​

The quickest route is the Raven Verifier extension for VS Code, which bundles the verifier and Z3; Part 0 of the tutorial walks through installing it and verifying a first file. To build from source instead:

$ git clone https://github.com/nyu-acsys/raven.git
$ cd raven
$ opam switch create raven 5.2.0
$ eval $(opam env)
$ opam install . --deps-only --with-test
$ dune build && dune runtest

Raven requires opam (>= 2.1.0), OCaml 5.x, and Z3 (>= 4.13.0).

Team ​

Raven is developed at the ACSys group at New York University by

• Ekanshdeep Gupta
• Nisarg Patel
• Thomas Wies

with further contributions from everyone who has worked on the repository.