Gobra
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
Go is targeted at high performance applications running in potentially distributed settings and on multicore machines. Hence, Go provides some built-in concurrency primitives, like channel-based communication. Gobra is intended to verify such programs. Gobra is used in the VerifiedSCION and Centre for Cyber Trust projects to verify correctness and security properties of substantial codebases. The Gobra project is open-source and available on external page Github. There is also a external page Zulip organization for discussions related to Gobra.
Links
external page GitHub pages
external page Zulip channel
Gobra versions of the examples and exercises from Rustan Leino's book external page Program Proofs
Project Members
external page Linard Arquint
Nicolas Klose
Andrew Lee
external page João C. Pereira
Peter Müller
Malte Schwerhoff
Publications on Gobra
- F. A. Wolf and L. Arquint and M. Clochard and W. Oortwijn and J. C. Pereira and P. Müller: Gobra: Modular Specification and Verification of Go Programs
In Computer Aided Verification (CAV), 2021. [PDF][BIB][external page Publisher][external page Talk] - F. A. Wolf and L. Arquint and M. Clochard and W. Oortwijn and J. C. Pereira and P. Müller: Gobra: Modular Specification and Verification of Go Programs (extended version)
In arXiv, 2021. [external page arXiv]
Selected Publications using Gobra
- L. Arquint: GCD: Garbled, Corrected, Demonstrandum – Fixing and Proving Go’s Extended GCD Implementation
In 2026 Workshop on Foundations of Computer Security (FCS), 2026. [external page PDF] [external page BIB] [external page arXiv] - L. Arquint, S. Kishor, J. R. Koenig, J. Dodds, D. Kroening, and P. Müller: The Secrets Must Not Flow: Scaling Security Verification to Large Codebases
In 2026 IEEE Symposium on Security and Privacy (SP), 2026. [PDF] [BIB] - C. Cauli, T. Lang, S. Chen, S. Mouelhi, X. Jin, S. Bandopadhyay, X. Chen, Y. Feng, H. Song, L. Tang, Z. Sheng, and A. S. Srinath: Lessons Learned from Incorporating Formal Methods in Huawei Cloud Reliability
In European Conference on Computer Systems (EUROSYS), 2026. [external page Publisher] - J. C. Pereira, T. Klenze, S. Giampietro, M. Limbeck, D. Spiliopoulos, F. A. Wolf, M. Eilers, C. Sprenger, D. Basin, P. Müller, and A. Perrig: Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router
In Computer and Communications Security (CCS), 2025. [PDF] [BIB] [external page Publisher] - L. Arquint, F. A. Wolf, J. Lallemand, R. Sasse, C. Sprenger, S. N. Wiesner, D. Basin, and P. Müller: Sound Verification of Security Protocols: From Design to Interoperable Implementations
In 2023 IEEE Symposium on Security and Privacy (SP), 2023. [PDF] [BIB] [external page Publisher] [external page Talk]
- L. Arquint, M. Schwerhoff, V. Mehta, and P. Müller: A Generic Methodology for the Modular Verification of Security Protocol Implementations
In Computer and Communications Security (CCS), 2023. [PDF] [BIB] [external page Publisher]