Language reference

Compact lookup for contract syntax and semantics. For a guided introduction, start with The CppVerify Book; for backends and cpp-verify flags, see Chapter 17 — Backends, modular calls, and debugging and Commands and flags.

• Contract syntax
• Contract expressions
• Functions and loops
• Ghost, spec, and proofs
• Structs and type invariants
• Pointers
• Integers
• Commands and flags
• Supported C++ subset