Formal verification · NVIDIA Blackwell

Automatically verify GPU kernels in PTX.

SentryWard automatically proves that a GPU kernel synchronizes correctly and is free of data races across every execution schedule. Add a PyTorch reference to prove that it computes the same function. Built for warp-specialized kernels on NVIDIA Blackwell GPUs.

Get started How it works

What goes in. What comes out.

Input

PTX kernel: Your compiled NVIDIA GPU kernel.
Input configuration: A JSON file describing input shapes, launch dimensions, kernel parameters, and any TMA descriptors.
Optional PyTorch reference: A reference(...) function and a binding that maps its arguments and outputs to the kernel. No separate reference input file is needed.

Output

A clear verdict: race_free means synchronization and memory checks passed without a reference. verified means reference equivalence was proved too.
Check results and witnesses: JSON from the CLI, or a Python dictionary, with each check’s status and evidence for findings such as potential_race.
Explicit limits: unsupported or timeout explains why analysis stopped. An undecided check is never reported as a pass.

What SentryWard verifies

Synchronization & deadlocks: Barriers and mbarriers, including TMA byte counts, behave consistently across schedules, ruling out deadlocks.
Data races: Conflicting accesses to global, shared, and tensor memory are ordered, including asynchronous copies and tensor-core operations.
Resource lifetimes: Tensor memory and barriers are never used after they are freed or invalidated.
Mathematical correctness: The kernel’s outputs equal those of your PyTorch reference in real arithmetic.
Unnecessary waits: Use verification to remove redundant synchronization: remove an operation, then verify again. Safe removals depend on the input shape.

Covers Blackwell TMA, tcgen05 MMA and tensor memory, mbarriers, thread-block clusters, and asynchronous copies. Proofs apply to fixed shapes and launches. By default, control flow cannot depend on tensor data. Floating-point rounding, fences, and the full PTX memory model are not modeled. Scope and limitations

Try it on your kernel

With Python 3.10 or newer, install and run synchronization and memory checks:

pip install sentryward
sentryward kernel.ptx \
  --input input.json > output.json

The CLI prints JSON; the command above saves it to output.json.

Also prove mathematical correctness

pip install "sentryward[reference]"
sentryward kernel.ptx \
  --input input.json \
  --reference reference.py \
  --reference-binding reference_binding.json \
  > output.json

Use the Python API

from sentryward import verify

result = verify(
    "kernel.ptx",
    input="input.json",
    reference="reference.py",                    # optional
    reference_binding="reference_binding.json",  # optional
)
print(result["result"], result["checks"])

Install sentryward[reference] when supplying a PyTorch reference.

Full usage and options, including time and memory limits.

Read the technical post for the algorithms, examples, and results