Boundary-Only Spec
This tutorial shows a VDD flow where a bodyless abstract spec is used as a
Non-Intersection Spec
This tutorial extends the VDD flow to two functions plus a global
App2 Invariants
This tutorial walks through the app2 suite in test/viper/app2 and focuses on the invariants and proof structure that make the system modular. The flow is VDD: define the contracts first, then refine each operation to satisfy them. Read this alongside actor invariants, modifies clauses, reads clauses, and quantifiers.