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.