vgo - verifiable go¶
Verifiable go or vgo for short is a subset of the go programming language introduced by Google that has been extended so that the programmer can use a temporal logic (CTL) to express assumptions and guarantees directly within the source code.
The tool is invoked like the go build system itself. It verifies that the code has the desired properties and produces a compiled library or aborts with an appropriate error message.
This has a number of advantages:
- The tool fits very well into the usual development practices.
- Verification failures prevent compilation of the code.
- The very same code that has been model checked is compiled, there is no need to translate the code to an intermediate language.
The produced library is a standard go module that other code written in go can use. This makes it possible to divide the code into parts that can be verified (like the core logic) and parts that is not easily verifiable (any kind of I/O, user interfaces, etc.).
The goals of vgo are
- to provide an implementation of a modular model checking framework for further experimentation and
- to provide a tool capable of checking properties of programs written in a modern imperative programming language while focusing on usability aspects, i.e. to provide a tool that can be used by programmers without intimate knowledge of the theoretical background of model checking.