Agentic framework formally verifies GPU kernels against PyTorch references

LARK uses Lean 4 to prove equivalence between low-level GPU kernels and their high-level specifications, catching bugs that testing alone misses.

Top University

Zixi Zhang · Jiayi Nie · Haoran Wu · Yujie Yan · Yann Herklotz · Rika Antonova · +4 more

Imperial College London · University of Cambridge · Zhejiang University · National University of Singapore

Research Digest·3 November 2026·3 min read

Illustration: Agentic framework formally verifies GPU kernels against PyTorch references

In one line

LARK uses Lean-checked proofs to certify that low-level GPU kernels match their PyTorch specifications and rejects kernels with data races.

Before you read this

An idea this paper builds on

verificationChecking outputs for correctness before accepting them, often to catch errors or reward hacking.284 papers →

Read it as

Graphics processors run specialized small programs called kernels. Tests check only selected inputs, so they can miss bugs in code that appears to work.

LARK uses Lean, a tool that checks mathematical proofs, to show that a kernel matches its reference implementation in PyTorch, a machine-learning software framework. Software agents split the proof into smaller parts, and Lean checks each part against a model of the hardware and operations prepared in advance.

LARK verified nine of ten production kernels and found a data race in the remaining one, where concurrent threads access shared data unsafely. This offers stronger assurance than sampled tests, though the proofs assume exact arithmetic and do not cover real-world rounding.

How it works

before and after

RSS

The Daily Edition

The front page in your inbox each weekday morning: the lead, the picks, and why each one earned its place.

Concepts

verification trust boundary