Gobra is a program verifier for Go programs. It allows programmers to specify their code with contracts and it checks whether the code meets its specification.
It is open-source and available on Github (https://github.com/viperproject/gobra). There is also a VS-Code plugin that allows users to interactively verify their Go programs (https://marketplace.visualstudio.com/items?itemName=viper-admin.gobra-ide).