Ep. 014 - Finding Miscompiles For Fun, Not Profit (AI Infrastructure) | Justin Lebar & Jordan Nanos

Summary

Justin Lebar walks through a project that hunted miscompiles in Nvidia’s PTX compiler and LLVM’s AMDGPU and x86 backends using two approaches: traditional fuzzing and LLM-assisted code reading. He describes how fuzzing requires generating well-formed random programs and checking equivalence after compilation, often by executing on a GPU, but eventually hits diminishing returns as the same bugs recur. Lebar reports finding one or two high-severity x86 bugs, including an atomic operation that can be split into two non-atomic operations, plus multiple AMDGPU miscompiles. He says agentic code reading was initially shocking in how well it worked, though it was expensive, and that newer tooling like slash-goal support and UltraCode improved token efficiency substantially. The broader takeaway is that LLMs can materially improve compiler bug-finding and even help validate fixes, if teams are willing to spend the compute and human review time.

Notes

• Episode focuses on compiler miscompile hunting across GPU and CPU backends.
• PTX sits between higher-level code and GPU machine code.
• Nvidia’s PTXAS was one target of the bug hunt.
• LLVM bug hunting covered AMDGPU, x86, and shared backend code.
• Fuzzing was framed as random-program generation plus semantic equivalence checking.
• Well-formed inputs were necessary because arbitrary programs can trigger undefined behavior.
• GPU-based execution was used to validate fuzzed programs.
• The fuzzer needed both weirdness and correctness to be useful.
• He found one or two very high-severity x86 bugs.
• One x86 miscompile can split an atomic into two non-atomic operations.
• That x86 atomic bug is severe because it breaks atomicity guarantees.
• AMDGPU produced multiple miscompiles, but Lebar avoids overgeneralizing from that sample.
• Lebar says the evidence does not prove AMDGPU is broadly buggier.
• The project surfaced a number of reproducible compiler failures.
• He examined only a subset of the x86 findings in detail.
• A subset of the x86 bugs were high severity, not just edge-case noise.
• Fuzzer progress slowed as it kept rediscovering the same issues.
• Diminishing returns made the fuzzing workflow harder to extend.
• LLM-assisted code reading became the next bug-finding tactic.
• The agent-based approach was surprisingly effective.
• The agent-based approach was also expensive.
• Newer harness features made orchestration easier.
• Slash-goal support reduced the amount of manual steering required.
• Improved model-generated code quality changed the workflow.
• Earlier attempts required more manual nudging of the model.
• UltraCode was designed for large orchestrated projects.
• UltraCode cut token usage to about one-tenth of prior scans.
• UltraCode produced higher-quality findings but fewer of them.
• Lebar is willing to trade quantity for more actionable bug reports.
• He estimates the newer UltraCode workflow cost about $1,000 versus $10,000 earlier.
• The model often helps verify his fixes after he edits them.
• He says AI is already improving the quality of published code.
• Tokens can be worth spending if the goal is real bug discovery.
• The bottleneck is organizational willingness, not just model capability.
• Formal verification is presented as the hard limit of compiler assurance.
• CompCert is cited as a formally verified compiler example.
• LLMs are framed as a practical complement to, not a replacement for, formal methods.
• The project is positioned as a scientific approach to bug finding.
• The episode closes with a call for community engagement.
• Bug-finding methods are still evolving quickly.
• The main investor-relevant implication is that token spend can buy real reliability gains.