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):

1. The verifier error message (the line with <pc>: <message> (<assertion>))
2. The pre-invariant at the failing instruction
3. The 3–5 instructions leading up to the failure
4. The source code of the eBPF program (or the relevant section)
5. 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:

Step 4: Trace the Root Cause

Follow the reasoning protocol from the reference:

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

Step 5: Recommend a Fix

Provide:

1. A clear explanation of why verification failed
2. The specific constraint that is missing or violated
3. A concrete code fix (with before/after examples when possible)
4. 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.