Overview

This book is an online resource that teaches how to prove the correctness of your programs written in Go against a formal specification. We use the Gobra verifier, and we exemplify it on multiple examples and exercises.

• If you find errors or have suggestions, please file an issue here.
• If you have any questions about Gobra's features that are not yet addressed in the book, feel free to ask them on Zulip.
• Finally, if you are interested in contributing directly to the project, please refer to our guide for contributors.

Some code blocks are tagged with the following images, to make it clear which code contains errors or verifies:

	Go program does not compile
	Program panics
	Verified by Gobra
	Gobra does not verify the program