diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs b/src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs
index c66f550f2..790a2c5ce 100644
--- a/src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs
@@ -151,9 +151,7 @@ pub fn make_daemon_set(fb: &FluentBit) -> (daemon_set: DaemonSet)
     daemon_set
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
     requires
         fb@.well_formed(),
diff --git a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs
index 657b6a870..1b6bf24c4 100644
--- a/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/proof/helper_invariants/proof.rs
@@ -175,9 +175,7 @@ pub proof fn lemma_eventually_always_every_resource_update_request_implies_at_af
     leads_to_always_tla_forall_subresource(spec, true_pred(), |sub_resource: SubResource| lift_state(every_resource_update_request_implies_at_after_update_resource_step(sub_resource, fb)));
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 pub proof fn make_fluentbit_pod_spec_determined_by_spec_and_name(fb1: FluentBitView, fb2: FluentBitView)
     requires
         fb1.metadata.name.get_Some_0() == fb2.metadata.name.get_Some_0(),
@@ -461,9 +459,7 @@ pub proof fn lemma_eventually_always_every_resource_create_request_implies_at_af
         lift_state(FBCluster::every_in_flight_req_msg_satisfies(requirements)));
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 pub proof fn lemma_always_no_update_status_request_msg_in_flight_of_except_daemon_set(spec: TempPred<FBCluster>, sub_resource: SubResource, fb: FluentBitView)
     requires
         spec.entails(lift_state(FBCluster::init())),
@@ -527,9 +523,7 @@ pub proof fn lemma_always_no_update_status_request_msg_in_flight_of_except_daemo
     init_invariant(spec, FBCluster::init(), stronger_next, inv);
 }
 
-// #[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 pub proof fn lemma_always_no_update_status_request_msg_not_from_bc_in_flight_of_daemon_set(spec: TempPred<FBCluster>, fb: FluentBitView)
     requires
         spec.entails(lift_state(FBCluster::init())),
diff --git a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs
index 42dcbd188..5077ff11d 100644
--- a/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/fluent_controller/fluentbit_config/proof/helper_invariants/proof.rs
@@ -436,9 +436,7 @@ pub proof fn lemma_eventually_always_every_resource_create_request_implies_at_af
         lift_state(FBCCluster::every_in_flight_req_msg_satisfies(requirements)));
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 pub proof fn lemma_always_no_update_status_request_msg_in_flight(spec: TempPred<FBCCluster>, sub_resource: SubResource, fbc: FluentBitConfigView)
     requires
         spec.entails(lift_state(FBCCluster::init())),
diff --git a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs
index ea3c6ff81..aa5db35ba 100644
--- a/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/rabbitmq_controller/proof/helper_invariants/proof.rs
@@ -114,9 +114,7 @@ pub proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_u
     lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(spec, rabbitmq);
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(spec: TempPred<RMQCluster>, rabbitmq: RabbitmqClusterView)
     requires
         spec.entails(always(lift_action(RMQCluster::next()))),
@@ -544,9 +542,7 @@ proof fn object_in_response_at_after_update_resource_step_is_same_as_etcd_helper
     }
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 proof fn lemma_always_request_at_after_get_request_step_is_resource_get_request(spec: TempPred<RMQCluster>, sub_resource: SubResource, rabbitmq: RabbitmqClusterView)
     requires
         spec.entails(lift_state(RMQCluster::init())),
@@ -996,9 +992,7 @@ pub proof fn lemma_always_no_update_status_request_msg_in_flight_of_except_state
     init_invariant(spec, RMQCluster::init(), RMQCluster::next(), inv);
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 pub proof fn lemma_always_no_update_status_request_msg_not_from_bc_in_flight_of_stateful_set(spec: TempPred<RMQCluster>, rabbitmq: RabbitmqClusterView)
     requires
         spec.entails(lift_state(RMQCluster::init())),
@@ -1229,9 +1223,7 @@ proof fn lemma_always_resource_object_create_or_update_request_msg_has_one_contr
 //
 // Tips: Talking about both s and s_prime give more information to those using this lemma and also makes the verification faster.
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 pub proof fn lemma_resource_update_request_msg_implies_key_in_reconcile_equals(sub_resource: SubResource, rabbitmq: RabbitmqClusterView, s: RMQCluster, s_prime: RMQCluster, msg: RMQMessage, step: RMQStep)
     requires
         !s.in_flight().contains(msg), s_prime.in_flight().contains(msg),
@@ -1826,8 +1818,6 @@ pub proof fn lemma_always_cm_rv_stays_unchanged(spec: TempPred<RMQCluster>, rabb
 }
 
 // We can probably hide a lof of spec functions to make this lemma faster
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
 pub proof fn lemma_always_no_create_resource_request_msg_without_name_in_flight(spec: TempPred<RMQCluster>, sub_resource: SubResource, rabbitmq: RabbitmqClusterView)
     requires
         spec.entails(lift_state(RMQCluster::init())),
diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
index 4a47b7124..35a7b3b95 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
@@ -915,9 +915,7 @@ pub proof fn lemma_always_no_update_status_request_msg_in_flight_of_except_state
     init_invariant(spec, ZKCluster::init(), stronger_next, inv);
 }
 
-//#[verifier(spinoff_prover)]
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
+#[verifier(spinoff_prover)]
 pub proof fn lemma_always_no_update_status_request_msg_not_from_bc_in_flight_of_stateful_set(spec: TempPred<ZKCluster>, zookeeper: ZookeeperClusterView)
     requires
         spec.entails(lift_state(ZKCluster::init())),
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
index 9fbc73f70..5378c9005 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
@@ -608,8 +608,6 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(
     );
 }
 
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
 proof fn lemma_resource_state_matches_at_after_create_resource_step(
     spec: TempPred<ZKCluster>, sub_resource: SubResource, zookeeper: ZookeeperClusterView, req_msg: ZKMessage
 )
@@ -951,8 +949,6 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(spec:
     );
 }
 
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
 pub proof fn lemma_resource_object_is_stable(spec: TempPred<ZKCluster>, sub_resource: SubResource, zookeeper: ZookeeperClusterView, p: TempPred<ZKCluster>)
     requires
         sub_resource != SubResource::StatefulSet,
diff --git a/src/kubernetes_cluster/proof/api_server_liveness.rs b/src/kubernetes_cluster/proof/api_server_liveness.rs
index 8f4d9ac4f..62fd41b94 100644
--- a/src/kubernetes_cluster/proof/api_server_liveness.rs
+++ b/src/kubernetes_cluster/proof/api_server_liveness.rs
@@ -412,8 +412,6 @@ proof fn lemma_pending_requests_number_is_n_leads_to_no_pending_requests(spec: T
     }
 }
 
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
 proof fn pending_requests_num_decreases(spec: TempPred<Self>, rest_id: RestId, msg_num: nat, msg: MsgType<E>)
     requires
         msg_num > 0,
diff --git a/src/kubernetes_cluster/proof/cluster.rs b/src/kubernetes_cluster/proof/cluster.rs
index 9036b859d..fd6e738f2 100644
--- a/src/kubernetes_cluster/proof/cluster.rs
+++ b/src/kubernetes_cluster/proof/cluster.rs
@@ -75,19 +75,6 @@ pub proof fn lemma_true_leads_to_busy_always_disabled(
     leads_to_stable::<Self>(spec, lift_action(Self::next()), true_pred(), lift_state(Self::busy_disabled()));
 }
 
-pub proof fn lemma_true_leads_to_pod_event_always_disabled(
-    spec: TempPred<Self>,
-)
-    requires
-        spec.entails(always(lift_action(Self::next()))),
-        spec.entails(Self::disable_pod_event().weak_fairness(())),
-    ensures spec.entails(true_pred().leads_to(always(lift_state(Self::pod_event_disabled())))),
-{
-    let true_state = |s: Self| true;
-    Self::disable_pod_event().wf1((), spec, Self::next(), true_state, Self::pod_event_disabled());
-    leads_to_stable::<Self>(spec, lift_action(Self::next()), true_pred(), lift_state(Self::pod_event_disabled()));
-}
-
 // This desired_state_is specifies the desired state (described in the cr object)
 // Informally, it says that given the cr object, the object's key exists in the etcd,
 // and the corresponding object in etcd has the same spec and uid of the given cr object.
diff --git a/src/kubernetes_cluster/proof/controller_runtime_safety.rs b/src/kubernetes_cluster/proof/controller_runtime_safety.rs
index 69f423097..03e7b2063 100644
--- a/src/kubernetes_cluster/proof/controller_runtime_safety.rs
+++ b/src/kubernetes_cluster/proof/controller_runtime_safety.rs
@@ -87,8 +87,6 @@ pub proof fn lemma_always_triggering_cr_has_lower_uid_than_uid_counter(spec: Tem
 //   - If the response is processed by the controller, the controller will create a new pending request in flight which
 //   allows the invariant to still hold.
 
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
 pub proof fn lemma_always_pending_req_in_flight_or_resp_in_flight_at_reconcile_state(spec: TempPred<Self>, key: ObjectRef, state: spec_fn(R::T) -> bool)
     requires
         forall |s| (#[trigger] state(s)) ==> s != R::reconcile_init_state(),
diff --git a/src/kubernetes_cluster/proof/daemon_set_controller.rs b/src/kubernetes_cluster/proof/daemon_set_controller.rs
index 3302b18d2..34dfa43d0 100644
--- a/src/kubernetes_cluster/proof/daemon_set_controller.rs
+++ b/src/kubernetes_cluster/proof/daemon_set_controller.rs
@@ -295,8 +295,6 @@ proof fn lemma_pending_update_status_req_num_is_n_leads_to_daemon_set_not_exist_
     }
 }
 
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
 proof fn daemon_set_not_exist_or_updated_or_pending_update_status_requests_num_decreases(spec: TempPred<Self>, key: ObjectRef, make_fn: spec_fn() -> DaemonSetView, msg_num: nat, msg: MsgType<E>)
     requires
         key.kind == DaemonSetView::kind(),
