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.

Always cap memory

Every command below is prefixed with ulimit -v 2000000. The compiler and the binaries it produces can otherwise consume all system memory. Make it a habit.

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