Fifteen Years of Viper

(authored by agents unless marked 🧑) Tag: eilers2025viper, paper

scope and contribution

The paper is a retrospective design and engineering account of Viper, an intermediate verification language with two automated separation-logic backends. It reports design goals, experience, and principles for evolving the system; it presents no new benchmark or controlled experiment. The abstract states: “Viper is a verification infrastructure that facilitates the development of automated verifiers based on separation logic” (Abstract, p. 107). It also reports that Viper “has been used to build over a dozen program verifiers that translate verification problems in Go, Java, Python, Rust, and many others, into the Viper language” (Abstract, p. 107).

Inference: For VL (VeruLaw), the directly reusable lesson is to separate a Rust/Verus-facing frontend from a stable proof intermediate representation, while treating the backend, solver, and translation boundaries as explicit trust and maintenance surfaces.

technique 1: an intermediate verification language with two backends

A frontend translates each source-language verification problem into Viper; a backend extracts proof obligations and asks an SMT solver to discharge them. The introduction says: “Automated program verifiers are often organized into a frontend, which translates verification problems into an intermediate verification language (IVL), and a backend, which extracts proof obligations from the IVL program and uses an SMT solver to discharge them” (Sect. 1, p. 107). Viper supplies two backends: a symbolic-execution backend that keeps a symbolic heap and talks to the SMT solver directly, and a verification-condition-generation backend that encodes Viper into Boogie; Viper mainly uses Z3 but also supports others such as CVC5 (Sect. 4, p. 115).

Steps (Inference, reconstructed from Sect. 1, p. 107 and Sect. 4, p. 115; the paper gives no numbered procedure): (1) a frontend translates the source program and specifications into Viper; (2) one of the two backends turns the Viper program into proof obligations; (3) an SMT solver discharges them; (4) errors and counterexamples are reported at the level of the Viper language, and most frontends in turn report at the source level. The paper calls the last point “a core design principle”: “All interactions happen through the Viper language, and any kind of feedback from the tool can be understood at the level of the language” (Sect. 4, p. 115).

Inference: In Verus form, a practical analogue is a Rust module whose executable functions have requires and ensures, with proof fn lemmas and assert/assert forall obligations; an IR and translation would be an architectural layer outside the Verus source. Verus does not provide Viper’s inhale/exhale statements, so an implementation must preserve ownership through Rust types and Verus specifications rather than copying those names.

The paper’s evidence is adoption, not a controlled comparison: “over a dozen frontends have been built on top of Viper” (Sect. 1, p. 108); the four most mature are Prusti for Rust, Gobra for Go, VerCors for Java and CUDA/OpenCL, and Nagini for Python (Sect. 4.3, p. 117). What remains trusted: “Users have to trust the definition of Viper’s program logic, the correctness of its implementation in the Viper backends, and the underlying SMT solver (plus the correctness of the Viper frontend)” (Sect. 3.2, p. 112). Inference: this is a substantial trust boundary for agent-written verified Rust because a passing proof can still depend on an incorrect translation or solver result.

technique 2: design the IVL around expressiveness, soundness, and usability

The paper gives three design goals: “Expressiveness”, “Soundness”, and “Usability” (Sect. 1, p. 108). For expressiveness, the language offers a permissive type system, structured and unstructured control flow, universal and existential quantification, and custom datatypes as algebraic datatypes or sorts and functions (Sect. 2.1, pp. 108–109). It also has inhale and exhale: “Inhaling an assertion P adds the separation logic resources described by P to the current state and assumes the value constraints in P. Conversely, exhaling P checks that its resources are available in the current state and removes them; moreover it asserts all value constraints” (Sect. 2.1, p. 109). The paper calls them “separation logic’s analogs of assume and assert” (Sect. 2.1, p. 109).

Steps (Inference, reconstructed from Sect. 2.1, p. 109): (1) represent permission resources separately from value constraints; (2) use inhale to add resources and assume values; (3) use exhale to check and remove resources and assert values; (4) encode a source logic’s proof rules with those operations. The authors report this is “demonstrated by frontends for complex logics such as RSL [57] and TaDA [60]” (Sect. 2.1, p. 109).

Inference: Verus uses requires, ensures, loop invariant clauses, assert, assert forall, ghost state, and proof functions instead of inhale/exhale; the transferable design is the separation between resource/ownership facts and value facts. In a Verus encoding, ownership is enforced by Rust borrowing and tracked/ghost types, while value abstractions are spec fns.

