Races and overflows, without a GPU - The Formal Era

Some GPU bugs only appear on some shapes, some inputs, or some schedules. This run verifies four such kernels with CUDA_VISIBLE_DEVICES='', so no GPU is visible:

$ python -c 'import torch; print("GPUs visible:", torch.cuda.device_count())'
GPUs visible: 0
$ time theformalera verify kernels/unsafe_samples.py
 kernel                       spec node                 configs   result    level / id     time
 ──────────────────────────────────────────────────────────────────────────────────────────────
 silu_mul_fp16_exp            layers[*].mlp.act             0/1   FAILED    F-0005         24ms
 silu_mul_int32_index         layers[*].mlp.act             0/1   FAILED    F-0006         56ms
 rmsnorm_unmasked_store       layers[*].input_norm          0/1   FAILED    F-0007         2.1s
 residual_overlapping_tiles   layers[*].attn_residual       0/1   FAILED    F-0008         2.6s

0 passed · 4 failed · 0 unknown        run `theformalera explain F-0005`

real	0m5.734s

With zero GPUs visible, theformalera verify fails all four kernels in 5.7 seconds; explain shows an int32 overflow for T=61682 and a write-write conflict

Kernel	Defect	Verdict
`silu_mul_fp16_exp`	Sigmoid as `e^g / (1 + e^g)` with `e^g` cast to fp16: `e^g` is infinite for `g > 11.09`, and inf / inf is NaN	OVERFLOW, 24 ms
`silu_mul_int32_index`	`row * (2 * I)` in int32 wraps for long prefills	OVERFLOW, 56 ms; `correct only when T <= 61681`
`rmsnorm_unmasked_store`	The store is not masked: lanes 5120–8191 write into the next row, racing the program that owns it	UNSAFE, 2.1 s
`residual_overlapping_tiles`	Tiles advance by `BLOCK - 64` but are `BLOCK` wide: neighbouring programs write the same 64 elements	UNSAFE, 2.6 s

$ theformalera explain F-0006
F-0006  OVERFLOW  silu_mul_int32_index -> Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act
failing configs    1 of 1
witness            T=61682                  int32 overflow of `%g` for T=61682
correct only when  T <= 61681

$ theformalera explain F-0008
F-0008  UNSAFE  residual_overlapping_tiles -> Qwen/Qwen3.8-27B@1.0:layers[*].attn_residual
failing configs    1 of 1
witness (minimal)  T=1                      write-write conflict on `Y` at element offset 960 (program (1, 0, 0)):
                   address already written by program 0

How they are found

Integer overflow is checked with an SMT solver over the whole shape domain, not by sampling. That is how the exact boundary T = 61682 comes out.
Float overflow uses interval analysis over the declared value domain (bf16 activations, |x| ≤ 65504).
Races and out-of-bounds accesses are found by an instrumented interpreter that records every address every program touches. A race shows up as two programs writing the same address, deterministically, whatever the schedule.

On a GPU, the unmasked store produces correct or wrong output depending on which program happens to run last. On a CPU, the verifier reports it every time.

⌘I