(No kernel panic — this finding is hardware-gated [no FireWire controller on
 the QEMU guest], so the live in-kernel path cannot be triggered.  Instead
 the primitive is proven at the harness level using the VERBATIM kernel code.
 See VERDICT.md "Proof (harness)" and "In-kernel reachability".)

Underflow math (confirmed by harness):
  textleaf->crc_len is u_int32_t:16  (BIT16x2 macro, firewire.h:122)
  fwcrom.c:215  qlen = textleaf->crc_len - 2;       // crc_len=0 -> qlen=-2 (signed int)
                                                    // crc_len=1 -> qlen=-1
  fwcrom.c:216  if (len < qlen * 4) qlen = len/4;   // len(32) < -8  -> FALSE, qlen stays negative
  fwcrom.c:218  for (i=0; i<qlen; i++) ...          // 0 < -2 -> FALSE, loop skipped
  fwcrom.c:221  if (len <= qlen*4) buf[len-1]=0;    // 32 <= -8 -> FALSE
  fwcrom.c:224  else buf[qlen*4]=0;                 // *** buf[-8]=0 (crc_len=0) / buf[-4]=0 (crc_len=1) ***

Harness observation:
  [crc_len=0] pre[8]  (== buf[-8]) zeroed  -> BUG CONFIRMED
  [crc_len=1] pre[12] (== buf[-4]) zeroed  -> BUG CONFIRMED
  [crc_len=2] control case: canary intact (no bug)