diff --git a/src/analysis_engine.cpp b/src/analysis_engine.cpp
new file mode 100644
index 000000000..f4aa7306a
--- /dev/null
+++ b/src/analysis_engine.cpp
@@ -0,0 +1,268 @@
+// Copyright (c) Prevail Verifier contributors.
+// SPDX-License-Identifier: MIT
+
+#include "analysis_engine.hpp"
+
+#include <filesystem>
+#include <iostream>
+#include <stdexcept>
+#include <string>
+
+namespace prevail {
+
+AnalysisEngine::AnalysisEngine(PlatformOps* ops) : ops_(ops) {}
+
+bool AnalysisEngine::analysis_options_equal(const prevail::ebpf_verifier_options_t& a,
+                                             const prevail::ebpf_verifier_options_t& b) {
+    return a.cfg_opts.check_for_termination == b.cfg_opts.check_for_termination &&
+           a.allow_division_by_zero == b.allow_division_by_zero && a.strict == b.strict;
+}
+
+bool AnalysisEngine::session_matches(const std::string& elf_path, const std::string& section,
+                                     const std::string& program, const std::string& type,
+                                     const prevail::ebpf_verifier_options_t& options) const {
+    if (!session_) {
+        return false;
+    }
+    if (session_->elf_path != elf_path || session_->section != section || session_->program_name != program ||
+        session_type_ != type) {
+        return false;
+    }
+    if (!analysis_options_equal(session_->options, options)) {
+        return false;
+    }
+    // Re-analyze if the file has been modified since last analysis.
+    try {
+        return std::filesystem::last_write_time(elf_path) == session_->file_mtime;
+    } catch (const std::filesystem::filesystem_error&) {
+        return false; // File no longer accessible — force re-analysis.
+    }
+}
+
+const prevail::ebpf_verifier_options_t& AnalysisEngine::session_options() const {
+    if (session_) {
+        return session_->options;
+    }
+    // No session — return platform defaults. Cache to avoid returning a dangling reference.
+    static thread_local prevail::ebpf_verifier_options_t defaults;
+    defaults = ops_->default_options();
+    return defaults;
+}
+
+std::vector<ProgramEntry> AnalysisEngine::list_programs(const std::string& elf_path) {
+    return ops_->list_programs(elf_path);
+}
+
+const AnalysisSession& AnalysisEngine::analyze(const std::string& elf_path, const std::string& section,
+                                               const std::string& program, const std::string& type,
+                                               const prevail::ebpf_verifier_options_t* options) {
+    // Use caller-provided options or platform defaults.
+    prevail::ebpf_verifier_options_t effective_options = options ? *options : ops_->default_options();
+
+    // Reuse the current session if it matches.
+    if (session_matches(elf_path, section, program, type, effective_options)) {
+        return *session_;
+    }
+
+    // Different program or options — discard old session and run fresh analysis.
+    session_.reset();
+
+    ops_->prepare_tls(type);
+
+    // Determine target program using the new ElfObject API.
+    std::string target_section = section;
+    std::string target_program = program;
+    if (target_section.empty() && target_program.empty()) {
+        auto entries = list_programs(elf_path);
+        for (const auto& entry : entries) {
+            if (entry.section != ".text") {
+                target_section = entry.section;
+                target_program = entry.function;
+                break;
+            }
+        }
+        if (target_section.empty() && !entries.empty()) {
+            target_section = entries.front().section;
+            target_program = entries.front().function;
+        }
+    }
+
+    auto tls_guard = std::make_unique<prevail::ThreadLocalGuard>();
+
+    prevail::ElfObject elf(elf_path, effective_options, ops_->platform());
+    const auto& raw_progs = elf.get_programs(target_section, target_program);
+
+    if (raw_progs.empty()) {
+        throw std::runtime_error("Program not found: " + target_program + " in " + elf_path);
+    }
+    const auto& found = raw_progs.front();
+
+    std::vector<std::vector<std::string>> notes;
+    auto prog_or_error = prevail::unmarshal(found, notes, effective_options);
+    if (auto* err = std::get_if<std::string>(&prog_or_error)) {
+        throw std::runtime_error("Unmarshal error: " + *err);
+    }
+    auto& inst_seq = std::get<prevail::InstructionSeq>(prog_or_error);
+
+    prevail::Program prog = prevail::Program::from_sequence(inst_seq, found.info, effective_options);
+    prevail::AnalysisResult result = prevail::analyze(prog);
+
+    // Build session with serialized invariants (while TLS is alive).
+    AnalysisSession session;
+    session.elf_path = elf_path;
+    session.section = found.section_name;
+    session.program_name = found.function_name;
+    session.options = effective_options;
+    session.inst_seq = std::move(inst_seq);
+    session.program = std::move(prog);
+    session.failed = result.failed;
+    session.max_loop_count = result.max_loop_count;
+    session.exit_value = result.exit_value;
+    session.file_mtime = std::filesystem::last_write_time(elf_path);
+
+    for (const auto& [label, inv_pair] : result.invariants) {
+        AnalysisSession::SerializedInvariant si;
+        si.pre_is_bottom = inv_pair.pre.is_bottom();
+        try {
+            if (!si.pre_is_bottom) {
+                si.pre = inv_pair.pre.to_set();
+            }
+            if (!inv_pair.post.is_bottom()) {
+                si.post = inv_pair.post.to_set();
+            }
+        } catch (const std::exception& e) {
+            std::cerr << "prevail: warning: failed to serialize invariant at label " << label.from << ": "
+                      << e.what() << std::endl;
+        }
+        if (inv_pair.error.has_value()) {
+            si.error_message = inv_pair.error->what();
+            si.error_label = inv_pair.error->where;
+        }
+        session.invariants.emplace(label, std::move(si));
+    }
+
+    // Build source maps from BTF line info.
+    int pc = 0;
+    for (const auto& [label, inst, line_info] : session.inst_seq) {
+        if (line_info.has_value()) {
+            session.pc_to_source[pc] = *line_info;
+            auto src_key = std::make_pair(line_info->file_name, static_cast<int>(line_info->line_number));
+            session.source_to_pcs[src_key].push_back(pc);
+        }
+        pc += prevail::size(inst);
+    }
+
+    // Build PC → Label lookup.
+    for (const auto& [label, inv] : session.invariants) {
+        session.pc_to_labels[label.from].push_back(label);
+    }
+
+    // Keep live state for check_constraint and slicing.
+    session.live_result = std::move(result);
+    session.tls_guard = std::move(tls_guard);
+
+    session_ = std::move(session);
+    session_type_ = type;
+    return *session_;
+}
+
+// ─── Live session operations ───────────────────────────────────────────────────
+
+prevail::ObservationCheckResult
+AnalysisEngine::check_constraint(const std::string& elf_path, const std::string& section, const std::string& program,
+                                 const std::string& type, const prevail::Label& label, prevail::InvariantPoint point,
+                                 const prevail::StringInvariant& observation, const std::string& mode_str) {
+    // analyze() ensures the session is live.
+    analyze(elf_path, section, program, type);
+
+    if (mode_str == "proven") {
+        auto it = session_->live_result->invariants.find(label);
+        if (it == session_->live_result->invariants.end()) {
+            return {.ok = false, .message = "No invariant available for label"};
+        }
+        const auto& abstract_state = (point == prevail::InvariantPoint::post) ? it->second.post : it->second.pre;
+        if (abstract_state.is_bottom()) {
+            return {.ok = false, .message = "Invariant at label is bottom (unreachable)"};
+        }
+
+        const auto observed_state = observation.is_bottom()
+                                        ? prevail::EbpfDomain::bottom()
+                                        : prevail::EbpfDomain::from_constraints(
+                                              observation.value(), prevail::thread_local_options.setup_constraints);
+        if (observed_state.is_bottom()) {
+            return {.ok = false, .message = "Observation constraints are unsatisfiable"};
+        }
+
+        if (abstract_state <= observed_state) {
+            return {.ok = true, .message = ""};
+        }
+        return {.ok = false,
+                .message = "Invariant does not prove the constraint (A ⊑ C is false). "
+                           "The verifier's state includes possibilities outside the observation."};
+    }
+
+    prevail::ObservationCheckMode mode;
+    if (mode_str == "entailed") {
+        mode = prevail::ObservationCheckMode::entailed;
+    } else if (mode_str == "consistent") {
+        mode = prevail::ObservationCheckMode::consistent;
+    } else {
+        return {.ok = false, .message = "Unknown mode: " + mode_str};
+    }
+    return session_->live_result->check_observation_at_label(label, point, observation, mode);
+}
+
+prevail::StringInvariant AnalysisEngine::get_live_invariant(const prevail::Label& label,
+                                                            prevail::InvariantPoint point) const {
+    if (!session_ || !session_->live_result) {
+        return prevail::StringInvariant::bottom();
+    }
+    auto it = session_->live_result->invariants.find(label);
+    if (it == session_->live_result->invariants.end()) {
+        return prevail::StringInvariant::bottom();
+    }
+    const auto& abstract_state = (point == prevail::InvariantPoint::post) ? it->second.post : it->second.pre;
+    if (abstract_state.is_bottom()) {
+        return prevail::StringInvariant::bottom();
+    }
+    return abstract_state.to_set();
+}
+
+std::vector<prevail::FailureSlice>
+AnalysisEngine::compute_failure_slices(const std::string& elf_path, const std::string& section,
+                                       const std::string& program, const std::string& type,
+                                       const prevail::Program& prog, size_t max_slices, size_t max_steps) {
+    analyze(elf_path, section, program, type);
+
+    prevail::AnalysisResult::SliceParams params;
+    params.max_slices = max_slices;
+    params.max_steps = max_steps;
+    return session_->live_result->compute_failure_slices(prog, params);
+}
+
+prevail::FailureSlice AnalysisEngine::compute_slice_from_label(const std::string& elf_path, const std::string& section,
+                                                               const std::string& program, const std::string& type,
+                                                               const prevail::Program& prog,
+                                                               const prevail::Label& label,
+                                                               const prevail::RelevantState& seed, size_t max_steps) {
+    analyze(elf_path, section, program, type);
+
+    prevail::RelevantState effective_seed = seed;
+    if (effective_seed.registers.empty() && effective_seed.stack_offsets.empty()) {
+        for (const auto& a : prog.assertions_at(label)) {
+            for (const auto& reg : prevail::extract_assertion_registers(a)) {
+                effective_seed.registers.insert(reg);
+            }
+        }
+        if (effective_seed.registers.empty()) {
+            auto deps = prevail::extract_instruction_deps(prog.instruction_at(label), prevail::EbpfDomain::top());
+            for (const auto& reg : deps.regs_read) {
+                effective_seed.registers.insert(reg);
+            }
+        }
+    }
+
+    return session_->live_result->compute_slice_from_label(prog, label, effective_seed, max_steps);
+}
+
+} // namespace prevail
diff --git a/src/analysis_engine.hpp b/src/analysis_engine.hpp
new file mode 100644
index 000000000..87d8a86a2
--- /dev/null
+++ b/src/analysis_engine.hpp
@@ -0,0 +1,158 @@
+// Copyright (c) Prevail Verifier contributors.
+// SPDX-License-Identifier: MIT
+#pragma once
+
+/// @file Analysis engine: runs the PREVAIL pipeline and holds a single live session.
+
+#include "platform_ops.hpp"
+
+#ifdef _MSC_VER
+#pragma warning(push)
+#pragma warning(disable : 4267) // Conversion from 'size_t' to 'int'.
+#endif
+
+#include "cfg/cfg.hpp"
+#include "result.hpp"
+#include "string_constraints.hpp"
+
+#ifdef _MSC_VER
+#pragma warning(pop)
+#endif
+
+#include <filesystem>
+#include <map>
+#include <memory>
+#include <optional>
+#include <string>
+#include <vector>
+
+namespace prevail {
+
+/// Holds all outputs from a single verification run.
+/// The session is always "live" — it retains both pre-serialized invariants
+/// (for callers that iterate or display them) and the live AnalysisResult with
+/// EbpfDomain objects (for check_constraint and backward slicing).
+/// Only one session exists at a time; analyzing a different program discards it.
+struct AnalysisSession {
+    std::string elf_path;
+    std::string section;
+    std::string program_name;
+
+    // The verifier options used for this session.
+    prevail::ebpf_verifier_options_t options;
+
+    // The instruction sequence (labels + instructions + btf_line_info).
+    prevail::InstructionSeq inst_seq;
+
+    // The CFG program (for instruction_at, assertions_at, cfg navigation).
+    prevail::Program program;
+
+    // Overall result metadata.
+    bool failed = false;
+    int max_loop_count = 0;
+    prevail::Interval exit_value = prevail::Interval::top();
+
+    /// Pre-serialized invariant data per label (serialized while TLS is alive).
+    struct SerializedInvariant {
+        prevail::StringInvariant pre;
+        prevail::StringInvariant post;
+        std::optional<std::string> error_message;  // VerificationError::what().
+        std::optional<prevail::Label> error_label; // VerificationError::where.
+        bool pre_is_bottom = false;
+    };
+    std::map<prevail::Label, SerializedInvariant> invariants;
+
+    // Derived: PC → source line info (built from BTF in InstructionSeq).
+    std::map<int, prevail::btf_line_info_t> pc_to_source;
+
+    // Derived: (file, line) → list of PCs.
+    std::map<std::pair<std::string, int>, std::vector<int>> source_to_pcs;
+
+    // Derived: PC → labels in the invariant map that have this PC as .from.
+    std::map<int, std::vector<prevail::Label>> pc_to_labels;
+
+    // Live state: TLS guard keeps variable_registry alive for EbpfDomain ops.
+    // live_result must be declared BEFORE tls_guard so it is destroyed FIRST
+    // (C++ destroys members in reverse declaration order), ensuring EbpfDomain
+    // objects are cleaned up while the thread-local state is still valid.
+    std::optional<prevail::AnalysisResult> live_result;
+    std::unique_ptr<prevail::ThreadLocalGuard> tls_guard;
+
+    // File modification time at analysis time (for staleness detection).
+    std::filesystem::file_time_type file_mtime;
+};
+
+/// Runs the PREVAIL pipeline and holds a single live session.
+/// Re-analyzes when a different program or different options are requested.
+class AnalysisEngine {
+  public:
+    explicit AnalysisEngine(PlatformOps* ops);
+
+    /// Run analysis on the given ELF file (or return the current session if it
+    /// matches). Keeps TLS alive so check_constraint and slicing work without
+    /// re-analyzing.
+    ///
+    /// @param options  Verifier options. When null, uses platform defaults.
+    ///                 Only the fields that affect analysis results
+    ///                 (check_for_termination, allow_division_by_zero, strict)
+    ///                 are compared for cache invalidation; verbosity and other
+    ///                 flags are passed through to the verifier without affecting
+    ///                 session caching.
+    /// @param type     Optional program type name override (e.g. "xdp", "bind").
+    /// @throws std::runtime_error on ELF parse, unmarshal, or analysis failure.
+    const AnalysisSession& analyze(const std::string& elf_path, const std::string& section = "",
+                                   const std::string& program = "", const std::string& type = "",
+                                   const prevail::ebpf_verifier_options_t* options = nullptr);
+
+    /// Check constraints against the live AnalysisResult (re-analyzes if needed).
+    /// @param mode_str  "consistent", "entailed", or "proven".
+    prevail::ObservationCheckResult check_constraint(const std::string& elf_path, const std::string& section,
+                                                     const std::string& program, const std::string& type,
+                                                     const prevail::Label& label, prevail::InvariantPoint point,
+                                                     const prevail::StringInvariant& observation,
+                                                     const std::string& mode_str);
+
+    /// Get the invariant at a label from the live session (calls to_set() on demand).
+    /// @returns StringInvariant::bottom() if no session, label not found, or state is bottom.
+    prevail::StringInvariant get_live_invariant(const prevail::Label& label, prevail::InvariantPoint point) const;
+
+    /// Compute failure slices from the live session (re-analyzes if needed).
+    std::vector<prevail::FailureSlice> compute_failure_slices(const std::string& elf_path, const std::string& section,
+                                                              const std::string& program, const std::string& type,
+                                                              const prevail::Program& prog, size_t max_slices = 1,
+                                                              size_t max_steps = 200);
+
+    /// Compute a backward slice from an arbitrary label (re-analyzes if needed).
+    prevail::FailureSlice compute_slice_from_label(const std::string& elf_path, const std::string& section,
+                                                   const std::string& program, const std::string& type,
+                                                   const prevail::Program& prog, const prevail::Label& label,
+                                                   const prevail::RelevantState& seed = {}, size_t max_steps = 200);
+
+    /// List all programs in an ELF file.
+    std::vector<ProgramEntry> list_programs(const std::string& elf_path);
+
+    /// Get the verifier options used for the current session.
+    /// Returns platform defaults if no session exists.
+    const prevail::ebpf_verifier_options_t& session_options() const;
+
+    /// Get the platform pointer.
+    const prevail::ebpf_platform_t* platform() const { return ops_->platform(); }
+
+    /// Get the platform ops.
+    PlatformOps* ops() const { return ops_; }
+
+  private:
+    /// Check if the current session matches the requested program and options.
+    bool session_matches(const std::string& elf_path, const std::string& section, const std::string& program,
+                         const std::string& type, const prevail::ebpf_verifier_options_t& options) const;
+
+    /// Check if two option sets produce the same analysis results.
+    static bool analysis_options_equal(const prevail::ebpf_verifier_options_t& a,
+                                       const prevail::ebpf_verifier_options_t& b);
+
+    PlatformOps* ops_;
+    std::optional<AnalysisSession> session_;
+    std::string session_type_;          // Program type override used for the current session.
+};
+
+} // namespace prevail
diff --git a/src/platform_ops.hpp b/src/platform_ops.hpp
new file mode 100644
index 000000000..0d93f50aa
--- /dev/null
+++ b/src/platform_ops.hpp
@@ -0,0 +1,104 @@
+// Copyright (c) Prevail Verifier contributors.
+// SPDX-License-Identifier: MIT
+#pragma once
+
+/// @file Platform abstraction for the analysis engine.
+/// Implementations provide platform-specific ELF validation, program enumeration,
+/// TLS management, and verifier options. This allows the analysis engine to work
+/// with different eBPF platforms (Linux, Windows) without compile-time dependencies.
+
+// Undef Windows macros that conflict with PREVAIL headers (std::numeric_limits::min/max).
+#undef FALSE
+#undef TRUE
+#undef min
+#undef max
+
+// Pre-define the include guard for bpf_conformance's ebpf_inst.h to prevent it
+// from being included (its EbpfInst struct conflicts with prevail::EbpfInst).
+#ifndef BPF_CONFORMANCE_CORE_EBPF_INST_H
+#define BPF_CONFORMANCE_CORE_EBPF_INST_H
+#endif
+
+#ifdef _MSC_VER
+#pragma warning(push)
+#pragma warning(disable : 4100) // Unreferenced formal parameter.
+#pragma warning(disable : 4244) // Conversion, possible loss of data.
+#pragma warning(disable : 4267) // Conversion from 'size_t' to 'int'.
+#pragma warning(disable : 4458) // Declaration hides class member.
+#pragma warning(disable : 26439) // Function may not throw.
+#pragma warning(disable : 26450) // Arithmetic overflow.
+#pragma warning(disable : 26451) // Arithmetic overflow.
+#pragma warning(disable : 26495) // Always initialize a member variable.
+#endif
+
+#include "ebpf_verifier.hpp"
+
+#ifdef _MSC_VER
+#pragma warning(pop)
+#endif
+
+#ifdef _WIN32
+#define FALSE 0
+#define TRUE 1
+#endif
+
+#include <stdexcept>
+#include <string>
+#include <vector>
+
+namespace prevail {
+
+/// Entry in the program list returned by PlatformOps::list_programs().
+struct ProgramEntry
+{
+    std::string section;
+    std::string function;
+};
+
+/// Abstract interface for platform-specific operations.
+/// The analysis engine calls through this interface instead of directly using
+/// platform-specific APIs.
+struct PlatformOps
+{
+    virtual ~PlatformOps() = default;
+
+    /// Get the PREVAIL platform pointer for read_elf/unmarshal/analyze.
+    [[nodiscard]] virtual const prevail::ebpf_platform_t*
+    platform() const = 0;
+
+    /// List all programs (sections + function names) in an ELF file.
+    [[nodiscard]] virtual std::vector<ProgramEntry>
+    list_programs(const std::string& elf_path) = 0;
+
+    /// Validate ELF data before analysis.
+    /// @return true if valid (or if no validation is available).
+    virtual bool
+    validate_elf(const std::string& /*data*/)
+    {
+        return true;
+    }
+
+    /// Prepare thread-local state before analysis.
+    /// Clears any cached TLS data and optionally sets a program type override.
+    virtual void
+    prepare_tls(const std::string& type_override) = 0;
+
+    /// Get default verifier options for this platform.
+    [[nodiscard]] virtual prevail::ebpf_verifier_options_t
+    default_options() = 0;
+
+    /// Attempt fallback verification to produce a clean error message
+    /// when direct PREVAIL analysis fails (e.g. due to access violation on Windows).
+    /// @return Error message string, or empty string if no fallback is available.
+    virtual std::string
+    fallback_verify(
+        const std::string& /*data*/,
+        const std::string& /*section*/,
+        const std::string& /*program*/,
+        const std::string& /*type*/)
+    {
+        return "";
+    }
+};
+
+} // namespace prevail
diff --git a/src/platform_ops_prevail.hpp b/src/platform_ops_prevail.hpp
new file mode 100644
index 000000000..e4b477f27
--- /dev/null
+++ b/src/platform_ops_prevail.hpp
@@ -0,0 +1,60 @@
+// Copyright (c) Prevail Verifier contributors.
+// SPDX-License-Identifier: MIT
+#pragma once
+
+/// @file Linux/portable PlatformOps implementation using only PREVAIL APIs.
+
+#include "platform_ops.hpp"
+
+namespace prevail {
+
+/// PlatformOps implementation using only PREVAIL's public API.
+/// Works on Linux and Windows (when linking the PREVAIL library directly
+/// without ebpf-for-windows).
+class PrevailPlatformOps : public PlatformOps
+{
+  public:
+    explicit PrevailPlatformOps(const prevail::ebpf_platform_t* platform) : platform_(*platform) {}
+    explicit PrevailPlatformOps(prevail::ebpf_platform_t platform) : platform_(platform) {}
+
+    [[nodiscard]] const prevail::ebpf_platform_t*
+    platform() const override
+    {
+        return &platform_;
+    }
+
+    [[nodiscard]] std::vector<ProgramEntry>
+    list_programs(const std::string& elf_path) override
+    {
+        prevail::ElfObject elf(elf_path, default_options(), &platform_);
+        std::vector<ProgramEntry> result;
+        for (const auto& info : elf.list_programs()) {
+            if (prevail::ElfObject::is_valid(info)) {
+                result.push_back({info.section_name, info.function_name});
+            }
+        }
+        return result;
+    }
+
+    void
+    prepare_tls(const std::string& /*type_override*/) override
+    {
+        prevail::ebpf_verifier_clear_thread_local_state();
+    }
+
+    [[nodiscard]] prevail::ebpf_verifier_options_t
+    default_options() override
+    {
+        prevail::ebpf_verifier_options_t opts{};
+        opts.mock_map_fds = true;
+        opts.setup_constraints = true;
+        opts.allow_division_by_zero = true;
+        opts.verbosity_opts.print_line_info = true;
+        return opts;
+    }
+
+  private:
+    prevail::ebpf_platform_t platform_;
+};
+
+} // namespace prevail
diff --git a/src/result.cpp b/src/result.cpp
index 39ab155e9..dd3e56f5f 100644
--- a/src/result.cpp
+++ b/src/result.cpp
@@ -377,269 +377,279 @@ std::set<Reg> extract_assertion_registers(const Assertion& assertion) {
         assertion);
 }
 
