Isabelle/UTP allows us to model simple imperative programs making use of all the data structures available in the HOL library. We can annotate programs with invariants and variants to support verification. This is provided by the ITree_VCG session, and by importing "ITree_VCG.ITree_VCG".

We can specify a Hoare triple (partial or total correctness), and use the vcg method to generate a set of verification conditions (VCs). The VCs can often be discharged automatically using automated theorem provers with sledgehammer. For complex VCs, we can use Isar to manage the individual verification tasks.