diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs
index cc0ffafc08..513fa446b6 100644
--- a/source/builtin_macros/src/syntax.rs
+++ b/source/builtin_macros/src/syntax.rs
@@ -77,8 +77,11 @@ pub(crate) struct Visitor {
     pub(crate) erase_ghost: EraseGhost,
     // TODO: this should always be true
     use_spec_traits: bool,
-    // inside_ghost > 0 means we're currently visiting ghost code
+    // inside_ghost > 0 means we're currently visiting ghost code (spec or proof)
     inside_ghost: u32,
+    // inside_spec > 0 means we're currently visiting spec code (not proof)
+    // This is used to distinguish spec fn from proof fn for proof block handling
+    inside_spec: u32,
     // inside_type > 0 means we're currently visiting a type
     inside_type: u32,
     // inside_external_code > 0 means we're currently visiting an external or external_body body
@@ -1021,10 +1024,15 @@ impl Visitor {
             _ => (vec![], vec![]),
         };
 
-        let (inside_ghost, mode_attrs): (u32, Vec<Attribute>) = match &sig.mode {
-            FnMode::Default => (0, vec![]),
-            FnMode::Spec(token) => (1, vec![mk_verus_attr(token.spec_token.span, quote! { spec })]),
+        // inside_ghost: 1 for spec/proof functions (ghost code)
+        // inside_spec: 1 for spec functions only (needed for proof block handling)
+        let (inside_ghost, inside_spec, mode_attrs): (u32, u32, Vec<Attribute>) = match &sig.mode {
+            FnMode::Default => (0, 0, vec![]),
+            FnMode::Spec(token) => {
+                (1, 1, vec![mk_verus_attr(token.spec_token.span, quote! { spec })])
+            }
             FnMode::SpecChecked(token) => (
+                1,
                 1,
                 vec![mk_verus_attr(
                     token.spec_token.span,
@@ -1032,14 +1040,17 @@ impl Visitor {
                 )],
             ),
             FnMode::Proof(token) => {
-                (1, vec![mk_verus_attr(token.proof_token.span, quote! { proof })])
+                (1, 0, vec![mk_verus_attr(token.proof_token.span, quote! { proof })])
             }
             FnMode::ProofAxiom(token) => {
-                (1, vec![mk_verus_attr(token.axiom_token.span, quote! { proof })])
+                (1, 0, vec![mk_verus_attr(token.axiom_token.span, quote! { proof })])
+            }
+            FnMode::Exec(token) => {
+                (0, 0, vec![mk_verus_attr(token.exec_token.span, quote! { exec })])
             }
-            FnMode::Exec(token) => (0, vec![mk_verus_attr(token.exec_token.span, quote! { exec })]),
         };
         self.inside_ghost = inside_ghost;
+        self.inside_spec = inside_spec;
 
         let prover = self.take_ghost(&mut sig.spec.prover);
         let prover_attr = prover.as_ref().map(|verus_syn::Prover { id: prover_ident, .. }| {
@@ -3070,6 +3081,7 @@ impl Visitor {
         self.inside_ghost -= 1;
 
         let is_inside_ghost = self.inside_ghost > 0;
+        let is_inside_spec = self.inside_spec > 0;
 
         if let Expr::Call(call) = expr {
             let (_, is_tracked) = mode_block;
@@ -3101,7 +3113,10 @@ impl Visitor {
                 ((false, _), Expr::Block(..)) => {
                     // proof { ... }
                     let inner = take_expr(&mut *unary.expr);
-                    let e = if is_inside_ghost {
+                    // Use is_inside_spec (not is_inside_ghost) to distinguish spec fn from proof fn.
+                    // In spec fn, proof blocks are used for termination checking (proof_in_spec).
+                    // In proof fn or exec fn, proof blocks are treated as regular proof_block.
+                    let e = if is_inside_spec {
                         quote_spanned!(span => #[verifier::proof_in_spec] /* vattr */ #inner)
                     } else {
                         quote_spanned!(span => #[verifier::proof_block] /* vattr */ #inner)
@@ -4831,6 +4846,7 @@ pub(crate) fn rewrite_items_inner(
         erase_ghost,
         use_spec_traits,
         inside_ghost: 0,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -4842,6 +4858,7 @@ pub(crate) fn rewrite_items_inner(
     for mut item in &mut *items {
         visitor.visit_item_mut(&mut item);
         visitor.inside_ghost = 0;
+        visitor.inside_spec = 0;
         visitor.inside_const = false;
         visitor.inside_arith = InsideArith::None;
     }
@@ -4866,6 +4883,7 @@ pub(crate) fn rewrite_impl_items(
         erase_ghost,
         use_spec_traits,
         inside_ghost: 0,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -4877,6 +4895,7 @@ pub(crate) fn rewrite_impl_items(
     for mut item in &mut items.items {
         visitor.visit_impl_item_mut(&mut item);
         visitor.inside_ghost = 0;
+        visitor.inside_spec = 0;
         visitor.inside_const = false;
         visitor.inside_arith = InsideArith::None;
     }
@@ -4899,6 +4918,7 @@ pub(crate) fn rewrite_expr(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: if inside_ghost { 1 } else { 0 },
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -4930,6 +4950,7 @@ pub(crate) fn rewrite_proof_decl(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: 0,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -4983,6 +5004,7 @@ pub(crate) fn rewrite_expr_node(erase_ghost: EraseGhost, inside_ghost: bool, exp
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: if inside_ghost { 1 } else { 0 },
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -5172,6 +5194,7 @@ pub(crate) fn sig_specs_attr(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: 1,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -5210,6 +5233,7 @@ pub(crate) fn while_loop_spec_attr(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: 1,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -5242,6 +5266,7 @@ pub(crate) fn for_loop_spec_attr(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: 1,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -5300,6 +5325,7 @@ pub(crate) fn proof_block(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: 1,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -5324,6 +5350,7 @@ pub(crate) fn proof_macro_exprs(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: if inside_ghost { 1 } else { 0 },
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -5353,6 +5380,7 @@ pub(crate) fn inv_macro_exprs(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: 0,
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
@@ -5388,6 +5416,7 @@ pub(crate) fn proof_macro_explicit_exprs(
         erase_ghost,
         use_spec_traits: true,
         inside_ghost: if inside_ghost { 1 } else { 0 },
+        inside_spec: 0,
         inside_type: 0,
         inside_external_code: 0,
         inside_const: false,
diff --git a/source/rust_verify_test/tests/proof_in_spec.rs b/source/rust_verify_test/tests/proof_in_spec.rs
index 3694827485..57e0c93cd4 100644
--- a/source/rust_verify_test/tests/proof_in_spec.rs
+++ b/source/rust_verify_test/tests/proof_in_spec.rs
@@ -262,8 +262,9 @@ test_verify_one_file! {
     } => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
 }
 
+// proof blocks inside proof fn are now allowed (redundant but harmless)
 test_verify_one_file! {
-    #[test] non_spec_fn_not_yet_supported verus_code! {
+    #[test] proof_block_in_proof_fn_allowed verus_code! {
         proof fn f(i: int) {
             let x: int = {
                 proof {
@@ -272,7 +273,7 @@ test_verify_one_file! {
                 3
             };
         }
-    } => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
+    } => Ok(())
 }
 
 test_verify_one_file! {
@@ -288,8 +289,9 @@ test_verify_one_file! {
     } => Err(err) => assert_vir_error_msg(err, "return is not allowed inside spec")
 }
 
+// assignment inside proof block in proof fn is now allowed
 test_verify_one_file! {
-    #[test] assign_not_allowed verus_code! {
+    #[test] assign_in_proof_block_in_proof_fn verus_code! {
         proof fn f(i: int) {
             let mut b = false;
             let x: int = {
@@ -299,7 +301,7 @@ test_verify_one_file! {
                 3
             };
         }
-    } => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
+    } => Ok(())
 }
 
 test_verify_one_file! {
@@ -322,20 +324,20 @@ test_verify_one_file! {
     } => Err(err) => assert_vir_error_msg(err, "expression has mode spec, expected mode proof")
 }
 
+// tracked variables inside proof block in proof fn is now allowed
 test_verify_one_file! {
-    #[test] tracked_not_allowed2 verus_code! {
+    #[test] tracked_in_proof_block_in_proof_fn verus_code! {
         proof fn h(tracked i: int) {
         }
         proof fn f(tracked i: int) {
             let x: int = {
                 proof {
                     h(i);
-                    h(i);
                 }
                 3
             };
         }
-    } => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
+    } => Ok(())
 }
 
 test_verify_one_file! {
@@ -487,3 +489,110 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
+
+// ============================================================================
+// Tests for issue #2061: proof blocks inside proof fn should be allowed
+// https://github.com/verus-lang/verus/issues/2061
+// ============================================================================
+
+// Basic case from the issue: proof { } directly in proof fn body
+test_verify_one_file! {
+    #[test] issue_2061_basic verus_code! {
+        proof fn foo() {
+            proof { }
+        }
+    } => Ok(())
+}
+
+// proof block with assertion in proof fn
+test_verify_one_file! {
+    #[test] issue_2061_with_assert verus_code! {
+        proof fn foo() {
+            proof {
+                assert(1 + 1 == 2);
+            }
+        }
+    } => Ok(())
+}
+
+// proof block with failing assertion in proof fn
+test_verify_one_file! {
+    #[test] issue_2061_with_failing_assert verus_code! {
+        proof fn foo() {
+            proof {
+                assert(false); // FAILS
+            }
+        }
+    } => Err(err) => assert_one_fails(err)
+}
+
+// nested proof blocks in proof fn
+test_verify_one_file! {
+    #[test] issue_2061_nested verus_code! {
+        proof fn foo() {
+            proof {
+                proof {
+                    assert(true);
+                }
+            }
+        }
+    } => Ok(())
+}
+
+// proof block in proof fn with local variable
+test_verify_one_file! {
+    #[test] issue_2061_with_local verus_code! {
+        proof fn foo() {
+            let x: int = 5;
+            proof {
+                assert(x == 5);
+            }
+        }
+    } => Ok(())
+}
+
+// proof block in proof fn inside expression
+test_verify_one_file! {
+    #[test] issue_2061_in_expression verus_code! {
+        proof fn foo() -> int {
+            let result: int = {
+                proof {
+                    assert(true);
+                }
+                42
+            };
+            result
+        }
+    } => Ok(())
+}
+
+// Verify spec fn with decreases still works (regression test)
+test_verify_one_file! {
+    #[test] issue_2061_spec_fn_still_works verus_code! {
+        spec fn factorial(n: nat) -> nat
+            decreases n
+        {
+            if n == 0 {
+                1
+            } else {
+                proof {
+                    // This proof block in spec fn with decreases should still work
+                    assert(n > 0);
+                }
+                n * factorial((n - 1) as nat)
+            }
+        }
+    } => Ok(())
+}
+
+// Ensure proof blocks in spec fn WITHOUT decreases still error
+test_verify_one_file! {
+    #[test] issue_2061_spec_fn_no_decreases_still_errors verus_code! {
+        spec fn f(i: int) -> int {
+            proof {
+                assert(true);
+            }
+            3
+        }
+    } => Err(err) => assert_vir_error_msg(err, "proof blocks inside spec code is currently supported only for")
+}
diff --git a/source/vir/src/modes.rs b/source/vir/src/modes.rs
index bcdc2dc314..32af74f0b4 100644
--- a/source/vir/src/modes.rs
+++ b/source/vir/src/modes.rs
@@ -2913,8 +2913,12 @@ fn check_expr(
                     }
                     Ghost::Ghost
                 }
-                (_, false, false) => {
-                    return Err(error(&expr.span, "already in proof mode"));
+                (Ghost::Ghost, false, false) => {
+                    // Already in proof/spec mode - proof block is redundant but allowed
+                    if !is_unit(&e1.typ) {
+                        return Err(error(&expr.span, "proof block must have type ()"));
+                    }
+                    Ghost::Ghost
                 }
                 (Ghost::Exec, false, true) => {
                     return Err(error(