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.

• 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 for every kernel in our benchmark, with diagnostics and evidence, are in Kernel verification results.

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.

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.

pip install sentryward                # the synchronization check, including race freedom
pip install "sentryward[reference]"   # adds PyTorch for reference equivalence

Wheels include the native verifier. Building from source needs CMake 3.27+, a C++20 compiler, OpenSSL, Boost headers and, optionally, Z3.

# Run the synchronization check, including race freedom
sentryward kernel.ptx --input input.json > output.json

# Override one analysis assumption for this invocation
sentryward kernel.ptx --input input.json --assume order_independent_atomics

# Accepted keys and repository defaults
sentryward --list-assumptions

# Also check equivalence to a PyTorch reference
sentryward kernel.ptx \
  --input input.json \
  --reference reference.py \
  --reference-binding reference_binding.json \
  --timeout 500 \
  --memory-limit-mib 81920 > output.json

The same check from Python:

from sentryward import verify

result = verify(
    "kernel.ptx",
    input="input.json",
    reference="reference.py",                    # optional
    reference_binding="reference_binding.json",  # optional
    timeout_seconds=500,
    memory_limit_mib=None,                       # unlimited
    assumptions={"order_independent_atomics": True},  # optional
)
print(result["result"], result["checks"])

The reference takes no separate input file. Its arguments are derived from the kernel's input configuration and the binding; anything that cannot be derived goes in the binding's reference section. The binding's optional provenance object supplies source metadata and recorded input scope; see the binding format.

Python paths accept strings or pathlib.Path. A reference binding requires a reference function. Timeout values must be positive and finite; explicit memory limits must be positive integers and apply to both capture and verification. The reference function executes as Python code during capture. The public Python package exports verify; the CLI accepts the PTX path directly, without a subcommand, except --list-assumptions, which prints the assumption pool and does not take a PTX path. Assumption flags are documented in assumptions.md.

The CLI prints a JSON result to stdout, and verify returns the same structure as a dictionary:

• result is the overall verdict. race_free means the synchronization check passed and no reference was given; verified means equivalence to the reference was proved as well. Other values name a finding, such as potential_race, or the reason the analysis stopped, such as unsupported or timeout.
• checks gives the status of the two checks: synchronization (synchronization, memory races and resource lifecycles) and equivalence.
• diagnostics and warnings hold the details; evidence holds race and synchronization witnesses.
• internal holds analysis details such as equivalence receipts; it is not a stable interface.

CLI exit code 0 can also accompany findings or inconclusive checks; inspect result and checks instead of using the exit code as a correctness verdict. See output.json for the complete result format.

Install a C++20 compiler, CMake 3.27+, Boost headers, OpenSSL and Z3 development libraries, then install from the repository root:

python -m pip install ".[reference]"

For a standalone native build, use make build-cpp. To rerun the saved examples:

make venv
build/venv/bin/python -m pip install ".[reference,dev]"
make rerun-examples

The default build contains the verifier only. Example reruns preserve previous outputs; make rerun-examples-performance includes historical timeout cases.

To select one example and set its total time budget:

make rerun-examples EXAMPLE_RUN_ARGS="--name pytorch__aten_MultiMarginLoss__sm_100a --timeout 500"

The runner reuses inputs unchanged and checks reference equivalence after verification prerequisites pass. Current results are saved in examples/<kernel>/output.json; previous outputs and run summaries are retained under build/artifacts/. Narrative reports are not included; use the generate-kernel-report skill to generate a report from the current output when needed.

• Problem sizes and the launch configuration are fixed.
• Branches and loop bounds may depend on the launch configuration, but not on tensor data, with two exceptions. Integer comparisons decided by stated tensor property bounds take the decided outcome. A forward branch over a straight-line block of register and tensor-memory operations can be merged. Other data-dependent control needs the representative-control assumptions; see Representative branches, off by default.
• Atomics (atom, red) are analyzed only under Order-independent atomics, off by default.
• Fences and the full PTX memory model are not modeled. The hardware model follows our reading of the PTX documentation, which does not specify every detail.
• Equivalence treats floating-point values as real numbers, and the check is incomplete: finding no proof does not mean the kernel is wrong.

• Assumptions and limitations: configurable assumptions and trusted address constraints.
• input.json: launch configuration, ABI arguments, tensor maps, pointer tables, tensor properties and assumptions.
• reference_binding.json: reference arguments, input/output correspondence and the equivalence contract.
• output.json: result categories, checks, diagnostics and warnings.

cpp/                C++ frontend, verifier and equivalence engine
sentryward/         Python CLI and process interface
corpus/             Compiled Blackwell PTX kernels of the benchmark
examples/<kernel>/  input.json, output.json, and reference.py/reference_binding.json where available
examples/_reference/ Shared mathematical helpers used by example references
config/             Default and available analysis assumptions
skills/             Agent skills for preparing inputs and explaining results
tools/              Example regression tooling

Questions, bug reports and feedback are welcome in the SentryWard Slack workspace and in GitHub issues.

Apache License 2.0; see LICENSE.