Kripke proves bugs.

A prover for the code your agents write — with a reproducible proof: the exact interleaving, the access path.

Reported · accepted · fixed

Found a data race in an 11K-star, security-first service mesh — they shipped the fix.

✓ ACCEPTED & FIXED
linkerd/linkerd2

A data race on a shared field — written by one goroutine, read by another, no lock. Maintainers accepted it and merged the fix.

issue #15096  ·  fix #15150
✗ NO FALSE ALARM
hatchet-dev/hatchet

A look-alike unsynchronized write — but reachable from only one goroutine, so no race exists. Kripke didn't flag it. The right call.

issue #3413

Real bug, proven. Non-bug, skipped. That's the difference between a prover and a linter.

A finding is a proof, not a comment.

DATA RACE RemoteClusterServiceWatcher.gatewayAlive (linkerd #15096) multicluster/service-mirror/cluster_watcher.go 1471 go func() { // repair-ticker goroutine 1480 rcsw.gatewayAlive = alive ← write, no lock }() 1459 go rcsw.processEvents(ctx) // reader goroutine 1789 if !rcsw.gatewayAlive { ... } ← concurrent read → two goroutines, one unsynchronized field. the read can observe a stale write. fix #15150: bool → atomic.Bool
Real file, real lines, a reproducible interleaving — not "this looks risky."

Go's own race detector agrees — but only once a test happens to hit the path:

$ go test -race ./multicluster/service-mirror # linkerd2 @ f37b69d2 WARNING: DATA RACE Read at 0x00c0003b8410 by goroutine 63: (*RemoteClusterServiceWatcher).updateReadiness() cluster_watcher.go:1789 ← if !rcsw.gatewayAlive Previous write at 0x00c0003b8410 by goroutine 64: concurrent write to rcsw.gatewayAlive (repair-ticker · cluster_watcher.go:1480) --- FAIL: race detected
The runtime catch — if a test gets lucky. Kripke proves the same race from the source, deterministically, with no test to write.

The Linkerd race is one of four bug classes Kripke proves:

Concurrency

Data races, deadlocks, goroutine leaks, unguarded shared state.

Authorization

IDOR, privilege escalation, missing owner- and tenant-scoping.

Data exfiltration

Secrets and PII that reach a response or cross a boundary.

Consistency & contracts

Illegal state transitions, broken invariants, cross-service drift.