Getting Started

Start with a short example, then use the guide to learn how to express your own verification problems in HeyVL.

1. Install Caesar

   Use the VS Code extension or the command-line verifier.

2. Verify the First Example

   A short walkthrough of the geometric loop and its expected runtime bound.

3. Read the Guide to HeyVL

   Specifications, invariants, types, functions, and verification statements in detail.

4. Explore More Examples

   Worked examples of probability bounds, termination proofs, and model checking.