Catch Go bugs that fuzzing misses with Gemini and a constraint solver

A Google engineer's pipeline pairing Gemini 4 Argon with the Z3 constraint solver caught all three bugs deliberately planted in skill-lint's test parsers and found three additional latent bugs in skill-lint, a Go CLI that validates SKILL.md files for Google's agent skills program, which now holds 175 agent skills. The workflow compiles target functions with GOOS=linux GOARCH=riscv64 and -gcflags="-S -d=ssa/check_bce/debug=1" to surface surviving runtime.panicBounds traps, then has Gemini 4 Argon translate each trap's path into Z3 rules that synthesize concrete Go reproducers, which go test runs directly. The author reports that go test -fuzz missed two of the crashes and describes a one-line change that fixes it.

I help lead Google's agent skills program https://github.com/google/skills , currently with 175 agent skills that supplement community collections like go-skills https://github.com/spf13/go-skills . To keep that many skill files consistent, I wrote skill-lint, a standalone Go https://go.dev/?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 CLI that checks SKILL.md files and applies LLM-generated line edits before they ship. Even with skill-lint's own unit and fuzz test suite, a small slice or line-number mistake inside its Markdown parsers or edit applier can sit dormant until an unusual file or edit range triggers a runtime panic in the linter. In Go, every slice or index operation that can panic at runtime compiles down to an explicit bounds-check trap in machine code, after the compiler's optimizer strips out the checks it can already rule out. To hunt for crashes, I compiled key functions from my code to see which panic traps survived optimization, and Gemini 4 Argon https://ai.google.dev/gemini-api/docs/models/gemini-4-argon?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 translated the path to each trap into rules for the Z3 constraint solver https://github.com/Z3Prover/z3 . An LLM-written solver model isn't a sound proof system, but it gives the agent an independent way to reason about control flow and synthesize concrete Go reproducers, and every crash it finds is real because go test runs the offending bytes directly. That workflow caught all three bugs I planted in test parsers and turned up three latent bugs in skill-lint. In this post, I'll walk through how the Gemini and Z3 pipeline works, why go test -fuzz https://go.dev/security/fuzz/?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 missed two of those crashes and the one-line change that fixes it , and where this approach fits in a day-to-day Go workflow. A recent post from Anthropic https://www.anthropic.com/research/formal-verification showed how formal verification catches latent bugs in C and C++ by having frontier AI models write machine-checked Rocq https://rocq-prover.org/ proofs across OSS-Fuzz https://github.com/google/oss-fuzz libraries. Instead of sampling random inputs like a fuzzer, a formal tool works backward from each failure condition to solve for the exact input that triggers it. Full theorem proving is still too heavy for most day-to-day Go projects, so I wanted to see how much of that bug-hunting power an agent can get from an LLM and a constraint solver in about a minute per function. In C and C++, reading or writing past the end of a buffer corrupts memory. Go catches out-of-bounds access at runtime instead, compiling every slice or index operation it can't prove safe into an explicit branch to runtime.panicBounds https://github.com/golang/go/blob/go1.27.3/src/runtime/panic.go L208 that panics, crashing the process unless recovered. Before generating machine code, Go's SSA https://pkg.go.dev/cmd/compile/internal/ssa?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 prove https://github.com/golang/go/blob/go1.27.3/src/cmd/compile/internal/ssa/prove.go pass already eliminates most of those checks by tracking slice lengths and loop variables. That optimization pass leaves behind only the runtime.panicBounds traps the compiler couldn't rule out on its own, giving the solver a short list of candidate crash sites to target. I compiled each target with GOOS=linux GOARCH=riscv64 go build -gcflags="-S -d=ssa/check bce/debug=1" -S prints the assembly listing and ssa/check bce/debug=1 logs every surviving bounds check and passed both the Go source and the disassembly to the model. Looking at Go source alone, you can't see which bounds checks the compiler already removed or where a register gets truncated to 8 bits; in the disassembly, both show up. I targeted RISC-V https://en.wikipedia.org/wiki/RISC-V because it's the instruction set Anthropic's post targets for its Rocq proofs, and Go cross-compiles to it out of the box. From there, Argon read the Go source and disassembly and returned a Z3 script modeling the path to each surviving trap, along with a patched function whenever it flagged a bug. Z3 then checked whether those constraints could be satisfied, and whenever it found a crashing input, go test replayed those bytes against the real function. Using an LLM saved me from translating assembly into solver constraints by hand. Argon's translation dominated the runtime, at about a minute per function, while Z3 itself finished in milliseconds. Anthropic's approach relies on interactive theorem proving https://en.wikipedia.org/wiki/Proof assistant , where experts model machine semantics and Rocq checks LLM-generated proofs against those rules. In contrast, my workflow uses a constraint solver based on satisfiability modulo theories SMT https://en.wikipedia.org/wiki/Satisfiability modulo theories , relying on Argon to translate assembly directly into Z3 constraints. While a constraint solver doesn't provide a complete correctness proof without a semantic model, it is highly effective for finding bugs. Z3's check-sat https://microsoft.github.io/z3guide/docs/logic/basiccommands command returns sat when input constraints can be satisfied and unsat when they cannot. A sat answer "definitely buggy" comes with concrete bytes aimed at the trap, and go test runs them against the real function. Once go test panics, you have a concrete bug reproducer regardless of whether Argon's model was sound. Like a Bloom filter for bugs, an unsat answer only means "maybe correct." Trading away a correctness proof is what makes the approach so practical: you get most of the bug-finding value of formal methods for a tiny fraction of the effort. Anthropic's setup proved no-crash properties on whole binaries under a 64 MB budget; I checked individual functions on fresh 64-byte slices where cap buf == len buf https://go.dev/ref/spec?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 Length and capacity , so any slice past len buf panics. If you want the full-binary Rocq setup for Go, theorem-labs/oss-verify https://github.com/theorem-labs/oss-verify includes a Go 1.27 https://go.dev/doc/go1.27?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 runtime overlay that makes the runtime single-threaded and deterministic. For the fuzzing baseline, I ran unseeded go test -fuzz https://go.dev/security/fuzz/?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 on Go 1.27.3 against each planted bug: one 3-second run and three 60-second runs, each with a fresh fuzz cache so a short time budget wouldn't explain a miss. I started with three safe parsers to make sure the pipeline didn't flag clean code. The compiler's prove pass removed every bounds check in a TOML key parser on its own, and Z3 returned unsat on the remaining traps in an HTTP header scanner and a varint decoder. Then I wrote three parsers with subtle panics. Here's the first one, ParseTwoChunkFrame : func ParseTwoChunkFrame buf byte byte, byte { if len buf < 4 || buf 0 = 0xA5 || buf 1 = 0x5A { return nil, nil } hdrLen, bodyLen := buf 2 , buf 3 total := hdrLen + bodyLen if int total +4 len buf { return nil, nil } endHdr := 4 + int hdrLen endBody := endHdr + int bodyLen return buf 4:endHdr , buf endHdr:endBody } In the RISC-V disassembly, the bug is much easier to see: 0x0060 ADD X16, X9, X5 ; X5 = hdrLen + bodyLen 0x0064 MOVBU X5, X5 ; TRUNCATE to uint8: X5 = X5 & 0xff 0x0068 ADDI $4, X5, X5 ; X5 = int total + 4 0x006a BLT X11, X5, 0x00bc ; guard: if len buf < X5, return nil, nil 0x006e MOV X9, X11 ; X11 = int hdrLen 0x0070 MOV X16, X14 ; X14 = int bodyLen 0x0072 ADD X14, X11, X9 ; X9 = int hdrLen + int bodyLen unmasked 0x0076 ADDI $4, X11, X16 ; X16 = endHdr = 4 + int hdrLen 0x007a BLTU X12, X16, 0x00ec ; if cap buf < endHdr - runtime.panicBounds ... 0x0090 ADDI $4, X9, X9 ; X9 = endBody = 4 + int hdrLen + int bodyLen 0x0092 BLTU X12, X9, 0x00e8 ; if cap buf < endBody - runtime.panicBounds total := hdrLen + bodyLen adds two uint8 values, so MOVBU wraps the sum at 256 https://go.dev/ref/spec?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 Integer overflow before the length guard checks it, while endBody adds the full 64-bit ints. Argon turned those instructions into a Z3 query asking whether a fresh slice of up to 64 bytes can pass the guard and still fail the endBody check at 0x0092 : python import z3 s = z3.Solver length, capacity = z3.BitVecs "length capacity", 64 b0, b1, hdrLen8, bodyLen8 = z3.BitVecs "b0 b1 hdrLen8 bodyLen8", 8 wrapped sum64 = z3.ZeroExt 56, hdrLen8 + bodyLen8 + z3.BitVecVal 4, 64 end hdr64 = z3.BitVecVal 4, 64 + z3.ZeroExt 56, hdrLen8 end body64 = end hdr64 + z3.ZeroExt 56, bodyLen8 s.add z3.UGE length, 4 , z3.ULE length, 64 , capacity == length s.add b0 == 0xA5, b1 == 0x5A s.add z3.UGE length, wrapped sum64 , z3.ULE end hdr64, capacity s.add z3.UGT end body64, capacity panic at 0x0092 assert s.check == z3.sat print s.model Z3 returned a 59-byte counterexample with hdrLen = 48 and bodyLen = 236 : their uint8 sum wraps from 284 down to 28 so 28 + 4 ≤ 59 passes the guard , and buf endHdr:endBody then slices to index 288 and panics. At 59 bytes, 19.4% of all possible hdrLen, bodyLen pairs trigger this crash. Yet a 3-second fuzz run missed it, and so did three 60-second runs. Go checks a slice expression https://go.dev/ref/spec?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 Slice expressions like buf endHdr:endBody against the slice's capacity, not its length, and Go's fuzzer rarely passes a slice without spare capacity. In a 10-second probe of 386,741 fuzz calls, 89% of inputs were views into a shared ~100 MB buffer, and only 0.07% had cap == len . With that much spare capacity, endBody at most 514 never exceeds cap buf , so the buggy parser returns bytes past the end of buf instead of panicking. The second target, ExtractQuotedToken , hit the same blind spot when a trailing backslash pushed the index one byte past len buf . Z3 caught it immediately with the 2-byte input byte{'"', '\\'} , while the fuzzer absorbed the overrun in spare capacity. Clipping capacity to length with a full slice expression turns any slice past len into a panic: f.Fuzz func t testing.T, data byte { data = data :len data :len data // cap == len: slicing past the end now panics ParseTwoChunkFrame data } After that change, the fuzzer crashed both ParseTwoChunkFrame and ExtractQuotedToken in all three runs median 0.28 s and 0.17 s . The third target, ParseMagicPacket , was a control because its signed int8 length bug panics on a negative index regardless of capacity, and the fuzzer found it in every run either way. Fuzzing still can't give you an unsat signal across the remaining paths, which is how I checked the three safe parsers and Argon's patches. Next, I pointed the pipeline at skill-lint itself. A whole Go CLI is too large to hand to a solver directly. Even a 10-line parser links 1,559 symbols from the Go runtime, and the 28 MB skill-lint binary has 32,321 symbols in total. Following Functional Core, Imperative Shell https://www.destroyallsoftware.com/screencasts/catalog/functional-core-imperative-shell , I left CLI flags, network calls, and file I/O to go test -fuzz and go test -race , and ran the solver only on pure functions and slice helpers extracted from file-reading code. Of the five functions I tested, two scanners came back unsat including a CRLF line splitter with six surviving bounds checks , and the other three had bugs. The sharpest was in ApplyReplacementChunks , which validates LLM-generated {StartLine, EndLine} edits against the initial line count and sorts them bottom-to-top so earlier edits don't shift later line numbers: for , c := range chunks { if c.StartLine < 1 || c.EndLine len lines || c.StartLine c.EndLine { return nil } } sort.Slice chunks, func i, j int bool { return chunks i .StartLine chunks j .StartLine } for , c := range chunks { lines = append lines :c.StartLine-1 , append c.Replacement, lines c.EndLine: ... ... } Z3 immediately returned sat because sorting by StartLine doesn't prevent two chunks from overlapping. In the extracted helper, which checks bounds once up front, replacing lines 3 and 4 of a 4-line file with one line shrinks lines to 3 elements, so a second chunk spanning lines 2 through 4 evaluates lines 4: and panics with slice bounds out of range 4:3 . In the shipped ApplyChunks , a per-iteration bounds check turns that case into a misleading range error, while overlapping chunks that stay within len lines silently overwrite the earlier edit. Rejecting overlapping chunks after the sort fixes both. The other two bugs were similar accounting errors. In the local fixer, target line numbers were checked once per violation before the inner chunk loop applied deletions that shrank the slice a latent panic if a fixer ever returns a second chunk after a deletion, though DeleteLineFix only returns one today . In the prompt packer, a truncation check reserved a flat 100 bytes for a ~70-byte wrapper plus file path, overshooting the 2 MB context budget in the shipped code when a path exceeds about 30 bytes and panicking in the extracted helper. When you check a function modularly like this, the target has to include its own entry-point guards like the bounds check and sort in ApplyReplacementChunks . If an internal helper assumes preconditions that are only enforced by its caller or stated in a doc comment, Z3 will happily invent inputs that violate them. Because each extracted helper included its entry guards, false positives weren't an issue: across all six buggy functions in my tests, the first sat assignment Z3 returned triggered a real panic in go test without needing to filter out non-crashing candidates or loop back into the solver. Once I pulled these helpers away from file I/O, a 3-second fuzz run caught all three bugs too. To make sure Argon wasn't leaning on source comments in my test files, I also reran the skill-lint targets with all comments stripped; Argon and Z3 still caught all three bugs and returned unsat on the two scanners and all three patches. Staying entirely inside the target language makes a whole class of bugs hard for an agent to see. When an LLM reviews Go source directly, a line like if int total +4 len buf looks like a textbook bounds check, and when it runs go test -fuzz , target-language runtime details like spare slice capacity or multi-step precondition checks can hide the crash indefinitely. Asking the agent to translate Go and assembly into a constraint solver forces a change of representation that strips away surface syntax and makes every bit width and slice bound explicit, while go test turns any solver hit back into a concrete Go reproducer. For most Go code, fuzzing pure helpers with slice capacity clipped to length will catch bounds bugs in seconds. A solver is worth the extra minute on the traps that survive both the compiler's range prover and a quick fuzz run, especially in parsers and editors that compute offsets from multi-field headers or line ranges. Single-threaded solver models don't see data races or deadlocks, so concurrent code still belongs with the race detector https://go.dev/doc/articles/race detector?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 , deterministic concurrency testing https://go.dev/pkg/testing/synctest?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 , and Go 1.27's goroutine leak profiles https://go.dev/doc/go1.27?utm team=DSS+DevRel&utm campaign=default&utm source=blog&utm medium=article&utm content=b583878026 goroutineleak-profiles . If you're experimenting with solvers or coding agents on Go, let's compare notes on X https://x.com/kweinmeister or LinkedIn https://www.linkedin.com/in/karlweinmeister/ .