diff --git a/.github/workflows/pr_main.yaml b/.github/workflows/pr_main.yaml
index 3f80c0582..34cac9dc0 100644
--- a/.github/workflows/pr_main.yaml
+++ b/.github/workflows/pr_main.yaml
@@ -330,6 +330,24 @@ jobs:
         run: |
           make compile-programs-rust
 
+      - name: Cache compiled recursion guest ELF artifacts
+        id: cache-recursion-elfs
+        uses: actions/cache@v4
+        with:
+          path: executor/program_artifacts/recursion
+          key: recursion-elf-artifacts-${{ hashFiles('bench_vs/lambda/**', 'prover/src/**', 'prover/Cargo.toml', 'crypto/**/src/**', 'crypto/**/Cargo.toml', 'executor/src/**', 'executor/Cargo.toml', 'syscalls/**', 'executor/programs/riscv64im-lambda-vm-elf.json', 'Makefile') }}
+          restore-keys: |
+            recursion-elf-artifacts-
+
+      - name: Setup Rust Environment (recursion ELFs)
+        if: steps.cache-recursion-elfs.outputs.cache-hit != 'true' && steps.cache-rust-elfs.outputs.cache-hit == 'true'
+        uses: ./.github/actions/setup-rust
+
+      - name: Compile recursion guest ELFs
+        if: steps.cache-recursion-elfs.outputs.cache-hit != 'true'
+        run: |
+          make compile-recursion-elfs
+
       - name: Install nextest
         uses: taiki-e/install-action@v2
         with:
diff --git a/Makefile b/Makefile
index ee107bc2a..bf39496b9 100644
--- a/Makefile
+++ b/Makefile
@@ -52,9 +52,18 @@ BENCH_ARTIFACTS := $(addprefix $(BENCH_ARTIFACTS_DIR)/, $(addsuffix .elf, $(BENC
 # rather than executor/programs/. The recursion guest is the in-VM STARK verifier.
 RECURSION_GUESTS_DIR=./bench_vs/lambda
 RECURSION_ARTIFACTS_DIR=./executor/program_artifacts/recursion
-RECURSION_GUESTS := empty fibonacci recursion
+RECURSION_GUESTS := empty fibonacci
 RECURSION_ARTIFACTS := $(addprefix $(RECURSION_ARTIFACTS_DIR)/, $(addsuffix .elf, $(RECURSION_GUESTS)))
 
+# The recursion verifier itself (bench_vs/lambda/recursion) requires picking
+# exactly one of its `min`/`blowup8` Cargo features at build time (fixes the
+# inner ProofOptions — see main.rs). Each preset builds its own distinctly
+# named [[bin]] (recursion-<preset>-bench) to its own artifact, via the
+# define/foreach/eval below rather than the generic %.elf pattern rule. The
+# distinct bin names also make the two `cp`s race-free under `make -j`.
+RECURSION_VERIFIER_PRESETS := min blowup8
+RECURSION_VERIFIER_ARTIFACTS := $(addprefix $(RECURSION_ARTIFACTS_DIR)/recursion-, $(addsuffix .elf, $(RECURSION_VERIFIER_PRESETS)))
+
 # Override with: make ... SYSROOT_DIR=$HOME/.lambda-vm-sysroot
 # to install the sysroot in a user-writable location and avoid sudo.
 SYSROOT_DIR ?= /opt/lambda-vm-sysroot
@@ -142,13 +151,13 @@ compile-programs-rust: prepare-sysroot $(RUST_ARTIFACTS)
 
 compile-bench: prepare-sysroot $(BENCH_ARTIFACTS)
 
-# NOTE: the recursion smoke tests are #[ignore]d (not run by `make test` /
-# `test-executor`) because they're too slow for CI today; only `test-prover-all`
-# runs them. We still compile their guest ELFs on every build so they keep
-# compiling until the tests are fast enough to run in CI.
+# NOTE: the recursion smoke tests read these prebuilt guest ELFs. The fast ones
+# run on every `cargo test` (so `make test`, which depends on this target, needs
+# them); the slow ones stay #[ignore]d (only `test-prover-all` runs them). We
+# compile the guest ELFs on every build so the tests always have them ready.
 compile-programs: compile-programs-asm compile-programs-rust compile-bench compile-recursion-elfs
 
-compile-recursion-elfs: prepare-sysroot $(RECURSION_ARTIFACTS)
+compile-recursion-elfs: prepare-sysroot $(RECURSION_ARTIFACTS) $(RECURSION_VERIFIER_ARTIFACTS)
 
 $(RECURSION_ARTIFACTS_DIR):
 	mkdir -p $@
@@ -167,21 +176,23 @@ $(BENCH_ARTIFACTS_DIR):
 FORCE:
 
 # The guest .elf rules all share one canned recipe: the cargo build invocation is
-# identical across the rust, bench, and recursion guests. They differ only in the
-# source directory ($(1)) and the built-binary name suffix ($(2): empty when the
-# binary == crate name, `-bench` for the recursion suite, whose crates are named
-# <name>-bench). cargo owns the dep graph (see FORCE above), so the recipe always
-# runs and lets cargo decide what to actually rebuild.
+# identical across the rust, bench, and recursion guests. They differ in the
+# crate directory ($(1), the full path — callers interpolate $* themselves, so
+# a target's stem needn't match its crate dir name, e.g. the recursion-verifier
+# presets below), the built binary's filename ($(2)), and optional extra cargo
+# args ($(3), e.g. `--features min`). cargo owns the dep graph (see FORCE
+# above), so the recipe always runs and lets cargo decide what to rebuild.
 define build_guest_elf
-cd $(1)/$* && \
+cd $(1) && \
 	CARGO_TARGET_DIR=$(abspath $(SHARED_TARGET_DIR)) \
 	CFLAGS_riscv64im_lambda_vm_elf="$(SYSROOT_CFLAGS)" \
 	rustup run nightly-2026-02-01 cargo build --release \
 		--target $(RV64_TARGET_SPEC) \
 		-Z build-std=core,alloc,std,compiler_builtins,panic_abort \
 		-Z build-std-features=compiler-builtins-mem \
-		-Z json-target-spec
-cp $(SHARED_TARGET_DIR)/riscv64im-lambda-vm-elf/release/$*$(2) $@
+		-Z json-target-spec \
+		$(3)
+cp $(SHARED_TARGET_DIR)/riscv64im-lambda-vm-elf/release/$(2) $@
 endef
 
 # Compile rust (64-bit)
@@ -191,18 +202,39 @@ endef
 # and fail to compile guest C dependencies). Order-only because prepare-sysroot is
 # .PHONY — a normal prereq would force a rebuild every time; its recipe is idempotent.
 $(RUST_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(RUST_ARTIFACTS_DIR)
-	$(call build_guest_elf,$(RUST_PROGRAMS_DIR),)
+	$(call build_guest_elf,$(RUST_PROGRAMS_DIR)/$*,$*)
 
 # Compile rust benches (64-bit)
 $(BENCH_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(BENCH_ARTIFACTS_DIR)
-	$(call build_guest_elf,$(BENCH_PROGRAMS_DIR),)
+	$(call build_guest_elf,$(BENCH_PROGRAMS_DIR)/$*,$*)
 
 # Recursion-suite guests (bench_vs/lambda/): the crate's binary is <name>-bench, so
 # copy <name>-bench -> <name>.elf. std-inclusive build-std covers both the no_std
 # inner guests and the std recursion verifier. Prover tests read these prebuilt
 # artifacts like every other program (see prover/src/tests/recursion_smoke_test.rs).
 $(RECURSION_ARTIFACTS_DIR)/%.elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
-	$(call build_guest_elf,$(RECURSION_GUESTS_DIR),-bench)
+	$(call build_guest_elf,$(RECURSION_GUESTS_DIR)/$*,$*-bench)
+
+# The recursion verifier's `min`/`blowup8` presets: same crate dir, one
+# differently named [[bin]] per preset (recursion-<preset>-bench, gated on that
+# preset's Cargo feature) -> a differently named artifact. Generated per preset
+# from RECURSION_VERIFIER_PRESETS via define/foreach/eval rather than a pattern
+# rule (the stem "recursion-min" wouldn't match the crate dir "recursion") and
+# rather than copy-paste (the presets list is the single source of truth).
+# $(1) is the preset; the recipe uses $$ so `$$(call build_guest_elf,...)`
+# survives the $(call ...) expansion and is expanded at recipe-run time (where
+# $@ is defined). Because the two bins have distinct filenames the post-build
+# `cp`s read different files, so the `make -j` cp race is gone structurally and
+# no `.NOTPARALLEL` is needed: cargo's target-dir lock already serializes the
+# compiles, and `.NOTPARALLEL` with prerequisites was wrong on every make
+# version anyway (it serializes the whole build on GNU make <= 4.3 — macOS ships
+# 3.81, ubuntu-latest 4.3 — and on >= 4.4 serializes only the listed targets'
+# own prerequisites, never the two ELF targets against each other).
+define recursion_verifier_rule
+$(RECURSION_ARTIFACTS_DIR)/recursion-$(1).elf: FORCE | prepare-sysroot $(RECURSION_ARTIFACTS_DIR)
+	$$(call build_guest_elf,$$(RECURSION_GUESTS_DIR)/recursion,recursion-$(1)-bench,--features $(1))
+endef
+$(foreach preset,$(RECURSION_VERIFIER_PRESETS),$(eval $(call recursion_verifier_rule,$(preset))))
 
 clean-asm:
 	-rm -rf $(ASM_ARTIFACTS_DIR)
@@ -261,21 +293,25 @@ test: compile-programs
 
 # === Quick test shortcuts ===
 
-# Fast prover tests (skips ignored slow tests)
-test-fast:
+# Fast prover tests (skips ignored slow tests). Recursion smoke/PoC tests read
+# prebuilt guest ELFs, so build them first.
+test-fast: compile-recursion-elfs
 	cargo test -p lambda-vm-prover -p stark -p executor -F stark/parallel
 
 # Prover tests only
-test-prover:
+test-prover: compile-recursion-elfs
 	cargo test -p lambda-vm-prover
 
-# Prover tests including slow ones. The recursion smoke tests (#[ignore]d) read
-# prebuilt guest ELFs from executor/program_artifacts/recursion/, so build them first.
+# Prover tests including slow ones. The recursion smoke tests read prebuilt
+# guest ELFs from executor/program_artifacts/recursion/ — the fast ones on every
+# run, the slow ones (still #[ignore]d) only under --include-ignored — so build
+# them first.
 test-prover-all: compile-recursion-elfs
 	cargo test -p lambda-vm-prover -- --include-ignored
 
-# Prover tests with debug-checks (shows bus balance report)
-test-prover-debug:
+# Prover tests with debug-checks (shows bus balance report). Also unfiltered, so
+# it runs the non-ignored recursion tests that read prebuilt guest ELFs.
+test-prover-debug: compile-recursion-elfs
 	cargo test -p lambda-vm-prover --features debug-checks -- --nocapture
 
 # Disk-spill tests (stark + prover). FORCE_DISK_SPILL is required by the prover tests.
@@ -305,7 +341,9 @@ test-cuda-fallback:
 # GPU + nvcc). The GPU CI counterpart of CPU CI's sharded prover tests. Single-threaded: the
 # GPU serializes proves and the dispatch counters are process-global. cuda on prover cascades
 # to stark; crypto/ecsm build without it (they have no GPU path).
-test-prover-cuda:
+# compile-recursion-elfs: this unfiltered run executes the non-ignored recursion
+# smoke tests, which read prebuilt guest ELFs; scripts/gpu_test.sh otherwise never builds them.
+test-prover-cuda: compile-recursion-elfs
 	cargo test --release -p lambda-vm-prover -p stark -p crypto -p ecsm \
 	    --features lambda-vm-prover/cuda -- --test-threads=1
 
diff --git a/bench_vs/lambda/recursion/Cargo.lock b/bench_vs/lambda/recursion/Cargo.lock
index 66048ba81..88a9fb605 100644
--- a/bench_vs/lambda/recursion/Cargo.lock
+++ b/bench_vs/lambda/recursion/Cargo.lock
@@ -412,6 +412,7 @@ dependencies = [
  "executor",
  "log",
  "math",
+ "postcard",
  "serde",
  "sha3",
  "stark",
diff --git a/bench_vs/lambda/recursion/Cargo.toml b/bench_vs/lambda/recursion/Cargo.toml
index 60f4cb1cc..4b5e1970b 100644
--- a/bench_vs/lambda/recursion/Cargo.toml
+++ b/bench_vs/lambda/recursion/Cargo.toml
@@ -5,6 +5,30 @@ name = "recursion-bench"
 version = "0.1.0"
 edition = "2024"
 
+[features]
+# Exactly one selects the fixed ProofOptions (see main.rs) — hardcoded, not
+# private input, so a malicious input can't downgrade the security level.
+# Cargo features are additive by design, so the compile_error! mutual-exclusion
+# guard in main.rs is the loud failure that stops a mislabeled artifact if both
+# ever get enabled at once (e.g. under `--all-features`). The crate must stay a
+# standalone `[workspace]` (not a root-workspace member) so root-level feature
+# unification can never turn both on.
+min = []
+blowup8 = []
+
+# One distinctly named binary per preset (selected by its feature) so a parallel
+# `make -j` builds them to different filenames — structurally race-free, no cp
+# clobbering. Both use src/main.rs; required-features gates each to its preset.
+[[bin]]
+name = "recursion-min-bench"
+path = "src/main.rs"
+required-features = ["min"]
+
+[[bin]]
+name = "recursion-blowup8-bench"
+path = "src/main.rs"
+required-features = ["blowup8"]
+
 [dependencies]
 lambda-vm-prover = { path = "../../../prover", default-features = false, features = [
     "profile-markers",
diff --git a/bench_vs/lambda/recursion/src/main.rs b/bench_vs/lambda/recursion/src/main.rs
index f19271aac..b91f2b841 100644
--- a/bench_vs/lambda/recursion/src/main.rs
+++ b/bench_vs/lambda/recursion/src/main.rs
@@ -1,44 +1,69 @@
 //! Naive recursion guest: verifies an inner lambda-vm proof inside the VM.
 //!
-//! Private input layout (postcard-encoded):
-//!   `(VmProof, Vec<u8>, ProofOptions)`
-//! where the `Vec<u8>` holds the inner program's ELF bytes and `ProofOptions`
-//! specifies the parameters the inner prover used. Commits `[1]` on success.
+//! Private input (postcard): `lambda_vm_prover::recursion::GuestInput` — the
+//! inner proof, the inner program's ELF bytes, and its precomputed DECODE and
+//! ELF-data-page commitments, supplied instead of recomputed in-VM.
 //!
-//! Not `no_std` (std/alloc are available — `build-std` provides them, and the
-//! prover links as a normal std crate; its prove-side code is dead-code
-//! eliminated since we only call `verify`). Like every other allocating guest
-//! it is `#![no_main]` and uses the syscalls crate's global allocator (a large
-//! `TlsfHeap`), initialized first thing in `main` — `verify` allocates far more
-//! than the target's default heap provides.
+//! `ProofOptions` is fixed by the `min`/`blowup8` Cargo feature (a `Preset`),
+//! not private input — an attacker could otherwise pick trivially weak options
+//! and have the guest accept as if a real proof had been checked.
+//!
+//! On success commits `program_id || inner_public_output` via
+//! `recursion::verify_and_attest` (a single ELF parse and a single full-ELF
+//! Keccak, shared between the statement absorb and the `program_id` fold). The
+//! attestation is not self-enforcing: the binding is established by the
+//! consumer via `recursion::check_attestation` (a host-side recompute+compare),
+//! never in-guest.
+//!
+//! std (not `no_std`): `build-std` provides it, prove-side code is DCE'd.
+//! `#![no_main]`; inits the syscalls global allocator first thing in `main`.
 
 #![no_main]
 
-use lambda_vm_prover::{ProofOptions, VmProof};
+use lambda_vm_prover::recursion::{GuestInput, Preset};
+
+#[cfg(not(any(feature = "min", feature = "blowup8")))]
+compile_error!("select exactly one of the `min`/`blowup8` features");
+#[cfg(all(feature = "min", feature = "blowup8"))]
+compile_error!("select exactly one of the `min`/`blowup8` features");
+
+/// The build preset fixing the inner `ProofOptions` (see the module docs).
+#[cfg(feature = "min")]
+const PRESET: Preset = Preset::Min;
+#[cfg(feature = "blowup8")]
+const PRESET: Preset = Preset::Blowup8;
 
 #[unsafe(export_name = "main")]
 pub fn main() -> ! {
     lambda_vm_syscalls::allocator::init_allocator();
 
-    // Install panic handler to make sure any OOM is because verifying itself is
-    // expensive rather than panics causing stack unwinding, which itself is very
-    // expensive in the guest.
+    // Panic -> sys_panic; unwinding is very expensive in-guest.
     const PANIC_MSG: &str = "PANICKED";
     std::panic::set_hook(Box::new(|_| unsafe {
         lambda_vm_syscalls::syscalls::sys_panic(PANIC_MSG.as_ptr(), PANIC_MSG.len())
     }));
 
     let blob = lambda_vm_syscalls::syscalls::get_private_input();
-    let (vm_proof, inner_elf, options): (VmProof, Vec<u8>, ProofOptions) =
+    let (vm_proof, inner_elf, decode_commitment, page_commitments): GuestInput =
         postcard::from_bytes(&blob).expect("failed to deserialize recursion input");
     lambda_vm_prover::profile_markers::step_marker::<
         { lambda_vm_prover::profile_markers::STEP_DECODE_DONE },
     >();
 
-    let ok = lambda_vm_prover::verify_with_options(&vm_proof, &inner_elf, &options, None, None)
-        .expect("verify errored");
-    assert!(ok, "inner proof failed verification");
-
-    lambda_vm_syscalls::syscalls::commit(&[1u8]);
+    // The guest's whole job: verify the inner proof against the supplied roots
+    // and, on success, produce `program_id || inner_public_output`. The id fold
+    // is what the consumer rebinds to a trusted ELF (`check_attestation`); it is
+    // not self-enforcing here.
+    let options = PRESET.options();
+    let attestation = lambda_vm_prover::recursion::verify_and_attest(
+        &vm_proof,
+        &inner_elf,
+        &options,
+        decode_commitment,
+        &page_commitments,
+    )
+    .expect("verify errored")
+    .expect("inner proof failed verification");
+    lambda_vm_syscalls::syscalls::commit(&attestation);
     lambda_vm_syscalls::syscalls::sys_halt();
 }
diff --git a/prover/Cargo.toml b/prover/Cargo.toml
index 57e8114d0..4a76a41bc 100644
--- a/prover/Cargo.toml
+++ b/prover/Cargo.toml
@@ -21,6 +21,9 @@ math = { path = "../crypto/math" }
 executor = { path = "../executor" }
 ecsm = { path = "../crypto/ecsm" }
 serde = { version = "1.0", features = ["derive"] }
+# The recursion guest-input blob codec (see `recursion::encode_guest_input`);
+# no_std+alloc, so the in-VM guest build (default-features = false) is fine.
+postcard = { version = "1.0", features = ["alloc"] }
 rayon = { version = "1.8.0", optional = true }
 sysinfo = { version = "0.31", default-features = false, features = ["system"] }
 log = "0.4"
@@ -30,7 +33,6 @@ sha3 = { version = "0.10.8", default-features = false }
 env_logger = "*"
 criterion = { version = "0.5", default-features = false }
 bincode = "1"
-postcard = { version = "1.0", features = ["alloc"] }
 tikv-jemallocator = "0.6"
 tikv-jemalloc-ctl = { version = "0.6", features = ["stats"] }
 tiny-keccak = { version = "2.0", features = ["keccak"] }
diff --git a/prover/src/lib.rs b/prover/src/lib.rs
index bd72a3670..49fd0bd30 100644
--- a/prover/src/lib.rs
+++ b/prover/src/lib.rs
@@ -20,6 +20,7 @@ mod debug_report;
 pub mod instruments;
 mod paged_mem;
 pub use stark::profile_markers;
+pub mod recursion;
 mod statement;
 pub mod tables;
 pub mod test_utils;
@@ -33,14 +34,13 @@ use crypto::fiat_shamir::is_transcript::IsTranscript;
 use executor::elf::Elf;
 use executor::vm::execution::Executor;
 use math::field::element::FieldElement;
-use stark::config::Commitment;
 use stark::prover::{IsStarkProver, Prover};
 #[cfg(feature = "disk-spill")]
 use stark::storage_mode::StorageMode;
 use stark::traits::AIR;
 use stark::verifier::{IsStarkVerifier, Verifier};
 
-use crate::statement::{StatementKind, absorb_statement};
+use crate::statement::{StatementKind, absorb_statement, absorb_statement_with_digest};
 pub use crate::tables::MaxRowsConfig;
 use crate::tables::bitwise;
 use crate::tables::decode;
@@ -59,8 +59,11 @@ use crate::test_utils::{
     create_register_air, create_shift_air, create_store_air,
 };
 
-// Re-exported so downstream verifier guests (e.g. the in-VM recursion guest) can
-// name the proof-options type carried in their private input alongside `VmProof`.
+// Re-exported for downstream hosts and verifier guests (e.g. the in-VM
+// recursion guest): `Commitment` is carried in the guest's private input
+// (see `recursion::GuestInput`); the proof-options types name the parameters
+// fixed at guest build time (`recursion::Preset`).
+pub use stark::config::Commitment;
 pub use stark::proof::options::{GoldilocksCubicProofOptions, ProofOptions};
 use stark::proof::stark::MultiProof;
 
@@ -199,6 +202,9 @@ pub enum Error {
     /// A non-final continuation epoch contains the program-terminating
     /// instruction. The terminating instruction must be in the final epoch.
     HaltInNonFinalEpoch,
+    /// Recursion host-side helper failed (guest-input encoding or
+    /// commitment recompute — see the `recursion` module).
+    Recursion(String),
 }
 
 impl fmt::Display for Error {
@@ -227,6 +233,7 @@ impl fmt::Display for Error {
                     "the program-terminating instruction must be in the final epoch"
                 )
             }
+            Error::Recursion(msg) => write!(f, "recursion helper error: {msg}"),
         }
     }
 }
@@ -414,36 +421,20 @@ impl VmAirs {
         refs
     }
 
-    /// Create all VM AIR instances. `minimal_bitwise` controls whether the full
-    /// 2^20 bitwise preprocessed table is included (false = full, true = minimal).
-    /// DECODE is always preprocessed.
+    /// Create all VM AIR instances. `minimal_bitwise` picks the minimal vs full
+    /// 2^20 bitwise preprocessed table. DECODE is always preprocessed.
+    /// `page_configs`/`table_counts` give the PAGE bases and split-table chunk
+    /// counts.
     ///
-    /// `page_configs` provides the page base addresses for creating PAGE AIRs.
-    /// `table_counts` specifies how many chunks for each split table.
+    /// `decode_commitment`/`page_commitments`, when `Some`, are used directly
+    /// (skipping the FFT + Merkle build) for the DECODE root and any matching
+    /// ELF-data page (keyed by `page_base`); `None` or unmatched pages recompute
+    /// from the ELF. Zero-init pages always use the shared compile-time constant.
     ///
-    /// `decode_commitment` is an optional precomputed DECODE preprocessed
-    /// commitment. When `Some`, the supplied value is used directly and the
-    /// FFT + Merkle build is skipped — useful for callers who have already
-    /// computed the commitment offline and embedded it as a compile-time
-    /// constant (e.g. the recursion guest, where the in-VM recompute is too
-    /// expensive). When `None`, the commitment is computed from the ELF.
-    ///
-    /// `page_commitments` is an optional list of precomputed ELF-data-page
-    /// preprocessed commitments, keyed by `page_base`. For each ELF data page
-    /// the verifier constructs, if a matching `(page_base, commitment)` pair
-    /// is supplied, it is used directly and that page's FFT + Merkle build is
-    /// skipped. Pages not in the list — including all zero-init pages and
-    /// pages without a match — take the normal compute path (zero-init pages
-    /// hit a compile-time constant via
-    /// `page::zero_init_preprocessed_commitment`; ELF data pages recompute
-    /// from the ELF). When `None`, every ELF data page recomputes from
-    /// scratch.
-    ///
-    /// The trust anchor for both `decode_commitment` and `page_commitments`
-    /// is the caller's compiled binary — never accept prover-supplied bytes
-    /// here. A wrong value is rejected, never silently accepted: it either
-    /// mismatches the prover's committed precomputed root (an explicit
-    /// verifier check) or yields diverging Fiat-Shamir challenges.
+    /// Supplied roots are used verbatim and NOT checked against `elf`. A wrong
+    /// caller-constant root is rejected (mismatches the proof root or diverges
+    /// Fiat-Shamir); a consistent prover-supplied mismatch is NOT — such
+    /// callers must bind identity externally (see `recursion::check_attestation`).
     #[allow(clippy::too_many_arguments)]
     pub fn new(
         elf: &Elf,
@@ -1003,34 +994,52 @@ pub fn verify(vm_proof: &VmProof, elf_bytes: &[u8]) -> Result<bool, Error> {
 /// ignoring the options embedded in the proof bundle. This prevents a
 /// malicious prover from weakening the security level.
 ///
-/// `decode_commitment` is an optional precomputed DECODE preprocessed
-/// commitment. When `Some`, the supplied value is used directly and the
-/// in-verifier FFT + Merkle build for the DECODE preprocessed columns is
-/// skipped — useful for callers (e.g. the recursion guest) that embed the
-/// commitment as a compile-time constant to avoid the in-VM recompute
-/// cost. When `None`, the verifier computes the commitment from the ELF.
-///
-/// `page_commitments` is an optional list of precomputed ELF-data-page
-/// preprocessed commitments, keyed by `page_base`. For each ELF data page
-/// the verifier constructs, if a matching `(page_base, commitment)` pair is
-/// supplied, the FFT + Merkle build for that page is skipped. Pages without
-/// a match — including all zero-init pages — take the normal compute path
-/// (zero-init pages hit a compile-time constant via
-/// `page::zero_init_preprocessed_commitment`; ELF data pages recompute
-/// from the ELF). When `None`, every ELF data page recomputes from scratch.
+/// `decode_commitment`/`page_commitments`, when `Some`, are used directly
+/// (skipping the in-verifier FFT + Merkle build) for the DECODE root and any
+/// ELF-data page matching by `page_base`; `None` or unmatched pages recompute
+/// from the ELF, and zero-init pages always use the shared compile-time
+/// constant. Callers (e.g. the recursion guest) supply these to avoid the
+/// in-VM recompute cost.
 ///
-/// Trust model: both `decode_commitment` and `page_commitments`, when
-/// supplied, must come from the caller's compiled binary (e.g. a
-/// `const [u8; 32]` and a `const [(u64, [u8; 32])]`), never from prover-
-/// supplied bytes. A wrong value is rejected, never silently accepted: it
-/// either mismatches the prover's committed precomputed root (an explicit
-/// verifier check) or yields diverging Fiat-Shamir challenges.
+/// Trust model: a supplied root is used verbatim — this function does NOT
+/// check it against `elf_bytes`. If it is a caller constant (from the compiled
+/// binary), a wrong value is rejected (it mismatches the proof's precomputed
+/// root or diverges Fiat-Shamir). If it is prover-supplied (e.g. the recursion
+/// guest's private input), a consistent mismatched root is NOT rejected here;
+/// the caller must bind identity externally (the recursion pipeline commits
+/// `recursion::program_id` and the consumer checks it via
+/// `recursion::check_attestation`).
 pub fn verify_with_options(
     vm_proof: &VmProof,
     elf_bytes: &[u8],
     proof_options: &ProofOptions,
     decode_commitment: Option<Commitment>,
     page_commitments: Option<&[(u64, Commitment)]>,
+) -> Result<bool, Error> {
+    let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?;
+    let elf_digest = statement::elf_digest(elf_bytes);
+    verify_prepared(
+        vm_proof,
+        &program,
+        &elf_digest,
+        proof_options,
+        decode_commitment,
+        page_commitments,
+    )
+}
+
+/// [`verify_with_options`] with the ELF already parsed and digested. Callers
+/// that need the parsed ELF or the digest for other purposes reuse them — the
+/// recursion attestation (`recursion::verify_and_attest`) shares one
+/// `Elf::load` and one full-ELF Keccak between verification and the
+/// `program_id` fold, which matters in-guest where both are expensive.
+pub(crate) fn verify_prepared(
+    vm_proof: &VmProof,
+    program: &Elf,
+    elf_digest: &[u8; 32],
+    proof_options: &ProofOptions,
+    decode_commitment: Option<Commitment>,
+    page_commitments: Option<&[(u64, Commitment)]>,
 ) -> Result<bool, Error> {
     // Validate table_counts before constructing AIRs.
     // A malicious prover could set counts to 0, removing entire constraint sets.
@@ -1048,9 +1057,8 @@ pub fn verify_with_options(
         }
     }
 
-    let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?;
     let page_configs = Traces::page_configs_from_elf_and_runtime(
-        &program,
+        program,
         &vm_proof.runtime_page_ranges,
         vm_proof.num_private_input_pages,
     );
@@ -1070,7 +1078,7 @@ pub fn verify_with_options(
     }
 
     let airs = VmAirs::new(
-        &program,
+        program,
         proof_options,
         false,
         &page_configs,
@@ -1091,10 +1099,10 @@ pub fn verify_with_options(
     // field makes this diverge from the prover's transcript state, so every
     // derived challenge differs and verification rejects.
     let mut transcript = DefaultTranscript::<E>::new(&[]);
-    absorb_statement(
+    absorb_statement_with_digest(
         &mut transcript,
         StatementKind::Monolithic,
-        elf_bytes,
+        elf_digest,
         &vm_proof.public_output,
         &vm_proof.table_counts,
         vm_proof.num_private_input_pages,
diff --git a/prover/src/recursion.rs b/prover/src/recursion.rs
new file mode 100644
index 000000000..0c290264b
--- /dev/null
+++ b/prover/src/recursion.rs
@@ -0,0 +1,309 @@
+//! Host and guest API for the naive (single-step) recursion pipeline.
+//!
+//! The recursion verifier guest (`bench_vs/lambda/recursion`) verifies an
+//! inner lambda-vm proof in-VM. Its private input ([`GuestInput`], built
+//! host-side by [`encode_guest_input`]) carries the inner program's
+//! precomputed DECODE/ELF-data-page roots so the guest skips the in-VM
+//! FFT + Merkle rebuild. `verify_with_options` uses supplied roots verbatim —
+//! it does NOT bind them to the inner ELF — so on success the guest commits
+//! an attestation that folds them into the identity instead:
+//! `program_id || inner_public_output` (see [`verify_and_attest`]).
+//!
+//! Trust model: the attestation is NOT self-enforcing. A consumer of the
+//! outer proof MUST recompute the id from the inner ELF it trusts and
+//! compare — that is [`check_attestation`]. A substituted root yields an id
+//! that differs from the honest recompute ([`expected_program_id`]), so the
+//! substitution `verify_with_options` cannot see is rejected here. The
+//! recompute is an expensive native FFT + Merkle pass, done once at the top
+//! level, never in-VM. `prover/src/tests/recursion_soundness_gap_poc.rs`
+//! demonstrates the attack this compare defeats.
+//!
+//! [`program_id`] deliberately does not fold the `ProofOptions`: the security
+//! level is pinned by which verifier guest the outer proof is checked against
+//! (`recursion-min.elf` vs `recursion-blowup8.elf`, fixed at build time — see
+//! [`Preset`]). A consumer must pin that outer ELF too, or a 1-query `min`
+//! attestation is indistinguishable from a 128-bit `blowup8` one.
+
+use executor::elf::Elf;
+use sha3::{Digest, Keccak256};
+
+use crate::statement::elf_digest;
+use crate::tables::trace_builder::Traces;
+use crate::{Commitment, Error, ProofOptions, VmProof};
+
+/// Smallest possible proof options (blowup=2, 1 query). Intentionally
+/// insecure — for cheap diagnostics, not soundness. The single source for the
+/// `recursion-min` guest build and the host tests that must match it.
+pub const MIN_PROOF_OPTIONS: ProofOptions = ProofOptions {
+    blowup_factor: 2,
+    fri_number_of_queries: 1,
+    coset_offset: 3,
+    grinding_factor: 1,
+    fri_final_poly_log_degree: 7,
+};
+
+/// The recursion verifier's build presets. Each fixes the guest's
+/// `ProofOptions` at build time (a Cargo feature — private input could
+/// otherwise downgrade the security level) and names the ELF artifact
+/// `make compile-recursion-elfs` produces. Deriving both from one value keeps
+/// a host from proving the inner under options the guest wasn't built for.
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+pub enum Preset {
+    /// Blowup=2, 1 query ([`MIN_PROOF_OPTIONS`]) — insecure, diagnostics only.
+    Min,
+    /// Blowup=8, multi-query — 128-bit security.
+    Blowup8,
+}
+
+impl Preset {
+    /// The fixed `ProofOptions` this preset's guest verifies with.
+    pub fn options(&self) -> ProofOptions {
+        match self {
+            Preset::Min => MIN_PROOF_OPTIONS,
+            Preset::Blowup8 => crate::GoldilocksCubicProofOptions::with_blowup(8)
+                .expect("blowup=8 is always valid"),
+        }
+    }
+
+    /// Artifact stem under `executor/program_artifacts/recursion/`
+    /// (`<stem>.elf`), matching the Makefile's preset rules.
+    pub fn artifact_stem(&self) -> &'static str {
+        match self {
+            Preset::Min => "recursion-min",
+            Preset::Blowup8 => "recursion-blowup8",
+        }
+    }
+
+    /// Short preset name (the Cargo feature that selects it).
+    pub fn name(&self) -> &'static str {
+        match self {
+            Preset::Min => "min",
+            Preset::Blowup8 => "blowup8",
+        }
+    }
+}
+
+/// The guest's private-input layout, postcard-encoded by
+/// [`encode_guest_input`] and decoded verbatim by the guest:
+/// `(inner proof, inner ELF bytes, DECODE root, ELF-data-page roots)`.
+pub type GuestInput = (VmProof, Vec<u8>, Commitment, Vec<(u64, Commitment)>);
+
+/// Precompute the DECODE and ELF-data-page preprocessed roots for `elf_bytes`
+/// under `opts` — the values the guest receives via private input instead of
+/// recomputing in-VM, and the values [`expected_program_id`] recomputes
+/// natively. Selection matches the verifier's page construction: every ELF
+/// data page (`init_values.is_some()`), keyed by `page_base`; zero-init pages
+/// use a compile-time constant and are never listed.
+pub fn precomputed_commitments(
+    elf_bytes: &[u8],
+    opts: &ProofOptions,
+) -> Result<(Commitment, Vec<(u64, Commitment)>), Error> {
+    let elf = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?;
+    let decode_commitment = crate::tables::decode::commitment_from_elf(&elf, opts)
+        .map_err(|e| Error::Recursion(format!("DECODE commitment from ELF: {e}")))?;
+    let page_commitments: Vec<(u64, Commitment)> = Traces::page_configs_from_elf(&elf)
+        .iter()
+        .filter(|c| c.init_values.is_some())
+        .map(|c| {
+            (
+                c.page_base,
+                crate::tables::page::compute_precomputed_commitment(c, opts),
+            )
+        })
+        .collect();
+    Ok((decode_commitment, page_commitments))
+}
+
+/// Build the guest's private-input blob for `inner_proof` of `inner_elf`:
+/// precomputes the roots and postcard-encodes the [`GuestInput`] tuple.
+pub fn encode_guest_input(
+    inner_proof: &VmProof,
+    inner_elf: &[u8],
+    opts: &ProofOptions,
+) -> Result<Vec<u8>, Error> {
+    let (decode_commitment, page_commitments) = precomputed_commitments(inner_elf, opts)?;
+    postcard::to_allocvec(&(
+        inner_proof,
+        inner_elf,
+        &decode_commitment,
+        &page_commitments,
+    ))
+    .map_err(|e| Error::Recursion(format!("postcard encode: {e}")))
+}
+
+/// Domain tag for [`program_id`].
+const PROGRAM_ID_TAG: &[u8] = b"LAMBDAVM_PROGRAM_ID_V1";
+
+/// [`program_id`] from a precomputed ELF digest and entry point — the guest
+/// path, sharing one full-ELF Keccak pass with the verify-side statement
+/// absorb (see [`verify_and_attest`]).
+pub fn program_id_from_digest(
+    elf_digest: &[u8; 32],
+    pc_start: u64,
+    decode_commitment: &Commitment,
+    page_commitments: &[(u64, Commitment)],
+) -> [u8; 32] {
+    let mut pages = page_commitments.to_vec();
+    pages.sort_by_key(|(base, _)| *base);
+
+    let mut h = Keccak256::new();
+    h.update(PROGRAM_ID_TAG);
+    h.update(elf_digest);
+    h.update(pc_start.to_le_bytes());
+    h.update(decode_commitment);
+    h.update((pages.len() as u64).to_le_bytes());
+    for (base, c) in &pages {
+        h.update(base.to_le_bytes());
+        h.update(c);
+    }
+    h.finalize().into()
+}
+
+/// Canonical program identity: a fold of the full ELF digest, entry point, and
+/// the supplied DECODE / ELF-data-page roots (folded in ascending `page_base`
+/// order). Folding the roots in makes a supplied-root substitution yield a
+/// different id than an honest native recompute — the binding is that compare
+/// ([`check_attestation`]).
+///
+/// `decode_commitment` needs no length prefix: [`Commitment`] is a fixed-size
+/// `[u8; COMMITMENT_SIZE]`, so its boundary in the hash input is unambiguous.
+/// Pages are self-delimiting too (count-prefixed, each entry a fixed
+/// `u64` base + fixed-size `Commitment`).
+pub fn program_id(
+    elf_bytes: &[u8],
+    pc_start: u64,
+    decode_commitment: &Commitment,
+    page_commitments: &[(u64, Commitment)],
+) -> [u8; 32] {
+    program_id_from_digest(
+        &elf_digest(elf_bytes),
+        pc_start,
+        decode_commitment,
+        page_commitments,
+    )
+}
+
+/// [`program_id`] with `pc_start` taken from `elf_bytes`' entry point.
+pub fn program_id_from_elf(
+    elf_bytes: &[u8],
+    decode_commitment: &Commitment,
+    page_commitments: &[(u64, Commitment)],
+) -> Result<[u8; 32], Error> {
+    let elf = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?;
+    Ok(program_id(
+        elf_bytes,
+        elf.entry_point,
+        decode_commitment,
+        page_commitments,
+    ))
+}
+
+/// Verify an inner proof against supplied roots and, on success, produce the
+/// attestation bytes the recursion guest commits:
+/// `program_id(elf, roots) || inner_public_output`. `Ok(None)` means the
+/// proof did not verify. This is the guest's whole job in one call; it does a
+/// single `Elf::load` and a single full-ELF Keccak, shared between the
+/// statement absorb and the `program_id` fold.
+///
+/// The attestation binds identity only for a consumer that recomputes the id
+/// from a trusted ELF ([`check_attestation`]) — see the module docs.
+pub fn verify_and_attest(
+    vm_proof: &VmProof,
+    elf_bytes: &[u8],
+    proof_options: &ProofOptions,
+    decode_commitment: Commitment,
+    page_commitments: &[(u64, Commitment)],
+) -> Result<Option<Vec<u8>>, Error> {
+    let program = Elf::load(elf_bytes).map_err(|e| Error::ElfLoad(format!("{e}")))?;
+    let digest = elf_digest(elf_bytes);
+    let ok = crate::verify_prepared(
+        vm_proof,
+        &program,
+        &digest,
+        proof_options,
+        Some(decode_commitment),
+        Some(page_commitments),
+    )?;
+    if !ok {
+        return Ok(None);
+    }
+    let id = program_id_from_digest(
+        &digest,
+        program.entry_point,
+        &decode_commitment,
+        page_commitments,
+    );
+    let mut attestation = id.to_vec();
+    attestation.extend_from_slice(&vm_proof.public_output);
+    Ok(Some(attestation))
+}
+
+/// Split committed attestation bytes into `(program_id, inner_public_output)`.
+/// `None` if too short to contain an id.
+pub fn split_attestation(committed: &[u8]) -> Option<([u8; 32], &[u8])> {
+    if committed.len() < 32 {
+        return None;
+    }
+    let id: [u8; 32] = committed[..32].try_into().ok()?;
+    Some((id, &committed[32..]))
+}
+
+/// The honest `program_id` for a trusted inner ELF under `opts`: recomputes
+/// the DECODE/page roots natively (the expensive FFT + Merkle pass) and folds
+/// them. Compute once per (ELF, opts) and reuse across proofs.
+pub fn expected_program_id(
+    trusted_elf_bytes: &[u8],
+    opts: &ProofOptions,
+) -> Result<[u8; 32], Error> {
+    let (decode_commitment, page_commitments) = precomputed_commitments(trusted_elf_bytes, opts)?;
+    program_id_from_elf(trusted_elf_bytes, &decode_commitment, &page_commitments)
+}
+
+/// The mandatory consumer-side binding check (see the module docs): split the
+/// guest's committed bytes, recompute the id from the ELF the *consumer*
+/// trusts, and compare. `Ok(Some(inner_public_output))` on match; `Ok(None)`
+/// if the bytes are malformed or attest a different (ELF, roots) identity —
+/// i.e. the inner proof was not for `trusted_elf_bytes` as the consumer knows
+/// it. The caller must also have verified the outer proof against the pinned
+/// `recursion-<preset>.elf` with `opts = preset.options()`.
+///
+/// This is the low-level primitive: it accepts any `opts`, including
+/// [`MIN_PROOF_OPTIONS`], and is meant for diagnostics/tests that need that
+/// escape hatch. Production consumers should go through
+/// [`check_attestation_for_preset`] instead, which refuses `Preset::Min`.
+pub fn check_attestation(
+    committed: &[u8],
+    trusted_elf_bytes: &[u8],
+    opts: &ProofOptions,
+) -> Result<Option<Vec<u8>>, Error> {
+    let Some((id, inner_public_output)) = split_attestation(committed) else {
+        return Ok(None);
+    };
+    if id != expected_program_id(trusted_elf_bytes, opts)? {
+        return Ok(None);
+    }
+    Ok(Some(inner_public_output.to_vec()))
+}
+
+/// [`check_attestation`] gated on [`Preset`] instead of a raw [`ProofOptions`],
+/// refusing `Preset::Min`: that preset (blowup=2, 1 query — [`MIN_PROOF_OPTIONS`])
+/// is intentionally insecure and exists only for cheap diagnostics. A real
+/// consumer pinning its trust to `recursion-min.elf` would accept a 1-query
+/// attestation as if it had 128-bit security. Diagnostics/benches that
+/// legitimately need `Preset::Min` call [`check_attestation`] directly with
+/// [`MIN_PROOF_OPTIONS`].
+pub fn check_attestation_for_preset(
+    committed: &[u8],
+    trusted_elf_bytes: &[u8],
+    preset: Preset,
+) -> Result<Option<Vec<u8>>, Error> {
+    if preset == Preset::Min {
+        return Err(Error::Recursion(
+            "Preset::Min (recursion-min.elf) is insecure (blowup=2, 1 query) and must not be \
+             used as a production consumer's trust gate; call check_attestation directly with \
+             MIN_PROOF_OPTIONS for diagnostics"
+                .to_string(),
+        ));
+    }
+    check_attestation(committed, trusted_elf_bytes, &preset.options())
+}
diff --git a/prover/src/statement.rs b/prover/src/statement.rs
index 87dab84cd..617d3d33d 100644
--- a/prover/src/statement.rs
+++ b/prover/src/statement.rs
@@ -18,7 +18,10 @@ use crate::{RuntimePageRange, TableCounts};
 /// Domain-separation tag. Bump the suffix (`_V2`, ...) on any encoding change.
 const DOMAIN_TAG: &[u8] = b"LAMBDAVM_STARK_STATEMENT_V3";
 
-fn elf_digest(elf: &[u8]) -> [u8; 32] {
+/// Canonical full-ELF identity digest — exactly what [`absorb_statement`] binds
+/// into the transcript. The recursion attestation folds the same digest into
+/// `program_id` (see the `recursion` module), sharing one pass over the ELF.
+pub(crate) fn elf_digest(elf: &[u8]) -> [u8; 32] {
     let mut h = Keccak256::new();
     h.update(elf);
     h.finalize().into()
@@ -46,6 +49,33 @@ pub(crate) fn absorb_statement(
     num_private_input_pages: usize,
     runtime_page_ranges: &[RuntimePageRange],
     fri_final_poly_log_degree: u8,
+) {
+    absorb_statement_with_digest(
+        t,
+        kind,
+        &elf_digest(elf_bytes),
+        public_output,
+        table_counts,
+        num_private_input_pages,
+        runtime_page_ranges,
+        fri_final_poly_log_degree,
+    )
+}
+
+/// [`absorb_statement`] with the ELF digest precomputed. Callers that already
+/// hold the digest reuse it instead of a second full-ELF Keccak pass — the
+/// recursion attestation path shares one digest between the transcript absorb
+/// and the `program_id` fold (a full-ELF hash is expensive in-guest).
+#[allow(clippy::too_many_arguments)]
+pub(crate) fn absorb_statement_with_digest(
+    t: &mut impl IsTranscript<E>,
+    kind: StatementKind,
+    elf_digest: &[u8; 32],
+    public_output: &[u8],
+    table_counts: &TableCounts,
+    num_private_input_pages: usize,
+    runtime_page_ranges: &[RuntimePageRange],
+    fri_final_poly_log_degree: u8,
 ) {
     // Leading domain tag — distinct per statement kind, so a monolithic proof and
     // a continuation epoch proof can never share a transcript prefix.
@@ -56,7 +86,7 @@ pub(crate) fn absorb_statement(
     t.append_bytes(domain_tag);
 
     // ELF: fixed 32-byte digest — no length prefix needed.
-    t.append_bytes(&elf_digest(elf_bytes));
+    t.append_bytes(elf_digest);
 
     // public_output: variable length → length-prefix to prevent boundary collisions.
     t.append_bytes(&(public_output.len() as u64).to_le_bytes());
diff --git a/prover/src/tests/mod.rs b/prover/src/tests/mod.rs
index 4085f3bc5..faabff35d 100644
--- a/prover/src/tests/mod.rs
+++ b/prover/src/tests/mod.rs
@@ -71,6 +71,8 @@ pub mod prove_elfs_tests;
 #[cfg(test)]
 pub mod recursion_smoke_test;
 #[cfg(test)]
+pub mod recursion_soundness_gap_poc;
+#[cfg(test)]
 pub mod register_tests;
 #[cfg(test)]
 pub mod shift_tests;
diff --git a/prover/src/tests/recursion_smoke_test.rs b/prover/src/tests/recursion_smoke_test.rs
index 6a100aaa9..61659a372 100644
--- a/prover/src/tests/recursion_smoke_test.rs
+++ b/prover/src/tests/recursion_smoke_test.rs
@@ -1,15 +1,18 @@
 //! End-to-end naive recursion pipeline smoke tests: prove an inner program,
-//! hand `(VmProof, elf, opts)` to the in-VM verifier guest, then either prove
-//! the guest's execution (`OuterMode::Prove`) or just execute it
-//! (`OuterMode::ExecuteOnly`). Guest ELFs come from `make compile-recursion-elfs`.
-//!
-//! Every pipeline host-verifies the inner proof, so building with
-//! `--features stark/instruments` makes any of these tests print the verifier's
-//! per-step `Time spent:` timings.
+//! build the guest's private-input blob with `recursion::encode_guest_input`,
+//! hand it to the in-VM verifier guest, then execute or prove the guest. Guest
+//! ELFs come from `make compile-recursion-elfs`. `ProofOptions` is fixed per
+//! preset at build time (`recursion::Preset`); `decode_commitment`/
+//! `page_commitments` are private input, precomputed host-side. Each pipeline
+//! host-verifies the inner proof via full recompute (`None, None`) as a
+//! ground-truth check, then runs the production consumer check
+//! (`recursion::check_attestation`) over the guest's committed attestation.
 
 use std::ops::ControlFlow;
 use std::path::PathBuf;
 
+use crate::recursion::{self, MIN_PROOF_OPTIONS, Preset};
+
 fn workspace_root() -> PathBuf {
     PathBuf::from(env!("CARGO_MANIFEST_DIR"))
         .parent()
@@ -28,19 +31,10 @@ fn read_guest_elf(root: &std::path::Path, name: &str) -> Vec<u8> {
     })
 }
 
-/// Smallest possible inner proof (blowup=2, 1 query). Intentionally insecure —
-/// for the cheap diagnostics, not soundness.
-const MIN_PROOF_OPTIONS: stark::proof::options::ProofOptions =
-    stark::proof::options::ProofOptions {
-        blowup_factor: 2,
-        fri_number_of_queries: 1,
-        coset_offset: 3,
-        grinding_factor: 1,
-        fri_final_poly_log_degree: 7,
-    };
-
-/// Prove `inner_elf` under `opts` and postcard-encode `(proof, elf, opts)` into
-/// the guest's private-input blob. Returns the proof and the blob.
+/// Prove `inner_elf` under `opts` and build the guest's private-input blob via
+/// [`recursion::encode_guest_input`] (which precomputes the DECODE/page roots
+/// and postcard-encodes the [`recursion::GuestInput`] tuple). Returns the proof
+/// and the blob.
 fn prove_inner_and_encode_blob(
     tag: &str,
     inner_elf: &[u8],
@@ -59,8 +53,8 @@ fn prove_inner_and_encode_blob(
     )
     .expect("inner prove should succeed");
 
-    let blob =
-        postcard::to_allocvec(&(&inner_proof, &inner_elf, opts)).expect("postcard encode failed");
+    let blob = recursion::encode_guest_input(&inner_proof, inner_elf, opts)
+        .expect("recursion::encode_guest_input failed");
     eprintln!("[{tag}] postcard blob: {} bytes", blob.len());
     (inner_proof, blob)
 }
@@ -161,12 +155,12 @@ fn drive_executor(
     (total_cycles, start.elapsed())
 }
 
-/// Shared preamble: build the blob (an `empty` inner proof under `opts`), load
-/// `guest_name`, and stand up an executor. Returns `(elf_bytes, program, executor)`.
+/// Shared preamble: build the blob (an `empty` inner proof under the preset's
+/// options), load the `recursion-<preset>.elf` verifier, and stand up an
+/// executor. Returns `(elf_bytes, program, executor)`.
 fn setup_guest_run(
     label: &str,
-    guest_name: &str,
-    opts: &stark::proof::options::ProofOptions,
+    preset: Preset,
 ) -> (
     Vec<u8>,
     executor::elf::Elf,
@@ -174,14 +168,17 @@ fn setup_guest_run(
 ) {
     let root = workspace_root();
     let empty_elf_bytes = read_guest_elf(&root, "empty");
-    let guest_elf_bytes = read_guest_elf(&root, guest_name);
+    let guest_elf_bytes = read_guest_elf(&root, preset.artifact_stem());
 
-    let (_inner_proof, blob) = prove_inner_and_encode_blob(label, &empty_elf_bytes, &[], opts);
+    let (_inner_proof, blob) =
+        prove_inner_and_encode_blob(label, &empty_elf_bytes, &[], &preset.options());
 
     let program = executor::elf::Elf::load(&guest_elf_bytes).expect("ELF load failed");
     assert_ne!(
-        program.entry_point, 0,
-        "{guest_name} ELF has entry_point=0 — build artifact is malformed"
+        program.entry_point,
+        0,
+        "recursion-{} ELF has entry_point=0 — build artifact is malformed",
+        preset.name()
     );
     let executor =
         executor::vm::execution::Executor::new(&program, blob).expect("Executor::new failed");
@@ -212,11 +209,6 @@ const STEP_LABELS: [&str; 7] = [
     "6. step 4: verify_trace_and_composition_openings (+ wrap-up)",
 ];
 
-/// `blowup=8` (128-bit, multi-query) options for the `multiquery` variants.
-fn blowup8() -> stark::proof::options::ProofOptions {
-    crate::GoldilocksCubicProofOptions::with_blowup(8).expect("blowup=8 is always valid")
-}
-
 /// Short per-step tag for the function table, keyed by the same bucket index
 /// used in `STEP_LABELS`/`buckets`.
 fn step_tag(bucket: u8) -> &'static str {
@@ -232,12 +224,9 @@ fn step_tag(bucket: u8) -> &'static str {
     }
 }
 
-/// Print one top-25 table: `rows` is `(name, cycles, distinct_pcs)`, already
-/// unsorted; `denom_cycles` is the denominator for percentages — the global
-/// total for the all-steps table, but *that step's own total* for a per-step
-/// table, so `%`/`cum %` show what dominates within that step (a `keccak`
-/// that's 90% of a cheap step should read as 90%, not as a fraction of a
-/// percent of the whole run).
+/// Print one top-25 table. `rows` is `(name, cycles, distinct_pcs)`;
+/// `denom_cycles` is the percentage denominator (global total for the all-steps
+/// table, that step's own total for a per-step table).
 fn print_top25_table(rows: &mut [(String, u64, u64)], denom_cycles: u64) {
     rows.sort_unstable_by_key(|(_name, cycles, _pcs)| std::cmp::Reverse(*cycles));
     let pct = |n: u64| 100.0 * (n as f64) / (denom_cycles as f64);
@@ -339,15 +328,11 @@ fn print_step_breakdown(buckets: &[u64; 7], total_cycles: u64) {
 /// per-step cycle breakdown (marker decode is cheap — one `InstructionCache`
 /// lookup per cycle), and a rough trace/LDE estimate; with `detailed`, also
 /// the top-25 functions table (needs a `pc_hist` HashMap, so gated).
-fn run_profile(
-    guest_name: &str,
-    progress_stride: usize,
-    opts: stark::proof::options::ProofOptions,
-    detailed: bool,
-) {
+fn run_profile(preset: Preset, progress_stride: usize, detailed: bool) {
     use std::collections::HashMap;
 
-    let (guest_elf_bytes, program, mut executor) = setup_guest_run("profile", guest_name, &opts);
+    let opts = preset.options();
+    let (guest_elf_bytes, program, mut executor) = setup_guest_run("profile", preset);
     let symbols = executor::elf::SymbolTable::parse(&guest_elf_bytes);
     let instructions = executor::vm::execution::InstructionCache::new(&program.data)
         .expect("instruction cache build failed");
@@ -358,7 +343,8 @@ fn run_profile(
     let unique = std::cell::Cell::new(0usize);
 
     eprintln!(
-        "[profile] executing {guest_name} guest ({}) ...",
+        "[profile] executing recursion-{} guest ({}) ...",
+        preset.name(),
         if detailed {
             "histogram + steps"
         } else {
@@ -403,8 +389,8 @@ fn run_profile(
     eprintln!();
     eprintln!("============================================================");
     eprintln!(
-        "  {} GUEST PROFILE (blowup={}, {} queries)",
-        guest_name.to_uppercase(),
+        "  RECURSION-{} GUEST PROFILE (blowup={}, {} queries)",
+        preset.name().to_uppercase(),
         opts.blowup_factor,
         opts.fri_number_of_queries,
     );
@@ -433,34 +419,29 @@ fn run_profile(
     eprintln!("============================================================");
 }
 
-/// Core pipeline: prove the inner program, run the guest to `mode`, assert it
-/// committed `[1]` (the in-VM verifier accepted the proof).
+/// Core pipeline: prove the inner program under `preset.options()`, run the
+/// guest (`recursion-<preset>.elf`) to `mode`, then run the production consumer
+/// check — recompute the program id from the trusted inner ELF and compare it
+/// against the guest's committed attestation (`program_id || inner_public_output`)
+/// via [`recursion::check_attestation`]. A match means the in-VM verifier
+/// accepted the proof and the host-side identity binding holds.
 fn run_recursion_pipeline_with_options(
     label: &str,
     inner_elf_bytes: &[u8],
     inner_private_input: &[u8],
-    inner_proof_options: stark::proof::options::ProofOptions,
+    preset: Preset,
     mode: OuterMode,
 ) {
     let root = workspace_root();
-    let recursion_elf_bytes = read_guest_elf(&root, "recursion");
+    let recursion_elf_bytes = read_guest_elf(&root, preset.artifact_stem());
+    let opts = preset.options();
 
-    let (inner_proof, blob) = prove_inner_and_encode_blob(
-        label,
-        inner_elf_bytes,
-        inner_private_input,
-        &inner_proof_options,
-    );
+    let (inner_proof, blob) =
+        prove_inner_and_encode_blob(label, inner_elf_bytes, inner_private_input, &opts);
 
     assert!(
-        crate::verify_with_options(
-            &inner_proof,
-            inner_elf_bytes,
-            &inner_proof_options,
-            None,
-            None
-        )
-        .expect("inner verify errored"),
+        crate::verify_with_options(&inner_proof, inner_elf_bytes, &opts, None, None)
+            .expect("inner verify errored"),
         "inner proof must verify on host"
     );
     assert!(
@@ -473,62 +454,121 @@ fn run_recursion_pipeline_with_options(
         OuterMode::Prove => prove_outer_and_commit(label, &recursion_elf_bytes, &blob),
     };
 
+    // Production consumer path: recompute the id from the trusted inner ELF and
+    // compare against the guest's committed attestation (the real host-side
+    // binding). `Some(inner_public_output)` iff the recompute matches.
+    let inner_output = recursion::check_attestation(&committed, inner_elf_bytes, &opts)
+        .expect("check_attestation errored")
+        .expect(
+            "guest attestation must match the trusted inner ELF (program_id recompute+compare)",
+        );
     assert_eq!(
-        committed,
-        vec![1u8],
-        "recursion guest must commit the [1] success marker (in-VM verify accepted)"
+        inner_output, inner_proof.public_output,
+        "attested inner public output must equal the inner proof's public output"
     );
-    eprintln!("[{label}] guest committed [1]: in-VM verify accepted ✓");
+    eprintln!("[{label}] guest attestation matched the trusted inner ELF (program_id recompute) ✓");
 }
 
-/// `run_recursion_pipeline_with_options` with `blowup=8` (the `empty`/`fibonacci` default).
+/// `run_recursion_pipeline_with_options` at `blowup=8` (the `empty`/`fibonacci`
+/// default), i.e. [`Preset::Blowup8`].
 fn run_recursion_pipeline(
     label: &str,
     inner_elf_bytes: &[u8],
     inner_private_input: &[u8],
     mode: OuterMode,
 ) {
-    let inner_proof_options = stark::proof::options::GoldilocksCubicProofOptions::with_blowup(8)
-        .expect("blowup=8 is always valid");
     run_recursion_pipeline_with_options(
         label,
         inner_elf_bytes,
         inner_private_input,
-        inner_proof_options,
+        Preset::Blowup8,
         mode,
     );
 }
 
-/// Decode the blob on the host and verify — a cheap guard on the encode/decode
-/// contract without running the VM.
+/// Decode the blob on the host and mirror the guest's verify+attest, then run
+/// the consumer check — a cheap guard on the encode/decode/attest contract
+/// without running the VM.
 #[test]
-#[ignore = "needs prebuilt guest ELF (make compile-recursion-elfs)"]
 fn test_recursion_blob_decodes_and_verifies_on_host() {
     let root = workspace_root();
     let empty_elf_bytes = read_guest_elf(&root, "empty");
     let (_inner, blob) =
         prove_inner_and_encode_blob("roundtrip", &empty_elf_bytes, &[], &MIN_PROOF_OPTIONS);
 
-    // Decode exactly as the guest does.
-    let decoded: Result<(crate::VmProof, Vec<u8>, crate::ProofOptions), _> =
-        postcard::from_bytes(&blob);
-    let (vm_proof, inner_elf, options) = match decoded {
+    // Decode exactly as the guest does (built with the `min` feature).
+    let decoded: Result<recursion::GuestInput, _> = postcard::from_bytes(&blob);
+    let (vm_proof, inner_elf, decode_commitment, page_commitments) = match decoded {
         Ok(t) => t,
         Err(e) => panic!("[roundtrip] postcard DECODE failed (this is the guest panic): {e}"),
     };
     eprintln!(
-        "[roundtrip] decode ok: elf {} bytes, blowup {}",
+        "[roundtrip] decode ok: elf {} bytes, {} page commitments",
         inner_elf.len(),
-        options.blowup_factor
+        page_commitments.len(),
     );
 
-    match crate::verify_with_options(&vm_proof, &inner_elf, &options, None, None) {
-        Ok(true) => eprintln!("[roundtrip] verify ok=true — guest path is sound"),
-        Ok(false) => panic!(
-            "[roundtrip] verify returned FALSE (guest hits assert!(ok)) — proof did not survive the postcard round-trip"
+    // Mirror the guest exactly: verify_and_attest over the supplied roots.
+    let attestation = match recursion::verify_and_attest(
+        &vm_proof,
+        &inner_elf,
+        &MIN_PROOF_OPTIONS,
+        decode_commitment,
+        &page_commitments,
+    ) {
+        Ok(Some(a)) => {
+            eprintln!("[roundtrip] verify_and_attest accepted — guest path is sound");
+            a
+        }
+        Ok(None) => panic!(
+            "[roundtrip] verify_and_attest returned None (guest hits the failed-verification expect) — proof did not survive the postcard round-trip"
         ),
-        Err(e) => panic!("[roundtrip] verify ERRORED (guest hits .expect): {e:?}"),
-    }
+        Err(e) => panic!("[roundtrip] verify_and_attest ERRORED (guest hits .expect): {e:?}"),
+    };
+
+    // Consumer check: the committed attestation must bind to the trusted inner
+    // ELF and carry the inner proof's public output.
+    let output = recursion::check_attestation(&attestation, &inner_elf, &MIN_PROOF_OPTIONS)
+        .expect("check_attestation errored")
+        .expect("attestation must match the trusted inner ELF (program_id recompute+compare)");
+    assert_eq!(
+        output, vm_proof.public_output,
+        "attested public output must equal the inner proof's public output"
+    );
+}
+
+/// Corrupting a private-input commitment on an *honest* proof makes
+/// verification fail (`Ok(false)`). Necessary but not sufficient alone — a
+/// custom prover can supply consistent mismatched roots (see
+/// `recursion_soundness_gap_poc`); the identity binding is the `program_id`
+/// fold, not this check.
+#[test]
+fn test_recursion_rejects_corrupted_commitment() {
+    let root = workspace_root();
+    let empty_elf_bytes = read_guest_elf(&root, "empty");
+    let (vm_proof, _blob) = prove_inner_and_encode_blob(
+        "corrupt-commitment",
+        &empty_elf_bytes,
+        &[],
+        &MIN_PROOF_OPTIONS,
+    );
+    let (mut decode_commitment, page_commitments) =
+        recursion::precomputed_commitments(&empty_elf_bytes, &MIN_PROOF_OPTIONS)
+            .expect("precomputed_commitments failed");
+    decode_commitment[0] ^= 0xFF;
+
+    let ok = crate::verify_with_options(
+        &vm_proof,
+        &empty_elf_bytes,
+        &MIN_PROOF_OPTIONS,
+        Some(decode_commitment),
+        Some(&page_commitments),
+    )
+    .expect("verify errored");
+    assert!(
+        !ok,
+        "corrupted decode_commitment must be rejected, not silently accepted"
+    );
 }
 
 // === Execute-only tier ========================================================
@@ -557,7 +597,7 @@ fn test_recursion_execute_1query() {
         "recursion-exec-1query",
         &empty_elf_bytes,
         &[],
-        MIN_PROOF_OPTIONS,
+        Preset::Min,
         OuterMode::ExecuteOnly,
     );
 }
@@ -577,8 +617,7 @@ fn test_recursion_execute_1query() {
 #[test]
 #[ignore = "slow: runs the in-VM STARK verifier (minutes on CI)"]
 fn test_recursion_step_markers_observed_in_order() {
-    let (_bytes, program, mut executor) =
-        setup_guest_run("step-markers", "recursion", &MIN_PROOF_OPTIONS);
+    let (_bytes, program, mut executor) = setup_guest_run("step-markers", Preset::Min);
     let instructions = executor::vm::execution::InstructionCache::new(&program.data)
         .expect("instruction cache build failed");
 
@@ -669,7 +708,7 @@ fn test_recursion_prove_1query() {
         "recursion-prove-1query",
         &empty_elf_bytes,
         &[],
-        MIN_PROOF_OPTIONS,
+        Preset::Min,
         OuterMode::Prove,
     );
 }
@@ -694,28 +733,28 @@ fn test_dump_recursion_input() {
 #[test]
 #[ignore = "diagnostic: fast; recursion guest cycle count (1 query)"]
 fn test_recursion_cycles_1query() {
-    run_profile("recursion", 500, MIN_PROOF_OPTIONS, false);
+    run_profile(Preset::Min, 500, false);
 }
 
 /// Cycle count only at 128-bit security: more FRI queries → more verifier cycles.
 #[test]
 #[ignore = "diagnostic: fast; recursion guest cycle count (multi-query)"]
 fn test_recursion_cycles_multiquery() {
-    run_profile("recursion", 500, blowup8(), false);
+    run_profile(Preset::Blowup8, 500, false);
 }
 
 /// Full profile (top-25 + per-step) of the 1-query run.
 #[test]
 #[ignore = "diagnostic: ~8 min; recursion guest histogram + steps (1 query)"]
 fn test_recursion_profile_1query() {
-    run_profile("recursion", 500, MIN_PROOF_OPTIONS, true);
+    run_profile(Preset::Min, 500, true);
 }
 
 /// Full profile at 128-bit security: weight shifts toward per-query FRI/Merkle.
 #[test]
 #[ignore = "diagnostic: heavy; recursion guest histogram + steps (multi-query)"]
 fn test_recursion_profile_multiquery() {
-    run_profile("recursion", 500, blowup8(), true);
+    run_profile(Preset::Blowup8, 500, true);
 }
 
 /// Inner program: fibonacci(10).
diff --git a/prover/src/tests/recursion_soundness_gap_poc.rs b/prover/src/tests/recursion_soundness_gap_poc.rs
new file mode 100644
index 000000000..73410ff62
--- /dev/null
+++ b/prover/src/tests/recursion_soundness_gap_poc.rs
@@ -0,0 +1,274 @@
+//! `verify_with_options(.., Some(decode), Some(pages))` does NOT bind the
+//! supplied roots to `inner_elf`: a custom prover can absorb `elf_digest(X)`
+//! into the Fiat-Shamir statement while the constrained instructions and every
+//! preprocessed root are those of a DIFFERENT program Y, and verification with
+//! `inner_elf = X` and Y's roots still returns `Ok(true)` (the "critical
+//! soundness check" in `crypto/stark/src/verifier.rs` compares two
+//! prover-controlled values here, so it is vacuous against a custom prover).
+//!
+//! The recursion guest does not rely on verify for that binding: it commits
+//! `program_id(inner_elf, decode, pages)`, which folds the supplied roots into
+//! the identity — so the same substitution yields an id that differs from the
+//! honest `program_id(X)`, detectable by whoever recomputes it natively and
+//! compares (`recursion::check_attestation`). These tests pin both facts:
+//! verify accepts, and the fold-and-compare catches.
+
+use std::collections::HashSet;
+use std::path::PathBuf;
+
+use crypto::fiat_shamir::default_transcript::DefaultTranscript;
+use stark::prover::{IsStarkProver, Prover};
+
+use crate::recursion::{MIN_PROOF_OPTIONS, precomputed_commitments};
+use crate::statement::{StatementKind, absorb_statement, elf_digest};
+use crate::tables::trace_builder::Traces;
+use crate::test_utils::E;
+use crate::{MaxRowsConfig, VmAirs, VmProof};
+
+use executor::elf::Elf;
+use executor::vm::execution::Executor;
+
+fn workspace_root() -> PathBuf {
+    PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .parent()
+        .expect("workspace root")
+        .to_path_buf()
+}
+
+fn read_guest_elf(name: &str) -> Vec<u8> {
+    let path = workspace_root().join(format!("executor/program_artifacts/recursion/{name}.elf"));
+    std::fs::read(&path).unwrap_or_else(|e| {
+        panic!(
+            "failed to read {} — run `make compile-recursion-elfs`: {e}",
+            path.display()
+        )
+    })
+}
+
+/// The set of program-counter values fetched during a run of `elf_bytes`.
+fn executed_pcs(elf_bytes: &[u8]) -> HashSet<u64> {
+    let elf = Elf::load(elf_bytes).expect("ELF load failed");
+    let executor = Executor::new(&elf, vec![]).expect("executor new");
+    let result = executor.run().expect("run failed");
+    result.logs.iter().map(|l| l.current_pc).collect()
+}
+
+/// Read a 4-byte word (LE) from an executable ELF segment at virtual address
+/// `vaddr`, returning its raw-file byte offset and current value. Parses the
+/// program headers directly so we can patch the raw bytes (and thus the
+/// `elf_digest`) at exactly the right place.
+fn exec_words(elf_bytes: &[u8]) -> Vec<(usize, u64, u32)> {
+    let rd_u16 = |o: usize| u16::from_le_bytes(elf_bytes[o..o + 2].try_into().unwrap());
+    let rd_u32 = |o: usize| u32::from_le_bytes(elf_bytes[o..o + 4].try_into().unwrap());
+    let rd_u64 = |o: usize| u64::from_le_bytes(elf_bytes[o..o + 8].try_into().unwrap());
+
+    let e_phoff = rd_u64(32) as usize;
+    let e_phentsize = rd_u16(54) as usize;
+    let e_phnum = rd_u16(56) as usize;
+
+    const PT_LOAD: u32 = 1;
+    const PF_X: u32 = 1;
+
+    let mut out = Vec::new();
+    for i in 0..e_phnum {
+        let ph = e_phoff + i * e_phentsize;
+        let p_type = rd_u32(ph);
+        let p_flags = rd_u32(ph + 4);
+        if p_type != PT_LOAD || (p_flags & PF_X) == 0 {
+            continue;
+        }
+        let p_offset = rd_u64(ph + 8) as usize;
+        let p_vaddr = rd_u64(ph + 16);
+        let p_filesz = rd_u64(ph + 32) as usize;
+        let mut off = 0usize;
+        while off + 4 <= p_filesz {
+            let file_off = p_offset + off;
+            let vaddr = p_vaddr + off as u64;
+            out.push((file_off, vaddr, rd_u32(file_off)));
+            off += 4;
+        }
+    }
+    out
+}
+
+/// Build program Y from program X (`= empty.elf`) by patching a single
+/// executable-segment word at a PC that X never fetches, to a *different*
+/// still-parseable instruction. Because the word is never fetched, Y halts
+/// byte-identically to X, so their AIR structure (entry, segments, pages,
+/// table counts, public output, runtime pages) is identical — they differ
+/// ONLY in one instruction's bytes, hence different DECODE root, different
+/// code-page root, and different `elf_digest`.
+fn make_variant_program(x_bytes: &[u8]) -> Vec<u8> {
+    let executed = executed_pcs(x_bytes);
+    let words = exec_words(x_bytes);
+
+    // A never-fetched slot we can rewrite to a valid, distinct instruction.
+    // Candidates are canonical nops (`addi x0,x0,K`), which always parse.
+    const NOP_0: u32 = 0x0000_0013; // addi x0, x0, 0
+    const NOP_1: u32 = 0x0010_0013; // addi x0, x0, 1
+
+    let (file_off, _vaddr, cur) = words
+        .iter()
+        .find(|(_, vaddr, _)| !executed.contains(vaddr))
+        .copied()
+        .expect("no never-executed executable word found to patch");
+
+    let new_word = if cur == NOP_1 { NOP_0 } else { NOP_1 };
+
+    let mut y = x_bytes.to_vec();
+    y[file_off..file_off + 4].copy_from_slice(&new_word.to_le_bytes());
+    assert_ne!(y, x_bytes.to_vec(), "variant must differ from base");
+    y
+}
+
+/// Custom prover: prove `prove_elf`'s execution honestly, but absorb
+/// `statement_elf`'s identity into the Fiat-Shamir transcript instead of
+/// `prove_elf`'s. Every preprocessed root in the resulting proof is computed
+/// from `prove_elf`. Mirrors `prove_with_options_and_inputs`, swapping only
+/// the `elf_bytes` passed to `absorb_statement`.
+fn custom_prove_with_statement_elf(
+    prove_elf: &[u8],
+    statement_elf: &[u8],
+    opts: &stark::proof::options::ProofOptions,
+) -> VmProof {
+    let program = Elf::load(prove_elf).expect("prove ELF load failed");
+    let executor = Executor::new(&program, vec![]).expect("executor new");
+    let result = executor.run().expect("run failed");
+
+    let max_rows = MaxRowsConfig::default();
+    let mut traces = Traces::from_elf_and_logs(
+        &program,
+        &result.logs,
+        &max_rows,
+        &[],
+        #[cfg(feature = "disk-spill")]
+        stark::storage_mode::StorageMode::Ram,
+    )
+    .expect("trace build failed");
+
+    let table_counts = traces.table_counts();
+    let airs = VmAirs::new(
+        &program,
+        opts,
+        false,
+        &traces.page_configs,
+        &table_counts,
+        None,
+        true,
+        None,
+        None,
+        None,
+    );
+
+    let runtime_page_ranges = traces.runtime_page_ranges();
+    let num_private_input_pages = traces
+        .page_configs
+        .iter()
+        .filter(|c| c.is_private_input)
+        .count();
+
+    let mut transcript = DefaultTranscript::<E>::new(&[]);
+    absorb_statement(
+        &mut transcript,
+        StatementKind::Monolithic,
+        statement_elf, // <-- the substitution: X's identity, Y's everything else
+        &traces.public_output_bytes,
+        &table_counts,
+        num_private_input_pages,
+        &runtime_page_ranges,
+        opts.fri_final_poly_log_degree,
+    );
+
+    let proof = Prover::multi_prove(
+        airs.air_trace_pairs(&mut traces),
+        &mut transcript,
+        #[cfg(feature = "disk-spill")]
+        stark::storage_mode::StorageMode::Ram,
+    )
+    .expect("multi_prove failed");
+
+    VmProof {
+        proof,
+        runtime_page_ranges,
+        table_counts,
+        public_output: traces.public_output_bytes.clone(),
+        num_private_input_pages,
+    }
+}
+
+/// Sanity: the custom prover, used honestly (statement == proven program),
+/// produces genuinely valid proofs. Guards against a vacuous PoC.
+#[test]
+fn test_custom_prover_is_not_vacuous() {
+    let x = read_guest_elf("empty");
+    let proof = custom_prove_with_statement_elf(&x, &x, &MIN_PROOF_OPTIONS);
+    let ok = crate::verify_with_options(&proof, &x, &MIN_PROOF_OPTIONS, None, None)
+        .expect("verify errored");
+    assert!(ok, "custom prover must produce valid proofs when honest");
+}
+
+/// `verify` accepts a proof whose Fiat-Shamir statement is X's but whose
+/// constrained instructions and supplied roots are Y's — so verify is not the
+/// binding. The `program_id` fold is: it commits an id that differs from the
+/// honest id of X, making the substitution detectable downstream.
+#[test]
+fn test_supplied_decode_root_not_bound_to_inner_elf() {
+    let x = read_guest_elf("empty");
+    let y = make_variant_program(&x);
+
+    // X and Y differ, and specifically in their preprocessed DECODE roots.
+    assert_ne!(elf_digest(&x), elf_digest(&y), "elf_digest must differ");
+    let (decode_x, pages_x) =
+        precomputed_commitments(&x, &MIN_PROOF_OPTIONS).expect("precomputed_commitments X");
+    let (decode_y, pages_y) =
+        precomputed_commitments(&y, &MIN_PROOF_OPTIONS).expect("precomputed_commitments Y");
+    assert_ne!(decode_x, decode_y, "DECODE roots must differ (X vs Y)");
+
+    // Craft a proof: constrain Y, but absorb X's identity into the statement.
+    let proof = custom_prove_with_statement_elf(&y, &x, &MIN_PROOF_OPTIONS);
+
+    // Negative control: the honest recompute path (None, None) rebuilds X's
+    // roots and rejects — the proof is NOT coincidentally valid for X.
+    let honest = crate::verify_with_options(&proof, &x, &MIN_PROOF_OPTIONS, None, None)
+        .expect("verify errored");
+    assert!(
+        !honest,
+        "honest recompute (None, None) must reject: proof carries Y's roots, X recompute differs"
+    );
+
+    // verify is NOT the binding: with Y's roots supplied (the guest's
+    // private-input path), verification accepts for inner_elf = X.
+    let accepted = crate::verify_with_options(
+        &proof,
+        &x,
+        &MIN_PROOF_OPTIONS,
+        Some(decode_y),
+        Some(&pages_y),
+    )
+    .expect("verify errored");
+    assert!(
+        accepted,
+        "verify unexpectedly rejected the mismatched-root proof"
+    );
+
+    // The fold IS the binding: folding Y's supplied roots into X's identity
+    // yields an id that differs from the honest id of X.
+    let forged_id = crate::recursion::program_id_from_elf(&x, &decode_y, &pages_y).unwrap();
+    let honest_id = crate::recursion::program_id_from_elf(&x, &decode_x, &pages_x).unwrap();
+    assert_ne!(
+        forged_id, honest_id,
+        "program_id fold must make the root substitution detectable"
+    );
+
+    // End-to-end consumer path: the guest would commit `forged_id ||
+    // public_output`; the mandatory host-side compare (`check_attestation`)
+    // rejects exactly this substitution that `verify` accepts above.
+    let mut forged = forged_id.to_vec();
+    forged.extend_from_slice(&proof.public_output);
+    assert!(
+        crate::recursion::check_attestation(&forged, &x, &MIN_PROOF_OPTIONS)
+            .expect("check_attestation errored")
+            .is_none(),
+        "check_attestation must reject the forged attestation the consumer would receive"
+    );
+}