diff --git a/src/kubernetes_cluster/proof/stateful_set_controller.rs b/src/kubernetes_cluster/proof/stateful_set_controller.rs
index ed50b2bee..abb55be67 100644
--- a/src/kubernetes_cluster/proof/stateful_set_controller.rs
+++ b/src/kubernetes_cluster/proof/stateful_set_controller.rs
@@ -352,8 +352,6 @@ proof fn lemma_pending_update_status_req_num_is_n_leads_to_stateful_set_not_exis
     }
 }
 
-// TODO: broken by pod_event; Xudong will fix it later
-#[verifier(external_body)]
 proof fn stateful_set_not_exist_or_updated_or_pending_update_status_requests_num_decreases(
     spec: TempPred<Self>, key: ObjectRef, cm_key: ObjectRef, make_fn: spec_fn(rv: StringView) -> StatefulSetView, msg_num: nat, msg: MsgType<E>
 )
diff --git a/src/kubernetes_cluster/spec/cluster.rs b/src/kubernetes_cluster/spec/cluster.rs
index cfade6e2f..04310befb 100644
--- a/src/kubernetes_cluster/spec/cluster.rs
+++ b/src/kubernetes_cluster/spec/cluster.rs
@@ -10,7 +10,6 @@ use crate::kubernetes_cluster::spec::{
     external_api::types::ExternalAPIState,
     message::*,
     network::types::NetworkState,
-    pod_event::types::PodEventState,
 };
 use crate::reconciler::spec::reconciler::Reconciler;
 use vstd::{multiset::*, prelude::*};
@@ -32,7 +31,6 @@ pub struct Cluster<K: CustomResourceView, E: ExternalAPI, R: Reconciler<K, E>> {
     pub client_state: ClientState,
     pub network_state: NetworkState<E::Input, E::Output>,
     pub external_api_state: ExternalAPIState<E>,
-    pub pod_event_state: PodEventState,
     pub rest_id_allocator: RestIdAllocator,
     pub crash_enabled: bool,
     pub transient_failure_enabled: bool,
diff --git a/src/kubernetes_cluster/spec/cluster_state_machine.rs b/src/kubernetes_cluster/spec/cluster_state_machine.rs
index 9b9ada28c..bb3eed465 100644
--- a/src/kubernetes_cluster/spec/cluster_state_machine.rs
+++ b/src/kubernetes_cluster/spec/cluster_state_machine.rs
@@ -16,7 +16,6 @@ use crate::kubernetes_cluster::spec::{
     },
     external_api::types::{ExternalAPIAction, ExternalAPIActionInput},
     message::*,
-    pod_event::types::{PodEventActionInput, PodEventState},
 };
 use crate::reconciler::spec::reconciler::Reconciler;
 use crate::state_machine::{action::*, state_machine::*};
@@ -32,13 +31,11 @@ pub enum Step<Msg> {
     ControllerStep((Option<Msg>, Option<ObjectRef>)),
     ClientStep(),
     ExternalAPIStep(Option<Msg>),
-    PodEventStep(),
     ScheduleControllerReconcileStep(ObjectRef),
     RestartController(),
     DisableCrash(),
     FailTransientlyStep((Msg, APIError)),
     DisableTransientFailure(),
-    DisablePodEvent(),
     StutterStep(),
 }
 
@@ -52,7 +49,6 @@ pub open spec fn init() -> StatePred<Self> {
         &&& (Self::client().init)(s.client_state)
         &&& (Self::network().init)(s.network_state)
         &&& (Self::external_api().init)(s.external_api_state)
-        &&& (Self::pod_event().init)(s.pod_event_state)
         &&& s.crash_enabled
         &&& s.transient_failure_enabled
         &&& s.pod_event_enabled
@@ -356,52 +352,6 @@ pub open spec fn client_next() -> Action<Self, (), ()> {
     }
 }
 
