I help lead Google's agent skills program, currently with 175 agent skills that supplement community collections like go-skills. To keep that many skill files consistent, I wrote skill-lint, a standalone Go 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 translated the path to each trap into rules for the Z3 constraint solver. 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 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 showed how formal verification catches latent bugs in C and C++ by having frontier AI models write machine-checked Rocq proofs across 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 that panics, crashing the process unless recovered.
Before generating machine code, Go's SSA prove 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 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, 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), 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 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), so any slice past len(buf) panics. (If you want the full-binary Rocq setup for Go, theorem-labs/oss-verify includes a Go 1.27 runtime overlay that makes the runtime single-threaded and deterministic.)
For the fuzzing baseline, I ran unseeded go test -fuzz 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 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:
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 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, 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, deterministic concurrency testing, and Go 1.27's goroutine leak profiles.
If you're experimenting with solvers or coding agents on Go, let's compare notes on X or LinkedIn.