Deploy Gobra to Europe — Felix Wolf 🇩🇪 + ETH Zurich (2021), the Viper-Based Formal Verifier for Go Programs Used in Kubernetes, Docker, and Cloud-Native Infrastructure, on EU Infrastructure in 2026

Go has become the language of cloud-native infrastructure. Kubernetes, Docker, containerd, Prometheus, etcd, CoreDNS, Helm, Terraform, and CockroachDB are all written in Go. The cloud-native stack that runs modern European digital infrastructure — financial services, healthcare IT, government platforms, telecom — depends on Go programs at its core. When these programs have bugs, the consequences cascade through the systems they underpin.

Gobra is a formal verifier for Go programs, developed at ETH Zurich 🇨🇭 (Eidgenössische Technische Hochschule) by Felix Wolf, Malte Schwerhoff, and Peter Müller, first published at CAV 2021 (Computer Aided Verification). Gobra takes Go source code annotated with preconditions, postconditions, loop invariants, and memory access specifications, translates it to the Viper intermediate verification language — also developed at ETH Zurich — and discharges proof obligations to Z3 via the Viper Silicon backend. The result is either a machine-checked correctness proof or a counterexample that pinpoints the specification violation.

Gobra is part of the Viper ecosystem: a family of European verifiers sharing a common verification infrastructure, all from ETH Zurich's Programming Methodology group. Prusti (Rust) and Nagini (Python) apply the same Viper backend to their respective languages. Together they cover the three dominant languages of modern systems programming — and all three are EU/Swiss origin.

Viper: Shared Infrastructure for Three Languages

Gobra's verification architecture is identical in structure to Prusti's: Go source → Viper intermediate representation → Silicon symbolic execution → Z3 SMT queries. The core insight behind the Viper ecosystem is that permission-based heap reasoning (Implicit Dynamic Frames) provides a common model for memory access that fits Go's pointer semantics, Rust's borrow checker semantics, and Python's reference semantics alike.

In Viper's permission model, each heap location carries an access permission (acc(x.field, p)) where p is a fraction from 0 to 1. Write permission corresponds to p = 1 — no other thread or alias holds any permission to this location. Read permission corresponds to any p > 0 — multiple readers may hold fractional permissions that sum to at most 1. This model directly encodes Go's pointer aliasing: a goroutine holding a *T with full permission is the sole writer; multiple goroutines holding fractional read permissions may read concurrently without data races.

The Viper ecosystem shares a single verified backend (Silicon + Z3) across three front-end languages:

Gobra's Specification Language

Gobra specifications are Go comments prefixed with //@ . They appear in Go source files and are invisible to the standard Go compiler — they exist only when Gobra processes the file.

Preconditions and Postconditions

package main

// @ requires n >= 0
// @ ensures result >= 0
// @ ensures result * result <= n
// @ ensures (result+1) * (result+1) > n
func IntSqrt(n int) (result int) {
    result = 0
    for result*result <= n {
        // @ invariant result >= 0
        // @ invariant result * result <= n
        result++
    }
    result--
    return
}

The specification states: given a non-negative input, IntSqrt returns the largest integer whose square does not exceed n — a complete functional correctness proof for integer square root. Gobra verifies that this property holds for all non-negative inputs, and that the loop terminates.

Memory Safety and Heap Access

Go programs use pointers and structs stored on the heap. Gobra's permission logic tracks which goroutine may access which heap locations:

// @ requires acc(x, 1/1)   // exclusive write access to *x
// @ ensures  acc(x, 1/1)
// @ ensures  *x == old(*x) + 1
func Increment(x *int) {
    *x = *x + 1
}

// @ requires acc(x, 1/2) && acc(y, 1/2)   // read access to both
// @ ensures  acc(x, 1/2) && acc(y, 1/2)
// @ ensures  result == *x + *y
func Sum(x, y *int) (result int) {
    return *x + *y
}

acc(x, 1/1) is exclusive write permission — no other goroutine can read or write *x while this function holds it. acc(x, 1/2) is a fractional read permission — multiple goroutines may hold 1/2 each (summing to 1), reading concurrently without races.

Struct Invariants and Methods

type BoundedQueue struct {
    items []int
    max   int
}

// Predicate capturing the struct's internal invariant
// @ pred (q *BoundedQueue) Inv() {
// @     acc(q) &&
// @     acc(q.items) &&
// @     q.max > 0 &&
// @     len(q.items) <= q.max
// @ }

// @ requires acc(q.Inv(), 1/1)
// @ ensures  acc(q.Inv(), 1/1)
// @ ensures  len(q.items) < q.max
// @ ensures  !full
func (q *BoundedQueue) IsFull() (full bool) {
    // @ unfold acc(q.Inv(), 1/1)
    full = len(q.items) >= q.max
    // @ fold acc(q.Inv(), 1/1)
    return
}

