Skip to content

Tutorial

This is the human-first on-ramp to Vow. By the end you will be able to write a Vow program, attach contracts to it, run the verifier, read a counterexample, and fix the program until it is proven correct — the core loop Vow is built around.

What you'll learn

  1. Install & first program — get the build/vowc compiler and compile a "hello, world".
  2. Your first contract — add a requires precondition and see blame semantics in action.
  3. The CEGIS loop — let the verifier find a bug, read the structured counterexample, and fix it.
  4. Loop invariants — prove properties of code that loops.
  5. Using the standard library — pull a verified module into your own project.

Prerequisites

  • A Unix-like environment (Linux or macOS).
  • A Rust toolchain (to build the bootstrap compiler the first time).
  • ESBMC on your PATH for the verification steps.

Once you're comfortable, the Language reference has the full grammar, contract semantics, and CLI details, and the Standard library documents the reusable modules.