diff --git a/dependencies/syn/src/gen/clone.rs b/dependencies/syn/src/gen/clone.rs
index ec5dc82a50..948f1bbed9 100644
--- a/dependencies/syn/src/gen/clone.rs
+++ b/dependencies/syn/src/gen/clone.rs
@@ -2479,6 +2479,9 @@ impl Clone for crate::TraitItem {
             crate::TraitItem::Fn(v0) => crate::TraitItem::Fn(v0.clone()),
             crate::TraitItem::Type(v0) => crate::TraitItem::Type(v0.clone()),
             crate::TraitItem::Macro(v0) => crate::TraitItem::Macro(v0.clone()),
+            crate::TraitItem::BroadcastGroup(v0) => {
+                crate::TraitItem::BroadcastGroup(v0.clone())
+            }
             crate::TraitItem::Verbatim(v0) => crate::TraitItem::Verbatim(v0.clone()),
         }
     }
diff --git a/dependencies/syn/src/gen/debug.rs b/dependencies/syn/src/gen/debug.rs
index 06fe9e5aff..4b71043668 100644
--- a/dependencies/syn/src/gen/debug.rs
+++ b/dependencies/syn/src/gen/debug.rs
@@ -3470,6 +3470,11 @@ impl Debug for crate::TraitItem {
             crate::TraitItem::Fn(v0) => v0.debug(formatter, "Fn"),
             crate::TraitItem::Type(v0) => v0.debug(formatter, "Type"),
             crate::TraitItem::Macro(v0) => v0.debug(formatter, "Macro"),
+            crate::TraitItem::BroadcastGroup(v0) => {
+                let mut formatter = formatter.debug_tuple("BroadcastGroup");
+                formatter.field(v0);
+                formatter.finish()
+            }
             crate::TraitItem::Verbatim(v0) => {
                 let mut formatter = formatter.debug_tuple("Verbatim");
                 formatter.field(v0);
diff --git a/dependencies/syn/src/gen/eq.rs b/dependencies/syn/src/gen/eq.rs
index e5cb1da8f9..a5b37f4443 100644
--- a/dependencies/syn/src/gen/eq.rs
+++ b/dependencies/syn/src/gen/eq.rs
@@ -2457,6 +2457,10 @@ impl PartialEq for crate::TraitItem {
             (crate::TraitItem::Macro(self0), crate::TraitItem::Macro(other0)) => {
                 self0 == other0
             }
+            (
+                crate::TraitItem::BroadcastGroup(self0),
+                crate::TraitItem::BroadcastGroup(other0),
+            ) => self0 == other0,
             (crate::TraitItem::Verbatim(self0), crate::TraitItem::Verbatim(other0)) => {
                 TokenStreamHelper(self0) == TokenStreamHelper(other0)
             }
diff --git a/dependencies/syn/src/gen/fold.rs b/dependencies/syn/src/gen/fold.rs
index 7629ff4634..a185ece133 100644
--- a/dependencies/syn/src/gen/fold.rs
+++ b/dependencies/syn/src/gen/fold.rs
@@ -4330,6 +4330,9 @@ where
         crate::TraitItem::Macro(_binding_0) => {
             crate::TraitItem::Macro(f.fold_trait_item_macro(_binding_0))
         }
+        crate::TraitItem::BroadcastGroup(_binding_0) => {
+            crate::TraitItem::BroadcastGroup(f.fold_item_broadcast_group(_binding_0))
+        }
         crate::TraitItem::Verbatim(_binding_0) => crate::TraitItem::Verbatim(_binding_0),
     }
 }
diff --git a/dependencies/syn/src/gen/hash.rs b/dependencies/syn/src/gen/hash.rs
index 14b5b5e7a4..73105290b6 100644
--- a/dependencies/syn/src/gen/hash.rs
+++ b/dependencies/syn/src/gen/hash.rs
@@ -3124,8 +3124,12 @@ impl Hash for crate::TraitItem {
                 state.write_u8(3u8);
                 v0.hash(state);
             }
-            crate::TraitItem::Verbatim(v0) => {
+            crate::TraitItem::BroadcastGroup(v0) => {
                 state.write_u8(4u8);
+                v0.hash(state);
+            }
+            crate::TraitItem::Verbatim(v0) => {
+                state.write_u8(5u8);
                 TokenStreamHelper(v0).hash(state);
             }
         }
diff --git a/dependencies/syn/src/gen/visit.rs b/dependencies/syn/src/gen/visit.rs
index f650734945..c0713f208d 100644
--- a/dependencies/syn/src/gen/visit.rs
+++ b/dependencies/syn/src/gen/visit.rs
@@ -4416,6 +4416,9 @@ where
         crate::TraitItem::Macro(_binding_0) => {
             v.visit_trait_item_macro(_binding_0);
         }
+        crate::TraitItem::BroadcastGroup(_binding_0) => {
+            v.visit_item_broadcast_group(_binding_0);
+        }
         crate::TraitItem::Verbatim(_binding_0) => {
             skip!(_binding_0);
         }
diff --git a/dependencies/syn/src/gen/visit_mut.rs b/dependencies/syn/src/gen/visit_mut.rs
index 9db06f52c5..dbf508b290 100644
--- a/dependencies/syn/src/gen/visit_mut.rs
+++ b/dependencies/syn/src/gen/visit_mut.rs
@@ -4217,6 +4217,9 @@ where
         crate::TraitItem::Macro(_binding_0) => {
             v.visit_trait_item_macro_mut(_binding_0);
         }
+        crate::TraitItem::BroadcastGroup(_binding_0) => {
+            v.visit_item_broadcast_group_mut(_binding_0);
+        }
         crate::TraitItem::Verbatim(_binding_0) => {
             skip!(_binding_0);
         }
diff --git a/dependencies/syn/src/item.rs b/dependencies/syn/src/item.rs
index 6c3e878458..99ff27ccda 100644
--- a/dependencies/syn/src/item.rs
+++ b/dependencies/syn/src/item.rs
@@ -648,6 +648,9 @@ ast_enum_of_structs! {
         /// A macro invocation within the definition of a trait.
         Macro(TraitItemMacro),
 
+        /// A broadcast group
+        BroadcastGroup(ItemBroadcastGroup),
+
         /// Tokens within the definition of a trait not interpreted by Syn.
         Verbatim(TokenStream),
 
@@ -2531,7 +2534,9 @@ pub(crate) mod parsing {
 
             let lookahead = ahead.lookahead1();
             let allow_safe = false;
-            let mut item = if lookahead.peek(Token![fn]) || peek_signature(&ahead, allow_safe) {
+            let mut item = if lookahead.peek(Token![broadcast]) && input.peek2(Token![group]) {
+                input.parse().map(TraitItem::BroadcastGroup)
+            } else if lookahead.peek(Token![fn]) || peek_signature(&ahead, allow_safe) {
                 input.parse().map(TraitItem::Fn)
             } else if lookahead.peek(Token![const]) {
                 let publish = input.parse()?;
@@ -2602,6 +2607,7 @@ pub(crate) mod parsing {
                 TraitItem::Fn(item) => &mut item.attrs,
                 TraitItem::Type(item) => &mut item.attrs,
                 TraitItem::Macro(item) => &mut item.attrs,
+                TraitItem::BroadcastGroup(item) => &mut item.attrs,
                 TraitItem::Verbatim(_) => unreachable!(),
             };
             attrs.append(item_attrs);
diff --git a/dependencies/syn/syn.json b/dependencies/syn/syn.json
index 8908806149..a911b64ecd 100644
--- a/dependencies/syn/syn.json
+++ b/dependencies/syn/syn.json
@@ -6218,6 +6218,11 @@
             "syn": "TraitItemMacro"
           }
         ],
+        "BroadcastGroup": [
+          {
+            "syn": "ItemBroadcastGroup"
+          }
+        ],
         "Verbatim": [
           {
             "proc_macro2": "TokenStream"
diff --git a/dependencies/syn/tests/debug/gen.rs b/dependencies/syn/tests/debug/gen.rs
index 15b45ff179..b46e355f08 100644
--- a/dependencies/syn/tests/debug/gen.rs
+++ b/dependencies/syn/tests/debug/gen.rs
@@ -5794,6 +5794,13 @@ impl Debug for Lite<syn::TraitItem> {
                 }
                 formatter.finish()
             }
+            syn::TraitItem::BroadcastGroup(_val) => {
+                formatter.write_str("TraitItem::BroadcastGroup")?;
+                formatter.write_str("(")?;
+                Debug::fmt(Lite(_val), formatter)?;
+                formatter.write_str(")")?;
+                Ok(())
+            }
             syn::TraitItem::Verbatim(_val) => {
                 formatter.write_str("TraitItem::Verbatim")?;
                 formatter.write_str("(`")?;
diff --git a/source/builtin_macros/src/syntax.rs b/source/builtin_macros/src/syntax.rs
index dbf96012ef..1827323220 100644
--- a/source/builtin_macros/src/syntax.rs
+++ b/source/builtin_macros/src/syntax.rs
@@ -1566,6 +1566,7 @@ impl Visitor {
     fn visit_trait_items_prefilter(&mut self, items: &mut Vec<TraitItem>) {
         if self.rustdoc {
             for trait_item in items.iter_mut() {
+                let span = trait_item.span().clone();
                 match trait_item {
                     TraitItem::Fn(trait_item_method) => {
                         crate::rustdoc::process_trait_item_method(trait_item_method);
@@ -1581,6 +1582,7 @@ impl Visitor {
                     FnMode::Spec(_) | FnMode::SpecChecked(_) | FnMode::Proof(_) => false,
                     FnMode::Exec(_) | FnMode::Default => true,
                 },
+                TraitItem::BroadcastGroup(_) => false,
                 _ => true,
             });
         }
@@ -1591,6 +1593,7 @@ impl Visitor {
                 TraitItem::Fn(ref mut fun) => {
                     split_trait_method(&mut spec_items, fun, erase_ghost);
                 }
+                TraitItem::BroadcastGroup(item_broadcast_group) => {}
                 _ => {}
             }
         }
@@ -3612,6 +3615,17 @@ impl VisitMut for Visitor {
     fn visit_item_trait_mut(&mut self, tr: &mut ItemTrait) {
         tr.attrs.push(mk_verus_attr(tr.span(), quote! { verus_macro }));
         self.visit_trait_items_prefilter(&mut tr.items);
+        for trait_item in &mut tr.items {
+            let span = trait_item.span();
+            match trait_item {
+                TraitItem::BroadcastGroup(item_broadcast_group) => {
+                    *trait_item = TraitItem::Verbatim(
+                        self.handle_broadcast_group(item_broadcast_group, span),
+                    );
+                }
+                _ => (),
+            }
+        }
         self.filter_attrs(&mut tr.attrs);
         syn_verus::visit_mut::visit_item_trait_mut(self, tr);
     }
diff --git a/source/rust_verify_test/tests/broadcast_forall.rs b/source/rust_verify_test/tests/broadcast_forall.rs
index 9526f0f60d..f9844e0ee2 100644
--- a/source/rust_verify_test/tests/broadcast_forall.rs
+++ b/source/rust_verify_test/tests/broadcast_forall.rs
@@ -627,3 +627,26 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_vir_error_msg(err, "lemma_foo is not a broadcast proof fn")
 }
+
+test_verify_one_file! {
+    #[test] #[ignore] broadcast_group_in_trait verus_code! {
+        trait ATrait {
+            spec fn foo(i: int) -> bool;
+
+            broadcast proof fn lemma_foo(i: int)
+                ensures Self::foo(i)
+            {}
+
+            broadcast group group_foo {
+                // TODO see if we can auto-replace `Self` with the trait name
+                ATrait::lemma_foo,
+            }
+        }
+
+        proof fn lemma_bar<A: ATrait>() {
+            // broadcast use A::group_foo;
+
+            // assert(A::foo(0));
+        }
+    } => Ok(())
+}