// @ requires acc(q.Inv(), 1/1)
// @ requires !q.IsFull()
// @ ensures  acc(q.Inv(), 1/1)
// @ ensures  len(q.items) == old(len(q.items)) + 1
func (q *BoundedQueue) Enqueue(item int) {
    // @ unfold acc(q.Inv(), 1/1)
    q.items = append(q.items, item)
    // @ fold acc(q.Inv(), 1/1)
}

Gobra's predicates encapsulate heap access permissions together with logical invariants. The fold/unfold operations correspond to packing and unpacking the predicate — making the heap shape explicit at key points while hiding it behind the predicate name elsewhere.

Quantifiers and Sequence Properties

// @ ensures forall i int :: { s[i] } 0 <= i && i < len(s) ==> s[i] >= 0
func AbsAll(s []int) []int {
    result := make([]int, len(s))
    // @ invariant 0 <= j && j <= len(s)
    // @ invariant forall i int :: { result[i] } 0 <= i && i < j ==> result[i] >= 0
    for j, v := range s {
        if v < 0 {
            result[j] = -v
        } else {
            result[j] = v
        }
    }
    return result
}

// Verified binary search
// @ requires forall i, j int :: 0 <= i && i < j && j < len(arr) ==> arr[i] <= arr[j]
// @ ensures result >= 0 ==> arr[result] == target
// @ ensures result < 0 ==> forall i int :: 0 <= i && i < len(arr) ==> arr[i] != target
func BinarySearch(arr []int, target int) (result int) {
    lo, hi := 0, len(arr)
    // @ invariant 0 <= lo && lo <= hi && hi <= len(arr)
    // @ invariant forall i int :: 0 <= i && i < lo ==> arr[i] < target
    // @ invariant forall i int :: hi <= i && i < len(arr) ==> arr[i] > target
    for lo < hi {
        mid := lo + (hi-lo)/2
        switch {
        case arr[mid] == target:
            return mid
        case arr[mid] < target:
            lo = mid + 1
        default:
            hi = mid
        }
    }
    return -1
}

Goroutine and Channel Verification

Go's concurrency model — goroutines communicating over typed channels — is central to cloud-native infrastructure. A miscommunication between goroutines (deadlock, data race, wrong message type) can bring down a distributed system. Gobra verifies goroutine interactions by tracking permission transfer through channels.

// Channel-based producer/consumer with verified no data race
// @ requires acc(data, 1/1)   // exclusive ownership before send
func Producer(ch chan<- *int, data *int) {
    // Sending through ch transfers permission over *data to the receiver
    // @ send acc(data, 1/1)   // permission annotation on channel send
    ch <- data
    // After send: no permission to *data remains here
}

// @ requires true
// @ ensures  acc(data, 1/1) && *data >= 0   // received ownership + postcondition
func Consumer(ch <-chan *int) (data *int) {
    // @ receive acc(data, 1/1)   // channel receive transfers permission
    data = <-ch
    if *data < 0 {
        *data = 0
    }
    return
}

Gobra's channel annotations declare what permissions are transferred when a value is sent or received. This prevents the most common Go concurrency bugs: sending a pointer and then continuing to write through it (creating a data race), or receiving a pointer and assuming it is exclusively owned when the sender kept a reference.

For mutex-based concurrency — common in infrastructure code:

import "sync"

type SafeCounter struct {
    mu    sync.Mutex
    count int
}

// @ pred (c *SafeCounter) Inv() {
// @     acc(c.mu) && acc(c.count) && c.count >= 0
// @ }

// @ requires acc(c.Inv(), 1/1)
// @ ensures  acc(c.Inv(), 1/1)
func (c *SafeCounter) Increment() {
    // @ unfold acc(c.Inv(), 1/1)
    c.mu.Lock()
    // Mutex locked: exclusive access to count
    c.count++
    c.mu.Unlock()
    // @ fold acc(c.Inv(), 1/1)
}

// @ requires acc(c.Inv(), 1/2)   // shared read access
// @ ensures  acc(c.Inv(), 1/2)
// @ ensures  result >= 0
func (c *SafeCounter) Value() (result int) {
    // @ unfold acc(c.Inv(), 1/2)
    c.mu.Lock()
    result = c.count
    c.mu.Unlock()
    // @ fold acc(c.Inv(), 1/2)
    return
}

Running Gobra

Installation

# Prerequisites: Java 11+ (for Viper Silicon backend)
java --version   # must be 11+

# Download Gobra JAR (latest release from ETH Zurich GitHub)
curl -L -o gobra.jar \
  https://github.com/viperproject/gobra/releases/latest/download/gobra.jar

