Google uses Gemini and Z3 to find crashes missed by Go fuzzing
Understand this story
The lead of Google's agent skills project shared a workflow: using Gemini 4 Argon to translate Go source code and RISC-V disassembly into Z3 constraints, locate the runtime.panicBounds trap that remains after compiler optimization, and then have go test reproduce the crash using the specific bytes provided by the solver. The lead said that go test -fuzz missed two of these crashes and provided a one-line fix. According to their explanation, most of the time in this workflow is spent on Argon's translation, about one minute per function, while Z3 itself only takes milliseconds; validation targets a 64-byte slice with cap(buf) == len(buf), and any slice beyond len(buf) will panic.
AI overview based on source reports · Updated 2 days ago
Coverage timeline
Follow the coverage to explore different perspectives.
- Google Developers BlogCatch Go bugs that fuzzing misses with Gemini and a constraint solver
The author describes a workflow that compiles Go functions to RISC-V assembly, has Gemini 4 Argon translate the surviving runtime.panicBounds traps into Z3 constraints, and replays any satisfying input through go test to produce a real reproducer. The pipeline caught three planted bugs and three latent bugs in skill-lint, and the post explains why go test -fuzz missed two crashes because fuzz inputs usually have spare slice capacity, fixed by clipping capacity to length with a full slice expression. It also notes that an unsat result only means "maybe correct," since the LLM-written solver model is not a sound proof system.
Activity for this story
- Current comparable activity
- 3
- Peak comparable activity
- 5Nov 13 06:00
- Change in the past 24 hours
- -49%
Trends compare the same fully observed participants, which may cover fewer participants than current activity. Move the pointer or tap the chart to inspect hourly activity; use the left and right arrow keys with a keyboard.