-std::vector<FailureSlice> AnalysisResult::compute_failure_slices(const Program& prog, const SliceParams params) const {
-    const auto max_steps = params.max_steps;
-    const auto max_slices = params.max_slices;
-    std::vector<FailureSlice> slices;
-
-    // Find all labels with errors
-    for (const auto& [label, inv_pair] : invariants) {
-        if (inv_pair.pre.is_bottom()) {
-            continue; // Unreachable
-        }
-        if (!inv_pair.error) {
-            continue; // No error here
-        }
-
-        // Check if we've reached the max slices limit
-        if (max_slices > 0 && slices.size() >= max_slices) {
-            break;
-        }
-
-        FailureSlice slice{
-            .failing_label = label,
-            .error = *inv_pair.error,
-            .relevance = {},
-        };
-
-        // Seed relevant registers from the actual failing assertion.
-        // Forward analysis stops at the first failing assertion, which may not be
-        // assertions[0]. Replay the checks against the pre-state to identify
-        // the actual failing assertion and seed relevance from it.
-        RelevantState initial_relevance;
-        const auto& assertions = prog.assertions_at(label);
-        bool found_failing = false;
-        for (const auto& assertion : assertions) {
-            if (ebpf_domain_check(inv_pair.pre, assertion, label)) {
-                for (const auto& reg : extract_assertion_registers(assertion)) {
-                    initial_relevance.registers.insert(reg);
-                }
-                found_failing = true;
-                break;
-            }
-        }
-        // Fallback: if no failing assertion was identified (shouldn't happen),
-        // or if the failing assertion has no register deps, aggregate all assertions.
-        if (!found_failing || initial_relevance.registers.empty()) {
-            for (const auto& assertion : assertions) {
-                for (const auto& reg : extract_assertion_registers(assertion)) {
-                    initial_relevance.registers.insert(reg);
-                }
-            }
-        }
+FailureSlice AnalysisResult::compute_slice_from_label(const Program& prog, const Label& label,
+                                                      const RelevantState& seed_relevance, size_t max_steps) const {
+    FailureSlice slice{
+        .failing_label = label,
+        .error = VerificationError(""),
+        .relevance = {},
+    };
+
+    // Copy error if present at this label.
+    const auto label_it = invariants.find(label);
+    if (label_it != invariants.end() && label_it->second.error) {
+        slice.error = *label_it->second.error;
+    }
 
-        // Always include the failing label in the slice, even if no registers were extracted
-        // (e.g., BoundedLoopCount has no register deps)
+    // `visited` tracks all explored labels for deduplication during backward traversal.
+    // `slice_labels` tracks only labels that interact with relevant registers (the output slice).
+    std::map<Label, RelevantState> visited;
+    std::set<Label> conservative_visited; // Dedup for empty-relevance labels in conservative mode
+    std::map<Label, RelevantState> slice_labels;
 
-        // `visited` tracks all explored labels for deduplication during backward traversal.
-        // `slice_labels` tracks only labels that interact with relevant registers (the output slice).
-        std::map<Label, RelevantState> visited;
-        std::set<Label> conservative_visited; // Dedup for empty-relevance labels in conservative mode
-        std::map<Label, RelevantState> slice_labels;
+    // Worklist: (label, relevant_state_after_this_label)
+    std::vector<std::pair<Label, RelevantState>> worklist;
+    worklist.emplace_back(label, seed_relevance);
 
-        // Worklist: (label, relevant_state_after_this_label)
-        std::vector<std::pair<Label, RelevantState>> worklist;
-        worklist.emplace_back(label, initial_relevance);
+    // When the seed has no register/stack deps (e.g., BoundedLoopCount),
+    // perform a conservative backward walk so the slice still shows the
+    // loop structure and control flow leading to the failure.
+    const bool conservative_mode = seed_relevance.registers.empty() && seed_relevance.stack_offsets.empty();
 
-        // When the seed has no register/stack deps (e.g., BoundedLoopCount),
-        // perform a conservative backward walk so the slice still shows the
-        // loop structure and control flow leading to the failure.
-        const bool conservative_mode = initial_relevance.registers.empty() && initial_relevance.stack_offsets.empty();
+    size_t steps = 0;
 
-        size_t steps = 0;
+    // Hoist the parent lookup for the target label outside the hot loop;
+    // it is invariant and parents_of() may return a temporary.
+    const auto parents_of_target = prog.cfg().parents_of(label);
 
-        // Hoist the parent lookup for the failing label outside the hot loop;
-        // it is invariant and parents_of() may return a temporary.
-        const auto parents_of_fail = prog.cfg().parents_of(label);
+    while (!worklist.empty() && steps < max_steps) {
+        auto [current_label, relevant_after] = worklist.back();
+        worklist.pop_back();
 
-        while (!worklist.empty() && steps < max_steps) {
-            auto [current_label, relevant_after] = worklist.back();
-            worklist.pop_back();
+        // Skip if nothing is relevant — unless we're in conservative mode
+        // (empty-seed assertions like BoundedLoopCount) or this is the target label.
+        if (!conservative_mode && current_label != label && relevant_after.registers.empty() &&
+            relevant_after.stack_offsets.empty()) {
+            continue;
+        }
 
-            // Skip if nothing is relevant — unless we're in conservative mode
-            // (empty-seed assertions like BoundedLoopCount) or this is the failing label.
-            if (!conservative_mode && current_label != label && relevant_after.registers.empty() &&
-                relevant_after.stack_offsets.empty()) {
+        // Merge with existing relevance at this label (for deduplication)
+        auto& existing = visited[current_label];
+        const size_t prev_size = existing.registers.size() + existing.stack_offsets.size();
+        existing.registers.insert(relevant_after.registers.begin(), relevant_after.registers.end());
+        existing.stack_offsets.insert(relevant_after.stack_offsets.begin(), relevant_after.stack_offsets.end());
+        const size_t new_size = existing.registers.size() + existing.stack_offsets.size();
+
+        // If no new relevance was added, skip (already processed with same or broader relevance).
+        // In conservative mode with empty relevance, use a separate visited set for dedup.
+        if (new_size == prev_size) {
+            if (prev_size > 0) {
                 continue;
             }
-
-            // Merge with existing relevance at this label (for deduplication)
-            auto& existing = visited[current_label];
-            const size_t prev_size = existing.registers.size() + existing.stack_offsets.size();
-            existing.registers.insert(relevant_after.registers.begin(), relevant_after.registers.end());
-            existing.stack_offsets.insert(relevant_after.stack_offsets.begin(), relevant_after.stack_offsets.end());
-            const size_t new_size = existing.registers.size() + existing.stack_offsets.size();
-
-            // If no new relevance was added, skip (already processed with same or broader relevance).
-            // In conservative mode with empty relevance, use a separate visited set for dedup.
-            if (new_size == prev_size) {
-                if (prev_size > 0) {
-                    continue;
-                }
-                // Empty relevance (conservative mode): skip if we already visited this label
-                if (!conservative_visited.insert(current_label).second) {
-                    continue;
-                }
+            // Empty relevance (conservative mode): skip if we already visited this label
+            if (!conservative_visited.insert(current_label).second) {
+                continue;
             }
+        }
 
-            // Compute what's relevant BEFORE this instruction using deps
-            RelevantState relevant_before;
-            const auto inv_it = invariants.find(current_label);
-            if (inv_it != invariants.end() && inv_it->second.deps) {
-                const auto& deps = *inv_it->second.deps;
+        // Compute what's relevant BEFORE this instruction using deps
+        RelevantState relevant_before;
+        const auto inv_it = invariants.find(current_label);
+        if (inv_it != invariants.end() && inv_it->second.deps) {
+            const auto& deps = *inv_it->second.deps;
 
-                // Start with what's relevant after
-                relevant_before = relevant_after;
+            // Start with what's relevant after
+            relevant_before = relevant_after;
 
-                // Remove registers that are written by this instruction
-                // (they weren't relevant before their definition)
-                for (const auto& reg : deps.regs_written) {
-                    relevant_before.registers.erase(reg);
-                }
+            // Remove registers that are written by this instruction
+            // (they weren't relevant before their definition)
+            for (const auto& reg : deps.regs_written) {
+                relevant_before.registers.erase(reg);
+            }
 
-                // Remove registers that are clobbered (killed without reading).
-                // These stop propagation for post-instruction uses but don't add read-deps.
-                for (const auto& reg : deps.regs_clobbered) {
-                    relevant_before.registers.erase(reg);
-                }
+            // Remove registers that are clobbered (killed without reading).
+            // These stop propagation for post-instruction uses but don't add read-deps.
+            for (const auto& reg : deps.regs_clobbered) {
+                relevant_before.registers.erase(reg);
+            }
 
-                // Determine if this instruction contributes to the slice.
-                // An instruction contributes when it writes to a relevant register/stack slot,
-                // or when it is a control-flow decision (Jmp/Assume) that reads relevant registers.
-                bool instruction_contributes = false;
-                for (const auto& reg : deps.regs_written) {
-                    if (relevant_after.registers.contains(reg)) {
-                        instruction_contributes = true;
-                        break;
-                    }
+            // Determine if this instruction contributes to the slice.
+            // An instruction contributes when it writes to a relevant register/stack slot,
+            // or when it is a control-flow decision (Jmp/Assume) that reads relevant registers.
+            bool instruction_contributes = false;
+            for (const auto& reg : deps.regs_written) {
+                if (relevant_after.registers.contains(reg)) {
+                    instruction_contributes = true;
+                    break;
                 }
-                for (const auto& offset : deps.stack_written) {
-                    if (relevant_after.stack_offsets.contains(offset)) {
-                        instruction_contributes = true;
-                        break;
-                    }
+            }
+            for (const auto& offset : deps.stack_written) {
+                if (relevant_after.stack_offsets.contains(offset)) {
+                    instruction_contributes = true;
+                    break;
                 }
+            }
 
-                // Control-flow instructions (Jmp/Assume) that read relevant registers
-                // contribute to the slice because they shape the path to the failure.
-                if (!instruction_contributes) {
-                    const auto& ins = prog.instruction_at(current_label);
-                    if (std::holds_alternative<Jmp>(ins) || std::holds_alternative<Assume>(ins)) {
-                        for (const auto& reg : deps.regs_read) {
-                            if (relevant_after.registers.contains(reg)) {
-                                instruction_contributes = true;
-                                break;
-                            }
+            // Control-flow instructions (Jmp/Assume) that read relevant registers
+            // contribute to the slice because they shape the path to the target.
+            if (!instruction_contributes) {
+                const auto& ins = prog.instruction_at(current_label);
+                if (std::holds_alternative<Jmp>(ins) || std::holds_alternative<Assume>(ins)) {
+                    for (const auto& reg : deps.regs_read) {
+                        if (relevant_after.registers.contains(reg)) {
+                            instruction_contributes = true;
+                            break;
                         }
                     }
                 }
+            }
 
-                // Immediate path guard: when the current label is a direct predecessor
-                // of the failing label and is an Assume instruction, its condition
-                // registers are causally relevant — they determine reachability.
-                if (std::holds_alternative<Assume>(prog.instruction_at(current_label))) {
-                    if (std::find(parents_of_fail.begin(), parents_of_fail.end(), current_label) !=
-                        parents_of_fail.end()) {
-                        instruction_contributes = true;
-                    }
-                }
-
-                // At the failing label, the assertion depends on registers the instruction
-                // reads (e.g., base pointer r3 in a store). Since stores write to memory
-                // not registers, instruction_contributes would be false without this.
-                if (current_label == label) {
+            // Immediate path guard: when the current label is a direct predecessor
+            // of the target label and is an Assume instruction, its condition
+            // registers are causally relevant — they determine reachability.
+            if (std::holds_alternative<Assume>(prog.instruction_at(current_label))) {
+                if (std::find(parents_of_target.begin(), parents_of_target.end(), current_label) !=
+                    parents_of_target.end()) {
                     instruction_contributes = true;
                 }
+            }
 
-                // In conservative mode (empty seed, e.g., BoundedLoopCount), include all
-                // reachable labels so the slice shows the loop structure and control flow.
-                if (conservative_mode) {
-                    instruction_contributes = true;
-                }
+            // At the target label, the assertion depends on registers the instruction
+            // reads (e.g., base pointer r3 in a store). Since stores write to memory
+            // not registers, instruction_contributes would be false without this.
+            if (current_label == label) {
+                instruction_contributes = true;
+            }
 
-                if (instruction_contributes) {
-                    for (const auto& reg : deps.regs_read) {
-                        relevant_before.registers.insert(reg);
-                    }
-                    for (const auto& offset : deps.stack_read) {
-                        relevant_before.stack_offsets.insert(offset);
-                    }
-                }
+            // In conservative mode (empty seed, e.g., BoundedLoopCount), include all
+            // reachable labels so the slice shows the loop structure and control flow.
+            if (conservative_mode) {
+                instruction_contributes = true;
+            }
 
-                // Remove stack locations that are written by this instruction,
-                // but preserve offsets that are also read (read-modify-write, e.g., Atomic).
-                // Done before storing to slice_labels for consistency with register handling
-                // (written registers are removed before storage at lines 476-478).
-                for (const auto& offset : deps.stack_written) {
-                    if (!deps.stack_read.contains(offset)) {
-                        relevant_before.stack_offsets.erase(offset);
-                    }
+            if (instruction_contributes) {
+                for (const auto& reg : deps.regs_read) {
+                    relevant_before.registers.insert(reg);
                 }
+                for (const auto& offset : deps.stack_read) {
+                    relevant_before.stack_offsets.insert(offset);
+                }
+            }
 
-                if (instruction_contributes) {
-                    // Only include contributing labels in the output slice.
-                    // Store relevant_before so pre-invariant filtering shows the
-                    // instruction's read-deps (the true upstream dependencies).
-                    slice_labels[current_label] = relevant_before;
+            // Remove stack locations that are written by this instruction,
+            // but preserve offsets that are also read (read-modify-write, e.g., Atomic).
+            for (const auto& offset : deps.stack_written) {
+                if (!deps.stack_read.contains(offset)) {
+                    relevant_before.stack_offsets.erase(offset);
                 }
-            } else {
-                // No deps available: conservatively treat this label as contributing
-                // and propagate all current relevance to predecessors.
-                relevant_before = relevant_after;
-                slice_labels[current_label] = relevant_before;
             }
 
-            // Add predecessors to worklist
-            for (const auto& parent : prog.cfg().parents_of(current_label)) {
-                worklist.emplace_back(parent, relevant_before);
+            if (instruction_contributes) {
+                // Only include contributing labels in the output slice.
+                // Merge (not assign) because a label may be revisited from
+                // a different successor with additional relevance.
+                auto& existing = slice_labels[current_label];
+                existing.registers.insert(relevant_before.registers.begin(), relevant_before.registers.end());
+                existing.stack_offsets.insert(relevant_before.stack_offsets.begin(),
+                                             relevant_before.stack_offsets.end());
             }
+        } else {
+            // No deps available: conservatively treat this label as contributing
+            // and propagate all current relevance to predecessors.
+            relevant_before = relevant_after;
+            auto& existing = slice_labels[current_label];
+            existing.registers.insert(relevant_before.registers.begin(), relevant_before.registers.end());
+            existing.stack_offsets.insert(relevant_before.stack_offsets.begin(),
+                                         relevant_before.stack_offsets.end());
+        }
 
-            ++steps;
+        // Add predecessors to worklist
+        for (const auto& parent : prog.cfg().parents_of(current_label)) {
+            worklist.emplace_back(parent, relevant_before);
         }
 
-        // Expand join points: for any traversed label that is a join point
-        // (≥2 predecessors) where at least one predecessor is already in the slice,
-        // add the join-point label itself and all predecessors that have invariants.
-        // This ensures the causal trace shows converging paths that cause precision loss.
-        // Note: predecessors may not be in `visited` if the worklist budget was exhausted
-        // before reaching them, so we check the invariant map directly.
-        std::map<Label, RelevantState> join_expansion;
-        for (const auto& [v_label, v_relevance] : visited) {
-            const auto& parents = prog.cfg().parents_of(v_label);
-            if (parents.size() < 2) {
-                continue;
-            }
-            // Check that at least one predecessor is in the slice (this join is relevant)
-            bool has_slice_parent = false;
-            for (const auto& parent : parents) {
-                if (slice_labels.contains(parent)) {
-                    has_slice_parent = true;
-                    break;
-                }
+        ++steps;
+    }
+
+    // Expand join points: for any traversed label that is a join point
+    // (≥2 predecessors) where at least one predecessor is already in the slice,
+    // add the join-point label itself and all predecessors that have invariants.
+    // This ensures the causal trace shows converging paths that cause precision loss.
+    // Note: predecessors may not be in `visited` if the worklist budget was exhausted
+    // before reaching them, so we check the invariant map directly.
+    std::map<Label, RelevantState> join_expansion;
+    for (const auto& [v_label, v_relevance] : visited) {
+        const auto& parents = prog.cfg().parents_of(v_label);
+        if (parents.size() < 2) {
+            continue;
+        }
+        // Check that at least one predecessor is in the slice (this join is relevant)
+        bool has_slice_parent = false;
+        for (const auto& parent : parents) {
+            if (slice_labels.contains(parent)) {
+                has_slice_parent = true;
+                break;
             }
-            if (!has_slice_parent) {
+        }
+        if (!has_slice_parent) {
+            continue;
+        }
+        // Include the join-point label itself so the printing code can display
+        // per-predecessor state at this join.
+        if (!slice_labels.contains(v_label)) {
+            join_expansion[v_label] = v_relevance;
+        }
+        // Include all predecessors so the join display is complete.
+        // Use visited relevance if available, otherwise use the join-point's relevance.
+        for (const auto& parent : parents) {
+            if (slice_labels.contains(parent) || join_expansion.contains(parent)) {
                 continue;
             }
-            // Include the join-point label itself so the printing code can display
-            // per-predecessor state at this join.
-            if (!slice_labels.contains(v_label)) {
-                join_expansion[v_label] = v_relevance;
+            const auto& rel = visited.contains(parent) ? visited.at(parent) : v_relevance;
+            join_expansion[parent] = rel;
+        }
+    }
+    slice_labels.insert(join_expansion.begin(), join_expansion.end());
+
+    // Build the slice from contributing labels only
+    slice.relevance = std::move(slice_labels);
+    return slice;
+}
+
+std::vector<FailureSlice> AnalysisResult::compute_failure_slices(const Program& prog, const SliceParams params) const {
+    const auto max_slices = params.max_slices;
+    std::vector<FailureSlice> slices;
+
+    for (const auto& [label, inv_pair] : invariants) {
+        if (inv_pair.pre.is_bottom()) {
+            continue;
+        }
+        if (!inv_pair.error) {
+            continue;
+        }
+        if (max_slices > 0 && slices.size() >= max_slices) {
+            break;
+        }
+
+        // Seed relevant registers from the actual failing assertion.
+        // Forward analysis stops at the first failing assertion, which may not be
+        // assertions[0]. Replay the checks against the pre-state to identify
+        // the actual failing assertion and seed relevance from it.
+        RelevantState initial_relevance;
+        const auto& assertions = prog.assertions_at(label);
+        bool found_failing = false;
+        for (const auto& assertion : assertions) {
+            if (ebpf_domain_check(inv_pair.pre, assertion, label)) {
+                for (const auto& reg : extract_assertion_registers(assertion)) {
+                    initial_relevance.registers.insert(reg);
+                }
+                found_failing = true;
+                break;
             }
-            // Include all predecessors so the join display is complete.
-            // Use visited relevance if available, otherwise use the join-point's relevance.
-            for (const auto& parent : parents) {
-                if (slice_labels.contains(parent) || join_expansion.contains(parent)) {
-                    continue;
+        }
+        // Fallback: if no failing assertion was identified (shouldn't happen),
+        // aggregate all assertions. When the failing assertion was found but has
+        // no register deps, leave the seed empty so compute_slice_from_label
+        // enters conservative mode.
+        if (!found_failing) {
+            for (const auto& assertion : assertions) {
+                for (const auto& reg : extract_assertion_registers(assertion)) {
+                    initial_relevance.registers.insert(reg);
                 }
-                const auto& rel = visited.contains(parent) ? visited.at(parent) : v_relevance;
-                join_expansion[parent] = rel;
             }
         }
-        slice_labels.insert(join_expansion.begin(), join_expansion.end());
 
-        // Build the slice from contributing labels only
-        slice.relevance = std::move(slice_labels);
-        slices.push_back(std::move(slice));
+        slices.push_back(compute_slice_from_label(prog, label, initial_relevance, params.max_steps));
     }
 
     return slices;
diff --git a/src/result.hpp b/src/result.hpp
index 6d2e0f0ba..c351420bf 100644
--- a/src/result.hpp
+++ b/src/result.hpp
@@ -154,6 +154,18 @@ struct AnalysisResult {
     std::vector<FailureSlice> compute_failure_slices(const Program& prog) const {
         return compute_failure_slices(prog, SliceParams{});
     }
+
+    /// Compute a backward slice from an arbitrary label with a given seed relevance.
+    /// This is the general form used by both compute_failure_slices (for errors) and
+    /// the MCP server (for arbitrary-PC tracing).
+    /// @param prog The program CFG.
+    /// @param label The label to slice backward from.
+    /// @param seed_relevance The initial set of relevant registers/stack offsets.
+    /// @param max_steps Maximum worklist items to process.
+    /// @return A FailureSlice containing the impacted labels and per-label relevance.
+    [[nodiscard]]
+    FailureSlice compute_slice_from_label(const Program& prog, const Label& label, const RelevantState& seed_relevance,
+                                          size_t max_steps = 200) const;
 };
 
 void print_error(std::ostream& os, const VerificationError& error);