It is possible to load the problem sumAndMax.dfy and show its project contents. It is possible to see all PVCs for sumAndMax and to select each of the PVC. For each chosen PVC it is possible to perform the proof either using Z3 or using user defined rules. It is possible to use the scripting language as well as point and click for interacting with the prover and performing proof steps.
It is possible to navigate through the proofs and view each proof node.