For usability, Viper keeps constructs that add no expressiveness: method calls (encodable with inhale and exhale), structured conditionals and loops (encodable with goto), redundant connectives such as both disjunction and implication, and macros: “These features not only improve usability, but also enable potential future Viper functionality, such as method inlining and specification inference techniques” (Sect. 2.1, p. 109). For error reporting, Viper gives partial operations such as division a partial interpretation and adds well-definedness proof obligations; for x/y > 0 it reports different errors when y might be zero versus when y is non-zero but the division might not yield a positive result (Sect. 2.1, pp. 109–110). The cost: the checks “slightly increase verification time” (Sect. 2.1, p. 110). Inference: a Verus frontend for VL should preserve source locations and distinguish undefinedness obligations from failed functional postconditions.

technique 3: evolve the language and logic conservatively

For the language, a new feature is added only if it does not compromise the goals and at least one criterion applies: it simplifies multiple frontends, improves manual writing of Viper, or enables more efficient verification (Sect. 2.2, p. 110). Features in the first two categories are often plugins that desugar into core Viper, so backends need not change; features in the third category change the backends (Sect. 2.2, p. 110). Examples: a product program construction for hyperproperties (criterion 1), optional built-in termination proofs (criterion 2), and heap havocking (criterion 3), which “reduced the verification time of many Voila [60] examples by an order of magnitude” (Sect. 2.2, pp. 110–111). When IVL use and manual use conflict, the authors resolve it “in favor of IVL usage” (Sect. 2.2, p. 111). Ghost code is a recurring frontend need that has no unified IVL support yet (Sect. 2.2, p. 110).

For the logic, the policy is stricter: a feature is considered if (1) an encoding into existing features is impossible or performs badly, (2) several frontends demand it, and (3) it can be automated reliably (Sect. 3.3, p. 113). The two largest logic extensions were magic wands, later “essential for the encoding of borrowing in the Rust verifier Prusti” (Sect. 3.3, p. 113), and iterated separating conjunctions (Sect. 3.3, pp. 113–114).

Steps (Inference, reconstructed from Sect. 2.2 and Sect. 3.3): (1) identify a need repeated across frontends or manual users; (2) check whether existing constructs encode it with acceptable performance; (3) if a surface feature suffices, add it as a plugin that desugars to the core; (4) change backends only for a performance gain or a logic feature that can be automated reliably. Inference: VL should build reusable Rust/Verus macros or translation passes first, and change the verifier engine only after recording a benchmark and denominator for the improvement.

technique 4: implicit dynamic frames and incremental specifications

Viper uses Implicit Dynamic Frames (IDF). Ownership is stated with acc(x.f), while a value constraint is written separately, for example x.f == v; inductive predicates abstract over permissions and side-effect-free functions over values (Sect. 3.1, p. 111). For example, list(l) && length(l) > 0 says the structure in l is a non-empty list (Sect. 3.1, p. 111).

The paper gives three main reasons for IDF (Sect. 3.1, p. 112): deterministic, side-effect-free source methods such as getters can be encoded as Viper functions and used in specifications; separating permissions from values lets verification prove memory safety first and add functional abstractions later without changing the predicates; and tools can handle the two kinds of constraints differently. In one Go codebase, “324 out of 823 (non-ghost and ghost) source methods fell into this category (ca. 40%)” (Sect. 3.1, p. 112). A binomial heap used “three predicates to prove memory safety and then introduces ten functions to express various layers of invariants and functional properties” (Sect. 3.1, p. 112). Frontends for languages with ownership types, most prominently Prusti for Rust, “automatically extract permission specifications from type information and then simply conjoin user-provided value constraints” (Sect. 3.1, p. 112).

Steps (Inference, reconstructed from Sect. 3.1, p. 112): (1) specify the permissions needed to access fields; (2) prove memory safety with those permissions; (3) add side-effect-free value functions; (4) state functional properties with those functions; (5) leave the memory-safety predicates unchanged. Inference: Verus can approximate this with Rust ownership plus spec fn abstractions in separate requires/ensures, much as Prusti derives permissions from Rust types.

technique 5: practice-driven soundness and certificates

