diff --git a/src/proof/nova.rs b/src/proof/nova.rs
index 7410f7b16f..e8cb98d382 100644
--- a/src/proof/nova.rs
+++ b/src/proof/nova.rs
@@ -1,4 +1,4 @@
-use bellpepper_core::{num::AllocatedNum, ConstraintSystem};
+use bellpepper_core::{num::AllocatedNum, ConstraintSystem, SynthesisError};
 use halo2curves::bn256::Fr as Bn256Scalar;
 use nova::{
     errors::NovaError,
@@ -18,6 +18,7 @@ use std::{
     marker::PhantomData,
     sync::{Arc, Mutex},
 };
+use tracing::info;
 
 use crate::{
     config::lurk_config,
@@ -25,7 +26,7 @@ use crate::{
     error::ProofError,
     eval::lang::Lang,
     field::LurkField,
-    lem::{interpreter::Frame, pointers::Ptr, store::Store},
+    lem::{interpreter::Frame, multiframe::MultiFrame, pointers::Ptr, store::Store},
     proof::{supernova::FoldingConfig, FrameLike, Prover},
 };
 
@@ -223,6 +224,28 @@ pub fn circuits<'a, F: CurveCycleEquipped, C: Coprocessor<F> + 'a>(
     )
 }
 
+/// For debugging purposes, synthesize the circuit and check that the constraint
+/// system is satisfied
+pub(crate) fn debug_step<F: LurkField, C: Coprocessor<F>>(
+    circuit: &MultiFrame<'_, F, C>,
+    store: &Store<F>,
+) -> Result<(), SynthesisError> {
+    use bellpepper_core::test_cs::TestConstraintSystem;
+    let mut cs = TestConstraintSystem::<F>::new();
+
+    let zi = store.to_scalar_vector(circuit.input());
+    let zi_allocated: Vec<_> = zi
+        .iter()
+        .enumerate()
+        .map(|(i, x)| AllocatedNum::alloc(cs.namespace(|| format!("z{i}_1")), || Ok(*x)))
+        .collect::<Result<_, _>>()?;
+
+    circuit.synthesize(&mut cs, zi_allocated.as_slice())?;
+
+    assert!(cs.is_satisfied());
+    Ok(())
+}
+
 impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<'a, F, C>>
     for Proof<F, C1LEM<'a, F, C>>
 {
@@ -237,22 +260,35 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
         steps: Vec<C1LEM<'a, F, C>>,
         store: &Store<F>,
     ) -> Result<Self, ProofError> {
-        assert!(!steps.is_empty());
-        assert_eq!(steps[0].arity(), z0.len());
         let debug = false;
-        let z0_primary = z0;
-        let z0_secondary = Self::z0_secondary();
+        let first_step = steps.first().expect("steps can't be empty");
+        assert_eq!(first_step.arity(), z0.len());
 
-        let circuit_secondary = TrivialCircuit::default();
+        let secondary_circuit = TrivialCircuit::default();
 
         let num_steps = steps.len();
-        tracing::debug!("steps.len: {num_steps}");
-
-        // produce a recursive SNARK
-        let mut recursive_snark: Option<RecursiveSNARK<E1<F>>> = None;
+        info!("proving {num_steps} steps");
+
+        let mut recursive_snark = RecursiveSNARK::new(
+            &pp.pp,
+            first_step,
+            &secondary_circuit,
+            z0,
+            &Self::z0_secondary(),
+        )
+        .map_err(ProofError::Nova)?;
+
+        let mut prove_step = |i: usize, step: &C1LEM<'a, F, C>| {
+            if debug {
+                debug_step(step, store).unwrap();
+            }
+            info!("prove_step {i}");
+            recursive_snark
+                .prove_step(&pp.pp, step, &secondary_circuit)
+                .unwrap();
+        };
 
-        // the shadowing here is voluntary
-        let recursive_snark = if lurk_config(None, None)
+        if lurk_config(None, None)
             .perf
             .parallelism
             .recursive_steps
@@ -272,69 +308,21 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
                     });
                 });
 