-pub open spec fn pod_event_next() -> Action<Self, (), ()> {
-    let result = |input: (), s: Self| {
-        let host_result = Self::pod_event().next_result(
-            s.rest_id_allocator,
-            s.pod_event_state
-        );
-        let msg_ops = MessageOps {
-            recv: None,
-            send: host_result.get_Enabled_1().send,
-        };
-        let network_result = Self::network().next_result(msg_ops, s.network_state);
-
-        (host_result, network_result)
-    };
-    Action {
-        precondition: |input: (), s: Self| {
-            &&& s.pod_event_enabled
-            &&& result(input, s).0.is_Enabled()
-            &&& result(input, s).1.is_Enabled()
-        },
-        transition: |input: (), s: Self| {
-            let (host_result, network_result) = result(input, s);
-            (Self {
-                pod_event_state: host_result.get_Enabled_0(),
-                network_state: network_result.get_Enabled_0(),
-                rest_id_allocator: host_result.get_Enabled_1().rest_id_allocator,
-                ..s
-            }, ())
-        },
-    }
-}
-
-pub open spec fn disable_pod_event() -> Action<Self, (), ()> {
-    Action {
-        precondition: |input:(), s: Self| {
-            true
-        },
-        transition: |input: (), s: Self| {
-            (Self {
-                pod_event_enabled: false,
-                ..s
-            }, ())
-        }
-    }
-}
-
 pub open spec fn stutter() -> Action<Self, (), ()> {
     Action {
         precondition: |input: (), s: Self| {
@@ -420,13 +370,11 @@ pub open spec fn next_step(s: Self, s_prime: Self, step: Step<MsgType<E>>) -> bo
         Step::ControllerStep(input) => Self::controller_next().forward(input)(s, s_prime),
         Step::ClientStep() => Self::client_next().forward(())(s, s_prime),
         Step::ExternalAPIStep(input) => Self::external_api_next().forward(input)(s, s_prime),
-        Step::PodEventStep() => Self::pod_event_next().forward(())(s, s_prime),
         Step::ScheduleControllerReconcileStep(input) => Self::schedule_controller_reconcile().forward(input)(s, s_prime),
         Step::RestartController() => Self::restart_controller().forward(())(s, s_prime),
         Step::DisableCrash() => Self::disable_crash().forward(())(s, s_prime),
         Step::FailTransientlyStep(input) => Self::fail_request_transiently().forward(input)(s, s_prime),
         Step::DisableTransientFailure() => Self::disable_transient_failure().forward(())(s, s_prime),
-        Step::DisablePodEvent() => Self::disable_pod_event().forward(())(s, s_prime),
         Step::StutterStep() => Self::stutter().forward(())(s, s_prime),
     }
 }
@@ -450,7 +398,6 @@ pub open spec fn sm_wf_spec() -> TempPred<Self> {
     .and(tla_forall(|input| Self::schedule_controller_reconcile().weak_fairness(input)))
     .and(Self::disable_crash().weak_fairness(()))
     .and(Self::disable_transient_failure().weak_fairness(()))
-    .and(Self::disable_pod_event().weak_fairness(()))
 }
 
 pub open spec fn kubernetes_api_action_pre(action: ApiServerAction<E::Input, E::Output>, input: Option<MsgType<E>>) -> StatePred<Self> {
diff --git a/src/kubernetes_cluster/spec/message.rs b/src/kubernetes_cluster/spec/message.rs
index 67aa16989..7ceb0c3be 100644
--- a/src/kubernetes_cluster/spec/message.rs
+++ b/src/kubernetes_cluster/spec/message.rs
@@ -29,7 +29,6 @@ pub enum HostId {
     CustomController,
     ExternalAPI,
     Client,
-    PodEvent,
 }
 
 pub type RestId = nat;
@@ -261,10 +260,6 @@ pub open spec fn client_req_msg(msg_content: MessageContent<I, O>) -> Message<I,
     Message::form_msg(HostId::Client, HostId::ApiServer, msg_content)
 }
 
-pub open spec fn pod_event_req_msg(msg_content: MessageContent<I, O>) -> Message<I, O> {
-    Message::form_msg(HostId::PodEvent, HostId::ApiServer, msg_content)
-}
-
 pub open spec fn resp_msg_matches_req_msg(resp_msg: Message<I, O>, req_msg: Message<I, O>) -> bool {
     ||| {
         &&& resp_msg.content.is_APIResponse()
diff --git a/src/kubernetes_cluster/spec/mod.rs b/src/kubernetes_cluster/spec/mod.rs
index b4a325c45..5e89b703d 100644
--- a/src/kubernetes_cluster/spec/mod.rs
+++ b/src/kubernetes_cluster/spec/mod.rs
@@ -9,4 +9,3 @@ pub mod controller;
 pub mod external_api;
 pub mod message;
 pub mod network;
-pub mod pod_event;