# Verify
java -jar gobra.jar --version
# Gobra 1.x (Viper Silicon / Z3)

# VS Code: install "Gobra" extension (viperproject.gobra)
# Provides inline verification with green/red annotations

Verifying a Go File

# Verify a single Go file
java -jar gobra.jar --input pkg/queue/queue.go

# Verify a package directory
java -jar gobra.jar --projectRoot . --packages ./pkg/queue

# Verbose output with proof details
java -jar gobra.jar --input pkg/queue/queue.go --debug

# Expected output for correct specifications:
# Verifying BoundedQueue.Enqueue ... verified [1.3s]
# Verifying BoundedQueue.IsFull  ... verified [0.8s]
# Verifying BinarySearch         ... verified [2.1s]
# Verification successful.

# Output for specification violation:
# Verifying BinarySearch         ... FAILED [1.1s]
# ERROR: postcondition might not hold
# At: pkg/queue/search.go:42: arr[result] == target
# Counterexample: arr=[1,3,5], target=4, result=-1 → arr[-1] out of bounds

Integration with Go Modules

Gobra understands Go module structure and can verify packages in dependency order:

# go.mod
module eu-service/core

go 1.22

require (
    github.com/prometheus/client_golang v1.19.0
)

# Verify the core module
java -jar gobra.jar \
    --projectRoot . \
    --packages ./internal/... \
    --timeout 120s

CI/CD Integration

# .github/workflows/verify.yml (or internal GitLab CI)
name: Gobra Formal Verification

on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-22.04
    steps:
      - uses: actions/checkout@v4

      - name: Install Java 17
        uses: actions/setup-java@v4
        with:
          distribution: temurin
          java-version: 17

      - name: Download Gobra
        run: |
          curl -L -o gobra.jar \
            https://github.com/viperproject/gobra/releases/latest/download/gobra.jar

      - name: Run Gobra Verification
        run: |
          java -jar gobra.jar \
            --projectRoot . \
            --packages ./pkg/... \
            --timeout 300s
        # Exits non-zero if any specification is violated — blocks merge

Deploy Go with Gobra Verification on sota.io

FROM eclipse-temurin:17-jre AS gobra-verify

# Download Gobra
RUN curl -L -o /usr/local/bin/gobra.jar \
    https://github.com/viperproject/gobra/releases/latest/download/gobra.jar

FROM golang:1.22-bookworm AS verify

COPY --from=gobra-verify /usr/local/bin/gobra.jar /usr/local/bin/gobra.jar
COPY --from=gobra-verify /opt/java/openjdk /opt/java/openjdk
ENV JAVA_HOME=/opt/java/openjdk PATH="${JAVA_HOME}/bin:${PATH}"

WORKDIR /service

COPY go.mod go.sum ./
RUN go mod download

COPY . .

# Formal verification gate: fails build if any Gobra spec is violated
RUN java -jar /usr/local/bin/gobra.jar \
    --projectRoot . \
    --packages ./internal/... \
    --timeout 120s

FROM golang:1.22-bookworm AS build
WORKDIR /service
COPY --from=verify /service/ .
RUN CGO_ENABLED=0 GOOS=linux go build -o /server ./cmd/server/

FROM gcr.io/distroless/static-debian12:nonroot
COPY --from=build /server /server
EXPOSE 8080
ENTRYPOINT ["/server"]

# Deploy verified Go service to EU
sota init eu-verified-go-api
sota deploy

# Output:
# Running Gobra formal verification (Viper Silicon / Z3)...
# Verified: internal/queue/queue.go [4 functions, 8.2s]
# Verified: internal/auth/validator.go [6 functions, 11.4s]
# All specifications verified.
# Building Go binary...
# Deploying to Hetzner Germany (eu-central)...
# Service running at https://eu-verified-go-api.sota.io

sota.io manages the JVM runtime (required for Viper Silicon), the Go toolchain, and Go module caching — so Gobra verification runs in CI without manual infrastructure configuration. The free tier (512 MB) supports Gobra verification of Go packages up to ~10,000 LOC. Larger services (Kubernetes controllers, distributed databases) benefit from the standard tier (2 GB) for Z3 memory headroom during complex verification.

The Viper Ecosystem: EU Formal Verification Across Languages

Gobra's significance extends beyond Go. It demonstrates that the Viper infrastructure — built at ETH Zurich over a decade — scales to production cloud-native languages. The three Viper front-ends now cover the principal languages of EU digital infrastructure:

Go (Gobra, ETH Zurich 🇨🇭): Kubernetes, Docker, cloud-native control planes, service meshes, observability platforms. EU organisations running Kubernetes clusters benefit from formally verified controllers and operators.

