In software engineering models are used for many different things. In this paper, we focus on program verification, where we use models to reason about the correctness of systems. There are many different types of program verification techniques which provide different correctness guarantees. We investigate the different types of program verification tools that exist, and present a concise megamodel to distinguish them. We also present a data set of over 350 program verification tools. This data set includes the type of verification tool according to our megamodel, practical information such as input/output format and repository links, and more. The categorisation makes it easier to find similar tools and compare them. We also identify trends for each level in our megamodel based on the categorisation. Our data set can be used by software engineers to enter the world of program verification and find a verification tool based on their needs and wants.