---
title: "Formalizing PTX in Lean to Prove GPU Kernel Correctness"
source: "arXiv AI/CL/LG（论文）"
source_tier: "t2"
url: "https://arxiv.org/abs/2611.04447v1"
permalink: "https://feed.astralor.com/items/itm_53012de7354d62dcc1041e41"
published: "2026-11-03T07:37:20.000Z"
score: 53
channel: "tech"
tags: ["Formalizing PTX","Lean","Prove GPU Kernel","Correctness","PTX","GPU","Deep Learning"]
---

# Formalizing PTX in Lean to Prove GPU Kernel Correctness

## At a glance

We present an approach to mathematically formalizing PTX, an approach that allows modeling and reasoning about patterns common in GPU kernels for Deep Learning, including acquire-release, tensor cores, proxies, async op…

## Key points

- We present an approach to mathematically formalizing PTX, an approach that allows modeling and reasoning about patterns common in GPU kernels for Deep Learning, including acquire-release, tensor cores, proxies, async op…
- We implement it in Lean and use it to prove the correctness of simple implementations of a WGMMA GEMM kernel, FlashAttention, and a 3-kernel MoE pipeline.

## Full text

We present an approach to mathematically formalizing PTX, an approach that allows modeling and reasoning about patterns common in GPU kernels for Deep Learning, including acquire-release, tensor cores, proxies, async operations, multi-kernel pipelines and data-dependent control flow. We implement it in Lean and use it to prove the correctness of simple implementations of a WGMMA GEMM kernel, FlashAttention, and a 3-kernel MoE pipeline.

---

Verify against the original before citing; curated by Astral Feed: https://feed.astralor.com/items/itm_53012de7354d62dcc1041e41