gpu-verifier / sentryward

# Formal verification of warp-specialized GPU kernels
*Reveal hidden bugs in GPU kernels.*
Features ·
Results ·
Getting started ·
How it works ·
Community
SentryWard is a static verifier for NVIDIA PTX kernels, built for the
warp-specialized kernels of Blackwell GPUs. Given a kernel's PTX and a launch
configuration, it proves that the kernel synchronizes correctly and is free of
data races in every schedule within the configured input scope and
model assumptions. Given a PyTorch reference as well, it also proves
that the kernel computes the same function.
## Features
- **Well-synchronization.** Barriers and mbarriers, including TMA byte counts,
 behave the same way in every schedule. This also rules out deadlocks.
- **Race freedom.** Every pair of conflicting accesses to global, shared or
 tensor memory is ordered. Footprints follow exact layouts, including
 swizzling, and an SMT solver decides overlap for symbolic addresses.
- **Resource lifetimes.** Tensor memory and barriers are never used after they
 are freed or invalidated.
- **Equivalence to a reference.** The kernel's outputs equal those of a
 PyTorch reference, in real arithmetic.
- **Witnesses.** Every failed check comes with evidence, such as the two
 unordered accesses of a race. Inconclusive checks retain their specific
 result category and diagnostics; they are never reported as a pass.
- **Blackwell coverage.** TMA, `tcgen05` MMA and tensor memory, mbarriers,
 thread-block clusters and asynchronous copies.
## Results
Results for every kernel in our benchmark, with diagnostics and evidence, are
in Kernel verification results.
### Bugs in popular kernel libraries
SentryWard has found synchronization bugs in popular kernel libraries, such as
a signal sent before the asynchronous write it announces has completed, and a
buffer reused while the tensor core is still reading it. We have reported some
of them upstream.
### Removing redundant synchronization
Because SentryWard checks every schedule, it can also show that a
synchronization operation is unnecessary: if the kernel still verifies without
it, the operation is redundant. We applied this test greedily, one operation at a time.
Per-kernel synchronization removal results
include removable operation counts and B200 timings for both recorded and larger
inputs. Experiments are saved in examples/results.json, with
their sources, methodology, and limitations. These results hold for the tested
input shapes; other shapes may require synchronization that was removable here.
## Getting started
### Install
 [code] 
Wheels include the native verifier. Building from source needs CMake 3.27+, a
C++20 compiler, OpenSSL, Boost headers and, optionally, Z3.
### Verify a kernel
 [code] 
The same check from Python:
 [code] 
| CLI | Python | Description |
| --- | --- | --- |
| `--input` | `input` | Required. The kernel's input configuration (JSON). |
| `--reference` | `reference` | Optional. A Python file that defines a `reference(...)` function. |
| `-