GoProve

A static analysis tool for Go that uses abstract interpretation to mathematically prove properties about your code — or tell you exactly where it can't.

When GoProve says a bug exists, it's guaranteed. When it says your code is safe, it's proven. When it's unsure, it tells you honestly.

• Why GoProve?
• Install
• Usage
• What It Detects
• How It Works
• Three-Color Model
• Comparison with Other Tools
• Soundness Details
• Real-World Results
• CI Integration
• Roadmap
• Contributing
• Credits
• License

$ goprove ./...
 Error: billing/charge.go:47 nil dereference of nil pointer — value is always nil
 Warning: handler/click.go:89 possible nil dereference of config — add a nil check before use

 Summary: 1 bugs, 1 warnings.

Go's type system prevents many classes of bugs at compile time, but three categories consistently escape into production: nil pointer dereferences, division by zero, and integer overflow. These are runtime panics — they depend on values, not types, and no amount of type safety prevents them.

Existing Go tools approach this through pattern matching (go vet, staticcheck) or constraint inference (NilAway). These are useful but limited — they can miss real bugs and flag correct code, with no formal guarantee either way.

GoProve takes a different approach. It uses abstract interpretation (Cousot & Cousot, 1977) — a mathematically rigorous framework for computing sound approximations of program behavior. The same theoretical foundation is used in tools like Polyspace (automotive/aerospace) and Astrée (Airbus flight controllers). GoProve applies this to production Go code.

Formal verification has traditionally been reserved for safety-critical systems — flight controllers, medical devices, nuclear reactors. The assumption is that ordinary software doesn't need mathematical proof.

But consider what "ordinary" Go backends actually do: process payments, calculate attribution, route vehicles, serve millions of requests. A nil panic in these systems doesn't kill anyone — but it loses money, corrupts data, breaks SLAs, and pages engineers at 3am. The cost of these bugs is real and measurable.

The barrier to proving wasn't that backend code didn't need it — it was that proving tools required annotations, specifications, or PhDs to operate. Abstract interpretation removes that barrier. It works on unmodified source code, runs in seconds, and gives you the same mathematical guarantee that Airbus gets for flight software: if the tool says it's safe, it's safe.

The question isn't "is my code safety-critical enough for proving?" It's "why wouldn't I want a mathematical guarantee that my nil checks actually work?"

Engineers building Go backends for:

• Banking / payment systems — where a nil panic in a transaction handler means lost money
• Ad tech / attribution — where a silent integer overflow in billing means wrong charges
• Ride-hailing / logistics — where a division by zero in routing means a 3am page
• Any team tired of runtime panics that their linter didn't catch

• Zero annotations. No special comments, contracts, or spec files. The tool infers everything from your code.
• Sound for bugs. When GoProve says Bug, abstract interpretation has proven it across all execution paths. No false negatives for proven bugs.
• Honest about limits. The three-color model (Bug/Warning/Safe) is transparent about what the analysis can and cannot prove. Completeness is deliberately sacrificed — the analysis may warn about code that's actually safe, in exchange for never missing a proven bug.
• Incremental value. Each analysis domain delivers a usable tool on its own. You don't need the full suite to get value.

• Not a replacement for testing — it proves properties about all inputs, but only for the patterns it tracks.
• Not a certification tool — it's designed for production engineers, not safety certification (IEC 62304, DO-178C).
• Not an annotation-based verifier — that's Gobra's territory.
• Not a theorem prover — that's coq-of-go's territory.
• Not a runtime analyzer — that's the race detector's territory.

GoProve offers two modes depending on your needs:

go install github.com/ahmedaabouzied/goprove/cmd/goprove@latest

The CLI analyzes your entire program at once. It uses whole-program parameter tracking with fixed-point iteration — if all callers of a function pass non-nil after nil guards, the parameter is proven non-nil. This is the most accurate mode with the fewest false positives.

go install github.com/ahmedaabouzied/goprove/cmd/goprove-lint@latest

The go/analysis integration works with golangci-lint, go vet, and any tool that supports the framework. It analyzes one package at a time, so whole-program parameter tracking is not available — you may see additional warnings on parameters that the CLI would prove safe.

Our recommendation: use both. Run goprove-lint locally for quick feedback during development. Run the GitHub Action in CI for the full whole-program proof.

# Analyze a single package
goprove ./pkg/server

