Verify Prevail

Diagnose PREVAIL Verification Failures (Linux-Compatible Programs)

Diagnose eBPF program verification failures using the standalone PREVAIL verifier

(external/ebpf-verifier). This skill covers linux-compatible eBPF programs

that can be verified directly with the PREVAIL check or run_yaml tools.

When to Use

• User shares a PREVAIL verifier error or log and asks why verification failed
• User asks to diagnose, debug, or explain an eBPF verification failure **in the

PREVAIL repo** (external/ebpf-verifier)

• User asks to debug PREVAIL YAML test failures or abstract-interpretation issues
• User is working on verifier internals (abstract domains, widening, transformers)
• User mentions "verifier", "verification", "PREVAIL", or "abstract interpretation" errors

for linux-compatible BPF programs

When NOT to Use

• Program uses Windows-specific helpers or headers (e.g., ebpf_helpers.h,

sample_ext_helpers.h, WFP hook types) → use verify-bpf instead

• User wants to run the bpf2c pipeline (clang → bpf2c → native driver) → use

verify-bpf instead

• User needs to compile a .c BPF source to .o for ebpf-for-windows → use

verify-bpf instead

Reference Document

Read the full PREVAIL diagnostic reference before diagnosing:

external/ebpf-verifier/docs/llm-context.md

This document contains:

• How to interpret PREVAIL log output (register state, stack state, invariants)
• Glossary of log terms, types, type groups, and assertions
• Common failure patterns with symptoms, causes, and fixes
• Advanced topics (widening, path-insensitivity, pointer provenance)
• A step-by-step reasoning protocol for diagnosis

Always read this file first — it is the authoritative reference for PREVAIL diagnostics.

Diagnosis Instructions

Step 1: Read the Reference

Read external/ebpf-verifier/docs/llm-context.md to load the full diagnostic context.

Step 2: Gather the Error

Ask the user to provide (if not already given):

• The verifier error message (the line with <pc>: <message> (<assertion>))
• The pre-invariant at the failing instruction
• The 3–5 instructions leading up to the failure
• The source code of the eBPF program (or the relevant section)
• Any map or context definitions (for map/context-related errors)

Step 3: Identify the Failure Pattern

Using the reference document, match the error to one of the common failure patterns:

| Pattern | Key Symptom |

|---------|-------------|

| Uninitialized register | Invalid type (r<N>.type in {...}) |

| Unbounded packet access | Upper bound must be at most packet_size |

| Stack out-of-bounds | Lower bound must be at least r10.stack_offset - EBPF_SUBPROGRAM_STACK_SIZE |

| Null pointer (map lookup) | Possible null access |

| Type mismatch | Only pointers can be dereferenced |

| Pointer arithmetic error | Only numbers can be added to pointers |

| Infinite loop | Loop counter is too large (pc[N] < 100000) |

| Division by zero | Possible division by zero |

| Map key/value mismatch | Illegal map update with a non-numerical value |

| Context bounds violation | Nonzero context offset or context Upper bound error |

| Lost correlation (verifier limitation) | Bounds check present but verifier can't prove safety |

Step 4: Trace the Root Cause

Follow the reasoning protocol from the reference:

• Check the pre-invariant — what types and constraints do the relevant registers have?
• Identify missing constraints — what constraint would make the assertion pass?
• Trace backwards — where was the constraint lost or never established?
• Check for verifier limitations — is this a code bug or a verifier precision issue?

Step 5: Recommend a Fix

Provide:

• A clear explanation of why verification failed
• The specific constraint that is missing or violated
• A concrete code fix (with before/after examples when possible)
• If it's a verifier limitation, suggest workarounds (direct pointer comparisons, restructured control flow, etc.)

Important Notes

• PREVAIL is more conservative than the Linux kernel verifier — code accepted by Linux may be rejected by PREVAIL.
• PREVAIL is path-insensitive — it uses a single abstract state per program point, so correlated conditions across branches may be lost.
• Widening at loop headers can destroy constraints — if a loop-related failure occurs, check whether widening eliminated a needed bound.
• Never assume a register has a type or constraint unless it appears in the pre-invariant.