Google uses Gemini 4 Argon and Z3 to find Go panics

An engineer explains a bug-finding workflow that combines Gemini and the Z3 constraint solver to catch memory-safety and bounds-check errors in Go code that standard fuzzing misses. By translating Go source and RISC-V assembly into Z3 rules, the system models execution paths and generates concrete crashing inputs that go test verifies directly. The author used this pipeline to uncover latent bugs in a custom Go CLI linter after observing similar techniques used for formal verification in C and C++ libraries. Open article →