An Extension API for the Concurrent Program Verifier Raven

Abstract

Raven is an intermediate verification language (IVL) and SMT-based deductive verifier for concurrent programs, combining a program logic rooted in the concurrent separation logic Iris, with robust proof automation. We present a new Extension API that allows users to enrich the Raven IVL with domain-specific types, expressions, and commands by plugging directly into Raven’s verification pipeline via OCaml’s extensible variant types. Extensions are lightweight and composable, expanding Raven’s utility across multiple use-cases: as a backend IVL for building front-end verifiers, as a standalone modeling tool for verifying concurrent programs, for rapid prototyping of new concurrency reasoning principles and separation logics, and for pedagogical use. We demonstrate the API through four case studies by developing extensions for: hardware concurrency primitives, Iris-style prophecy variables, and error credits for probabilistic programs. Each extension requires only a few hundred lines of OCaml. Compared to interactive Rocq proofs built on analogous Iris extensions, Raven’s extensions continue to achieve an order-of-magnitude reduction in proof size and a several-fold speedup in verification time by exploiting SMT automation–albeit at the cost of an increased trusted code base. We further show that combining extensions requires careful vetting, as individually sound extensions can interact to produce unsound results.