| name | verify-prevail |
| description | Diagnose eBPF program verification failures from the PREVAIL verifier. Use this skill for linux-compatible eBPF programs verified in the standalone PREVAIL repo (external/ebpf-verifier). For programs using Windows-specific features (bpf2c pipeline, Windows helpers, ebpf-for-windows headers), use the 'verify-bpf' skill instead.
|
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.
