Skip to main content


HeyVL is a verification language similar to Viper and Boogie. The main innovation is that it supports quantitative reasoning via its constructs inspired by Gรถdel logic. Refer to our publications for details on the theory.

A HeyVL file consists of a sequence of declarations: procedure and domain declarations.

Use the source, Lukeโ€‹

We do not formally describe the syntax of HeyVL in this documentation. You can find a more formal definition in the src/front/parser/grammar.lalrpop file that specifies the syntax used to generate Caesar's parser. It is written in the LALRPOP language.


The pgcl/examples-heyvl directory contains the machine-translated HeyVL code for our pGCL examples. Note that they are just sequences of HeyVL statements without wrapping procedure declarations. Refer to the page on the pGCL frontend for more information.

Caesar's integration tests in tests/ can also serve as a reference. Refer to the development guide for more information about these tests.