Bug Zoo is TorchLean’s collection of small case studies for semantic bugs that can pass ordinary runtime checks. These examples focus on cases where code still returns tensors, losses, or tokens, but the returned value no longer satisfies the intended contract.

Each Bug Zoo file follows the same pattern:

• name the failure mode,
• state the contract (what the code is supposed to mean),
• prove the part that is actually within Lean’s scope,
• and label the boundary when the checked claim depends on an external runtime.

A Few Case Studies

Attention Masks Checks that masked future positions receive exactly zero attention weight under the stated causal mask semantics. KV Cache and RoPE Makes the cache-position contract explicit so incremental decoding agrees with the intended full-sequence computation. Tokenizer Boundaries Separates byte/token assumptions from model assumptions, so text preprocessing cannot silently change the checked claim. Normalization State Tracks which statistics are training state, inference state, or explicit inputs rather than treating normalization as a black box. Batch Invariance States when processing one sample alone should agree with processing it as part of a batch. Float and Autograd Boundaries Shows how runtime `Float32` and reverse-mode claims are connected through named assumptions and proof-facing statements.

What “A Checked Claim” Looks Like Here

Each case study should end in a precise statement.

Here is the attention-mask claim in one line: strict-future keys get exactly zero attention weight under the stated causal mask semantics.

theorem trueInfinityMask_future_attention_weight_zero :
  Spec.get2 (Spec.hardMaskedSoftmaxSpec scores (Spec.causalMask n)) i j = 0

And here is the Float32 boundary claim: runtime arithmetic rewrites to the explicit IEEE32Exec model only under a named assumption.

theorem runtimeFloat32_add_rewrites_to_ieee32
    [RuntimeFloat32MatchesIEEE32Exec] (a b : F32) :
    toIEEE32Exec (a + b) = IEEE32Exec.add (toIEEE32Exec a) (toIEEE32Exec b)

Those are the statement shapes Bug Zoo is meant to make routine.