# Analyze all packages (recommended)
goprove ./...

# Use in CI — exits with code 1 if any findings
goprove ./... || exit 1

go vet -vettool=$(which goprove-lint) ./...

Add to your .golangci.yml:

linters:
  enable:
    - goprove

(Plugin registration with golangci-lint is coming soon.)

GoProve tracks nil state through your entire program:

func process(config *Config) {
    if config == nil {
        return
    }
    helper(config) // GoProve knows config is non-nil here
}

func helper(config *Config) {
    config.Validate() // No warning — all callers pass non-nil
}

• Proven nil derefs (var p *int; *p) are flagged as Bug
• Unchecked params are flagged as Warning — unless all callers pass non-nil
• Nil checks (if p != nil), early returns (if p == nil { return }), new(), make(), &x are all tracked
• Field reloads after nil checks (if o.Field != nil { o.Field.Use() }) are proven safe
• Interface method calls (s.Method()) on nil interfaces are detected
• Global variable nil checks propagate across subsequent reads

func safe(x, y int) int {
    if y != 0 {
        return x / y // GoProve: safe
    }
    return 0
}

func unsafe(x int) int {
    zero := 0
    return x / zero // GoProve: Bug — division by zero
}

func narrow(x int16) int8 {
    if x < 100 && x > -100 {
        return int8(x) // GoProve: safe — x fits in int8
    }
    return 0
}

• Arithmetic overflow on int8, int16, int32
• Narrowing conversion overflow (int16 → int8)
• Negation overflow (-math.MinInt8)

GoProve builds on Go's SSA (Static Single Assignment) intermediate representation and runs abstract interpretation with two domains:

1. Interval domain [lo, hi] per integer variable — proves division and overflow safety
2. Nil state domain {DefinitelyNil, DefinitelyNotNil, MaybeNil} per pointer — proves nil safety

Key techniques:

• Address-based memory model — tracks nil state per memory address, not per SSA register. Two loads from the same field share nil state.
• Whole-program parameter analysis — fixed-point iteration computes what callers actually pass to each parameter. If all callers pass non-nil after nil guards, the parameter is proven non-nil.
• Interprocedural return summaries — callee return nil/interval state is tracked via CHA call graph resolution.
• Branch refinement — if p != nil, if y != 0, <, <=, >, >= narrow abstract state per branch.
• Worklist with widening — guarantees termination on loops while maintaining soundness.

GoProve uses an honest three-color classification:

GoProve's advantage: when it says Bug, it's proven. When it says Safe, it's mathematically guaranteed. No other open-source Go tool offers this.

NilAway's advantage: faster, scales to massive codebases, integrates with golangci-lint. But it can produce both false positives and false negatives.

What "proven" means:

• Bug findings are sound: abstract interpretation has proven the bug exists across all execution paths.
• Safe findings are sound for tracked patterns: if GoProve produces no finding, the operation is safe for the patterns it analyzes.

What the tool does NOT cover:

• Concurrency: no tracking of values across goroutines or channels.
• Reflection: reflect.Call arguments are invisible to static analysis.
• Some unsafe.Pointer cast chains.
• CGo: C function calls are outside Go's type system.

Intentional pragmatic choices:

• Method receivers are assumed non-nil (eliminates noise, misses (*T)(nil).Method()).
• Slice indexing only flags proven nil slices, not possible nil (deferred to future bounds checker).

Patterns correctly handled:

• v, ok := m[key]; if ok && v != nil { *v } — map ok pattern
• v, ok := x.(T); if ok { v.Do() } — type assertion ok pattern
• time.NewTimer(), bytes.NewBuffer() — stdlib return values (via interprocedural analysis)
• if x.F != nil { x.F.Use() } — field reload after nil check (via address model)

Use the GoProve Action for full whole-program proof:

- uses: ahmedaabouzied/goprove-action@v1
  with:
    path: ./...

- name: Run GoProve
  run: |
    go install github.com/ahmedaabouzied/goprove/cmd/goprove@latest
    goprove ./...

GoProve exits with code 1 when findings are detected.

Contributions welcome. The codebase has 296 test functions with 99.5% statement coverage.

git clone https://github.com/ahmedaabouzied/goprove
cd goprove
go test ./...

Gopher mascot created with gopherize.me by Mat Ryer and Ashley McNamara, based on original Go gopher by Renee French.

MIT