-                for circuit_primary in cc.iter() {
-                    let mut circuit_primary = circuit_primary.lock().unwrap();
-
-                    let mut r_snark = recursive_snark.unwrap_or_else(|| {
-                        RecursiveSNARK::new(
-                            &pp.pp,
-                            &*circuit_primary,
-                            &circuit_secondary,
-                            z0_primary,
-                            &z0_secondary,
-                        )
-                        .expect("Failed to construct initial recursive snark")
-                    });
-                    r_snark
-                        .prove_step(&pp.pp, &*circuit_primary, &circuit_secondary)
-                        .expect("failure to prove Nova step");
-                    circuit_primary.clear_cached_witness();
-                    recursive_snark = Some(r_snark);
+                for (i, step) in cc.iter().enumerate() {
+                    let mut step = step.lock().unwrap();
+                    prove_step(i, &step);
+                    step.clear_cached_witness();
                 }
-                recursive_snark
             })
             .unwrap()
         } else {
-            for circuit_primary in steps.iter() {
-                if debug {
-                    // For debugging purposes, synthesize the circuit and check that the constraint system is satisfied.
-                    use bellpepper_core::test_cs::TestConstraintSystem;
-                    let mut cs = TestConstraintSystem::<F>::new();
-
-                    let zi = store.to_scalar_vector(circuit_primary.input());
-                    let zi_allocated: Vec<_> = zi
-                        .iter()
-                        .enumerate()
-                        .map(|(i, x)| {
-                            AllocatedNum::alloc(cs.namespace(|| format!("z{i}_1")), || Ok(*x))
-                        })
-                        .collect::<Result<_, _>>()?;
-
-                    circuit_primary.synthesize(&mut cs, zi_allocated.as_slice())?;
-
-                    assert!(cs.is_satisfied());
-                }
-
-                let mut r_snark = recursive_snark.unwrap_or_else(|| {
-                    RecursiveSNARK::new(
-                        &pp.pp,
-                        circuit_primary,
-                        &circuit_secondary,
-                        z0_primary,
-                        &z0_secondary,
-                    )
-                    .expect("Failed to construct initial recursive snark")
-                });
-                r_snark
-                    .prove_step(&pp.pp, circuit_primary, &circuit_secondary)
-                    .expect("failure to prove Nova step");
-                recursive_snark = Some(r_snark);
+            for (i, step) in steps.iter().enumerate() {
+                prove_step(i, step);
             }
-            recursive_snark
         };
 
         Ok(Self::Recursive(
-            Box::new(recursive_snark.unwrap()),
+            Box::new(recursive_snark),
             num_steps,
             PhantomData,
         ))
diff --git a/src/proof/supernova.rs b/src/proof/supernova.rs
index dfd2bbae93..66883efd6e 100644
--- a/src/proof/supernova.rs
+++ b/src/proof/supernova.rs
@@ -28,7 +28,7 @@ use crate::{
     field::LurkField,
     lem::{interpreter::Frame, pointers::Ptr, store::Store},
     proof::{
-        nova::{CurveCycleEquipped, Dual, NovaCircuitShape, E1},
+        nova::{debug_step, CurveCycleEquipped, Dual, NovaCircuitShape, E1},
         Prover, RecursiveSNARKTrait,
     },
 };
@@ -202,36 +202,29 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
         steps: Vec<C1LEM<'a, F, C>>,
         store: &Store<F>,
     ) -> Result<Self, ProofError> {
-        let mut recursive_snark_option: Option<RecursiveSNARK<E1<F>>> = None;
+        let debug = false;
+        let first_step = steps.first().expect("steps can't be empty");
 
-        let z0_primary = z0;
-        let z0_secondary = Self::z0_secondary();
+        info!("proving {} steps", steps.len());
 
-        let mut prove_step = |i: usize, step: &C1LEM<'a, F, C>| {
-            info!("prove_recursively, step {i}");
-
-            let secondary_circuit = step.secondary_circuit();
-
-            let mut recursive_snark = recursive_snark_option.clone().unwrap_or_else(|| {
-                info!("RecursiveSnark::new {i}");
-                RecursiveSNARK::new(
-                    &pp.pp,
-                    step,
-                    step,
-                    &secondary_circuit,
-                    z0_primary,
-                    &z0_secondary,
-                )
-                .unwrap()
-            });
+        let mut recursive_snark = RecursiveSNARK::new(
+            &pp.pp,
+            first_step,
+            first_step,
+            &first_step.secondary_circuit(),
+            z0,
+            &Self::z0_secondary(),
+        )
+        .map_err(ProofError::SuperNova)?;
 
+        let mut prove_step = |i: usize, step: &C1LEM<'a, F, C>| {
+            if debug {
+                debug_step(step, store).unwrap();
+            }
             info!("prove_step {i}");
-
             recursive_snark
-                .prove_step(&pp.pp, step, &secondary_circuit)
+                .prove_step(&pp.pp, step, &step.secondary_circuit())
                 .unwrap();
-
-            recursive_snark_option = Some(recursive_snark);
         };
 
         if lurk_config(None, None)
@@ -291,11 +284,7 @@ impl<'a, F: CurveCycleEquipped, C: Coprocessor<F>> RecursiveSNARKTrait<F, C1LEM<
             }
         }
 
-        // This probably should be made unnecessary.
-        Ok(Self::Recursive(
-            Box::new(recursive_snark_option.expect("RecursiveSNARK missing")),
-            PhantomData,
-        ))
+        Ok(Self::Recursive(Box::new(recursive_snark), PhantomData))
     }
 
     fn compress(self, pp: &PublicParams<F>) -> Result<Self, ProofError> {