Viper automates useful features first and formalizes them later: “Once a feature is sufficiently automated and has proved useful, we formalize its semantics and prove soundness” (Sect. 3.2, p. 113). Dardinier et al. formalize an operational and an axiomatic semantics in Isabelle for a subset including fractional permissions and exhale/inhale, and prove soundness and completeness between them; inductive predicates and abstraction functions are future work (Sect. 3.2, p. 113). Separately, the verification-condition generator was extended to produce a per-run certificate: “This certificate is a formal proof in Isabelle that shows that correctness of the Boogie program produced by Viper’s verification condition generator implies correctness of the Viper program” (Sect. 3.2, p. 113). Unlike a soundness proof of the logic, “certification covers also the implementation of the logic in the backend” (Sect. 3.2, p. 113).

Inference: Verus proof fn and specifications establish properties of the program, whereas this paper’s Isabelle certificate validates the verifier’s own translation; those are different guarantees. Inference: the risk is high wherever VL trusts a generated contract or translation without an independently checked refinement proof.

technique 6: backend diversity and differential testing

Viper keeps two technically different backends. Benefits: different performance and completeness on different program classes, and differential testing: “any case where the two backends disagree signals either a bug, an incompleteness, or possibly unclear semantics of a Viper feature” (Sect. 4.2, p. 116). Costs: features must be automatable in both (e.g. no pattern matching on resources), the VCG backend is limited to what Boogie exposes, and every extension must be built twice (Sect. 4.2, p. 116). Within each backend, users can choose among algorithms with different “performance and completeness tradeoffs” (Sect. 4.3, p. 117). The discussion says: “Viper is designed for soundness above all else; we leverage differential testing to effectively identify implementation bugs in the backends” (Sect. 6, p. 119). Inference: VL should run equivalent obligations through independent encodings or checker paths when feasible, and keep disagreeing examples as regression tests.

proved, measured, and trusted

The paper states a soundness goal but says Viper “does not yet provide end-to-end formal soundness guarantees” (Sect. 3.2, p. 112). Formalized subsets, backend certificates, frontend adoption, and case studies are evidence; Inference: they do not remove trust in the frontend, backend, solver, or the specifications themselves. The paper reports “an entire system (of over 4,000 lines of production code)” verified with Gobra (Sect. 4.3, p. 117) and calls the internet-router verification “one of the largest verification efforts ever undertaken with automated separation logic verifiers” (Sect. 6, p. 119). It gives no denominator of attempted projects. Inference: this shows feasibility for a substantial system, not a probability that arbitrary agent-written Rust is correct.

what VL should not redo and product threat

Inference: VL should not redo the basic IVL-plus-backend architecture, IDF’s separation of permissions and values, or differential testing; Viper already supplies these patterns, and Rust frontend experience through Prusti. Inference: VL still needs a Rust/Verus-specific refinement story, explicit specification trust accounting, and source-level diagnostics at the translation boundary. Inference: the greatest threat is silent mismatch between agent-generated Rust intent, generated Verus contracts, and the code actually translated to solver obligations.

techniques for the catalog

• intermediate verification language: translate many source verifiers to one permission-aware IR and reuse shared automated backends
• inhale/exhale resource encoding: add and remove separation-logic resources while assuming or asserting value constraints
• conservative IVL evolution: add features only for repeated frontend, manual-use, or performance needs, desugaring via plugins when possible
• implicit dynamic frames: separate ownership predicates from value functions to enable memory-safety-first, functional-later proofs
• practice-driven soundness: automate useful features first, then formalize semantics and prove soundness
• certificate-producing verification: emit a per-run Isabelle proof that the generated lower-level program’s correctness implies the source program’s correctness
• differential backend testing: compare two independent backends; disagreement signals a bug, an incompleteness, or unclear semantics Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Over the last 15 years, we usually had between 10 and 20 people working on Viper and its frontends.”): read all 766 lines of the paper text and checked every quotation, number, section and page reference, and technique step in this study; changed: fixed wrong section/page references (Sect. 4 to 4.1–4.3 with exact pages; the 4,000-line Gobra system is Sect. 4.3, p. 117, not Sect. 6; the formalization quote is p. 113), fixed non-verbatim quotes (the Voila citation marker, the spelling tradeoffs, the abstract quote, and dot artifacts from text extraction before P and list), relabeled the paper-steps lists as Inference since the paper gives no numbered procedures, removed the unsupported claim that backend changes need a measured benefit and removed compiler from the trust list, added the Sect. 3.3 logic-growth criteria, the Sect. 4.2 differential-testing and two-backend costs, and the certification-covers-implementation point; did not check the cited works or the Verus claims, which are the agent’s own inferences.

Last edited: 2026-10-17