Rust (Prusti, ETH Zurich 🇨🇭): Safety-critical embedded systems, automotive (ISO 26262), aerospace (DO-178C), medical devices (IEC 62304), railway (EN 50128). EU manufacturers transitioning to Rust from C for memory safety can add formal verification.

Python (Nagini, ETH Zurich 🇨🇭): Data science, AI model serving, scientific computing. EU AI Act Art. 9 requires systematic verification of AI systems — Nagini brings Viper verification to Python ML codebases.

The three front-ends share the Silicon/Z3 backend and the permission logic model. Engineers who learn Gobra's annotation style will recognise Prusti's and Nagini's immediately — the concepts are isomorphic, only the surface syntax differs.

ETH Zurich and the European Research Area

ETH Zurich (Eidgenössische Technische Hochschule Zürich, founded 1855) is Switzerland's federal engineering university — not EU-member-state, but deeply integrated into the European Research Area:

• Horizon Europe: ETH Zurich participates as an associated country institution (Switzerland-EU bilateral research agreements post-2021)
• SNSF (Swiss National Science Foundation): primary funder of the Viper project, Gobra development, and Prusti research
• Marie Curie fellowships: ETH hosts EU doctoral and postdoctoral researchers; Felix Wolf completed PhD research at ETH Zurich
• COST Actions: ETH contributes to EU-coordinated research networks in programming languages and formal methods

The Gobra and Viper projects are Apache 2.0 licensed and hosted on GitHub under the viperproject organisation. Development is led by ETH Zurich's Programming Methodology group (Prof. Peter Müller), with contributions from researchers across EU institutions.

For data sovereignty: ETH Zurich is Swiss, not subject to the US Cloud Act. Running Gobra verification pipelines on EU or Swiss infrastructure keeps verification artefacts (proof certificates, counterexamples, annotated source) outside US jurisdiction. Swiss data protection law (revDSG, 2023) is recognised by the European Commission as providing equivalent protection to GDPR.

EU Regulatory Context

EU AI Act (Art. 9) — High-Risk AI Systems

EU AI Act Art. 9 requires high-risk AI systems to implement a risk management system including testing, evaluation, and validation procedures. A Go service that implements an AI inference pipeline — annotated with Gobra specifications and verified correct — provides machine-readable proof artefacts that satisfy Art. 9(4)(b)'s requirement for documented testing evidence. Gobra's Silicon backend generates a verification trace that can be included in the technical documentation required by Art. 11.

Cyber Resilience Act (CRA, 2027)

The CRA requires manufacturers of products with digital elements to implement security-by-design. For Go services, this means: no out-of-bounds accesses, no nil dereferences, no data races, no logic errors in authentication and authorisation paths. Gobra can verify all four. A Gobra-verified Go service with //@ requires annotations on security-sensitive functions provides the CRA's required documented evidence of security testing.

NIS2 Directive (Critical Infrastructure)

Go powers much of the infrastructure covered by NIS2's "essential entities" scope: DNS operators (CoreDNS), cloud service providers (Kubernetes-based), digital infrastructure operators (Prometheus monitoring). NIS2 Art. 21 requires appropriate cybersecurity risk management measures. Formal verification of the Go components that implement these services demonstrates due diligence proportionate to the risk.

GDPR Art. 25 — Privacy by Design

Gobra's //@ requires annotations on data access functions can encode GDPR data processing lawfulness constraints. A function with //@ requires user.ConsentGiven cannot be called without consent — the constraint is enforced by the verifier before any runtime execution occurs. This embeds GDPR Art. 6 (lawfulness of processing) into the formal proof structure.

IEC 62443 (Industrial Cybersecurity) and EN 50128 (Railway)

Cloud-native architectures are increasingly used in industrial control systems. Go services acting as Kubernetes operators for SCADA systems, or as microservices in EN 50128 SIL-rated railway platforms, benefit from Gobra verification of their control logic. The Gobra proof certificates serve as the formal evidence required by these standards' software safety requirements.

See Also

• Deploy Prusti to Europe → — Viper-based Rust verifier (ETH Zurich 🇨🇭): same Viper/Silicon/Z3 backend, IDF permissions, CRA 2027 angle
• Deploy Nagini to Europe → — Viper-based Python verifier (ETH Zurich 🇨🇭): Python AI/ML pipelines, EU AI Act Art. 9 compliance
• Deploy Viper to Europe → — Permission-based IVL (ETH Zurich 🇨🇭): the shared Silver IL backend Gobra targets
• Deploy Creusot to Europe → — EU-native Rust verifier (INRIA Saclay 🇫🇷): WhyML/Alt-Ergo, prophecy variables, 100% French EU stack
• Deploy VeriFast to Europe → — Separation logic verifier for C/Java (KU Leuven 🇧🇪): the conceptual predecessor to Viper IDF