diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs
index 794c7f36b..7951a4ae0 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/owner_ref.rs
@@ -7,6 +7,7 @@ use crate::kubernetes_api_objects::spec::{
     stateful_set::*,
 };
 use crate::kubernetes_cluster::spec::{
+    api_server::state_machine::generated_name_is_unique,
     builtin_controllers::types::BuiltinControllerChoice,
     cluster::*,
     cluster_state_machine::Step,
@@ -131,14 +132,26 @@ pub proof fn lemma_always_every_owner_ref_of_every_object_in_etcd_has_different_
     let next = |s, s_prime| {
         &&& ZKCluster::next()(s, s_prime)
         &&& object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, zookeeper)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
     };
     lemma_always_object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(spec, sub_resource, zookeeper);
-    combine_spec_entails_always_n!(spec, lift_action(next), lift_action(ZKCluster::next()), lift_state(object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, zookeeper)));
+    lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, zookeeper);
+    combine_spec_entails_always_n!(spec, lift_action(next), lift_action(ZKCluster::next()),
+        lift_state(object_in_every_resource_create_or_update_request_msg_only_has_valid_owner_references(sub_resource, zookeeper)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))
+    );
     let resource_key = get_request(sub_resource, zookeeper).key;
     assert forall |s, s_prime| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         if s_prime.resources().contains_key(resource_key) {
             assert(s.kubernetes_api_state.uid_counter <= s_prime.kubernetes_api_state.uid_counter);
-            if !s.resources().contains_key(resource_key) || s.resources()[resource_key].metadata.owner_references != s_prime.resources()[resource_key].metadata.owner_references {} else {}
+            let step = choose |step| ZKCluster::next_step(s, s_prime, step);
+            match step {
+                Step::ApiServerStep(input) => {
+                    assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0()));
+                    if !s.resources().contains_key(resource_key) || s.resources()[resource_key].metadata.owner_references != s_prime.resources()[resource_key].metadata.owner_references {} else {}
+                },
+                _ => {}
+            }
         }
     }
     init_invariant(spec, ZKCluster::init(), next, inv);
diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs
index c5368c0ab..a9f6df120 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/predicate.rs
@@ -229,12 +229,8 @@ pub open spec fn resource_object_only_has_owner_reference_pointing_to_current_cr
 }
 
 pub open spec fn no_create_resource_request_msg_with_empty_name_in_flight(sub_resource: SubResource, zookeeper: ZookeeperClusterView) -> StatePred<ZKCluster> {
-    |s: ZKCluster| {
-        forall |msg: ZKMessage| !{
-            &&& s.in_flight().contains(msg)
-            &&& #[trigger] resource_create_request_msg_with_empty_name(get_request(sub_resource, zookeeper).key.kind, get_request(sub_resource, zookeeper).key.namespace)(msg)
-        }
-    }
+    let resource_key = get_request(sub_resource, zookeeper).key;
+    ZKCluster::no_create_msg_that_uses_generate_name(resource_key.kind, resource_key.namespace)
 }
 
 pub open spec fn no_delete_resource_request_msg_in_flight(sub_resource: SubResource, zookeeper: ZookeeperClusterView) -> StatePred<ZKCluster> {
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 bbbe9dc13..7cec0d302 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/proof.rs
@@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{
     api_method::*, common::*, owner_reference::*, prelude::*, resource::*,
 };
 use crate::kubernetes_cluster::spec::{
+    api_server::state_machine::generated_name_is_unique,
     cluster::*,
     cluster_state_machine::Step,
     controller::types::{ControllerActionInput, ControllerStep},
@@ -168,9 +169,10 @@ pub proof fn lemma_eventually_always_cm_rv_is_the_same_as_etcd_server_cm_if_cm_u
             match step {
                 Step::ApiServerStep(input) => {
                     let req = input.get_Some_0();
-                    assert(!resource_delete_request_msg(get_request(SubResource::ConfigMap, zookeeper).key)(req));
-                    assert(!resource_update_status_request_msg(get_request(SubResource::ConfigMap, zookeeper).key)(req));
-                    if resource_update_request_msg(get_request(SubResource::ConfigMap, zookeeper).key)(req) {} else {}
+                    assert(!resource_delete_request_msg(cm_key)(req));
+                    assert(!resource_update_status_request_msg(cm_key)(req));
+                    generated_name_is_unique(s.kubernetes_api_state);
+                    if resource_update_request_msg(cm_key)(req) {} else {}
                 },
                 _ => {},
             }
@@ -191,6 +193,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
         spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper))))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper))))),
+        spec.entails(always(tla_forall(|res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper))))),
         spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper))))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper))))),
@@ -198,6 +201,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
 {
     always_tla_forall_apply(spec, |res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper)), SubResource::ConfigMap);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper)), SubResource::ConfigMap);
+    always_tla_forall_apply(spec, |res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), SubResource::ConfigMap);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper)), SubResource::ConfigMap);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), SubResource::ConfigMap);
     lemma_eventually_always_object_in_response_at_after_create_resource_step_is_same_as_etcd(spec, zookeeper);
@@ -216,6 +220,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
         spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))),
         spec.entails(always(lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)))),
         spec.entails(always(lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)))),
+        spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)))),
         spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))),
         spec.entails(always(lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)))),
         spec.entails(always(lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)))),
@@ -232,6 +237,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
         &&& ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(key)(s_prime)
         &&& no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)(s)
         &&& no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)(s)
         &&& object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)(s)
         &&& resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)(s)
     };
@@ -246,6 +252,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
         later(lift_state(ZKCluster::key_of_object_in_matched_ok_create_resp_message_is_same_as_key_of_pending_req(key))),
         lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)),
         lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)),
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)),
         lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper))
     );
@@ -293,6 +300,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_create_resource
                             assert(!resource_delete_request_msg(resource_key)(req_msg));
                             assert(!resource_update_request_msg(resource_key)(req_msg));
                             assert(!resource_update_status_request_msg(resource_key)(req_msg));
+                            assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req_msg));
                             match req_msg.content.get_APIRequest_0() {
                                 APIRequest::CreateRequest(_) => {
                                     if !s.in_flight().contains(msg) {
@@ -336,6 +344,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
         spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper))))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper))))),
+        spec.entails(always(tla_forall(|res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper))))),
         spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper))))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper))))),
@@ -343,6 +352,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
 {
     always_tla_forall_apply(spec, |res: SubResource| lift_state(no_delete_resource_request_msg_in_flight(res, zookeeper)), SubResource::ConfigMap);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(res, zookeeper)), SubResource::ConfigMap);
+    always_tla_forall_apply(spec, |res: SubResource| lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), SubResource::ConfigMap);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper)), SubResource::ConfigMap);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), SubResource::ConfigMap);
     lemma_eventually_always_object_in_response_at_after_update_resource_step_is_same_as_etcd(spec, zookeeper);
@@ -361,6 +371,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
         spec.entails(always(lift_state(ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(zookeeper.object_ref())))),
         spec.entails(always(lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)))),
         spec.entails(always(lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)))),
+        spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)))),
         spec.entails(true_pred().leads_to(lift_state(|s: ZKCluster| !s.ongoing_reconciles().contains_key(zookeeper.object_ref())))),
         spec.entails(always(lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)))),
         spec.entails(always(lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)))),
@@ -377,6 +388,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
         &&& ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(key)(s_prime)
         &&& no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)(s)
         &&& no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)(s)
         &&& object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)(s)
         &&& resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper)(s)
     };
@@ -391,6 +403,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
         later(lift_state(ZKCluster::key_of_object_in_matched_ok_update_resp_message_is_same_as_key_of_pending_req(key))),
         lift_state(no_delete_resource_request_msg_in_flight(SubResource::ConfigMap, zookeeper)),
         lift_state(no_update_status_request_msg_in_flight_of_except_stateful_set(SubResource::ConfigMap, zookeeper)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::ConfigMap, zookeeper)),
         lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(SubResource::ConfigMap, zookeeper)),
         lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::ConfigMap, zookeeper))
     );
@@ -438,6 +451,7 @@ pub proof fn lemma_eventually_always_object_in_response_at_after_update_resource
                             let req_msg = input.get_Some_0();
                             assert(!resource_delete_request_msg(resource_key)(req_msg));
                             assert(!resource_update_status_request_msg(resource_key)(req_msg));
+                            assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req_msg));
                             match req_msg.content.get_APIRequest_0() {
                                 APIRequest::UpdateRequest(_) => {
                                     if !s.in_flight().contains(msg) {
@@ -999,15 +1013,29 @@ pub proof fn lemma_always_resource_object_has_no_finalizers_or_timestamp_and_onl
 {
     let inv = resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper);
     lemma_always_resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(spec, sub_resource, zookeeper);
+    lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, zookeeper);
     let stronger_next = |s, s_prime| {
         &&& ZKCluster::next()(s, s_prime)
         &&& resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, zookeeper)(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
     };
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
         lift_action(ZKCluster::next()),
-        lift_state(resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, zookeeper))
+        lift_state(resource_object_create_or_update_request_msg_has_one_controller_ref_and_no_finalizers(sub_resource, zookeeper)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))
     );
+    let resource_key = get_request(sub_resource, zookeeper).key;
+    assert forall |s, s_prime| inv(s) && #[trigger] stronger_next(s, s_prime) implies inv(s_prime) by {
+        let step = choose |step| ZKCluster::next_step(s, s_prime, step);
+        match step {
+            Step::ApiServerStep(input) => {
+                let req_msg = input.get_Some_0();
+                assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req_msg));
+            }
+            _ => {}
+        }
+    }
     init_invariant(spec, ZKCluster::init(), stronger_next, inv);
 }
 
@@ -1405,12 +1433,14 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
         spec.entails(always(tla_forall(|sub_resource: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper))))),
         spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper))))),
         spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, zookeeper))))),
+        spec.entails(always(tla_forall(|sub_resource: SubResource|lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))))),
     ensures spec.entails(true_pred().leads_to(always(tla_forall(|sub_resource: SubResource| (lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper))))))),
 {
     assert forall |sub_resource: SubResource| spec.entails(true_pred().leads_to(always(lift_state(#[trigger] resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper))))) by {
         always_tla_forall_apply(spec, |res: SubResource| lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), sub_resource);
         always_tla_forall_apply(spec, |res: SubResource|lift_state(every_resource_create_request_implies_at_after_create_resource_step(res, zookeeper)), sub_resource);
         always_tla_forall_apply(spec, |res: SubResource|lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(res, zookeeper)), sub_resource);
+        always_tla_forall_apply(spec, |res: SubResource|lift_state(no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), sub_resource);
         lemma_eventually_always_resource_object_only_has_owner_reference_pointing_to_current_cr(spec, sub_resource, zookeeper);
     }
     leads_to_always_tla_forall_subresource(spec, true_pred(), |sub_resource: SubResource| lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)));
@@ -1427,6 +1457,7 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
         spec.entails(always(lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(object_in_every_resource_update_request_only_has_owner_references_pointing_to_current_cr(sub_resource, zookeeper)))),
+        spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))),
     ensures spec.entails(true_pred().leads_to(always(lift_state(resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper))))),
 {
     let key = get_request(sub_resource, zookeeper).key;
@@ -1438,11 +1469,13 @@ pub proof fn lemma_eventually_always_resource_object_only_has_owner_reference_po
     let state = |s: ZKCluster| {
         ZKCluster::desired_state_is(zookeeper)(s)
         && resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)(s)
+        && no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
     };
     invariant_n!(
         spec, lift_state(state), lift_state(ZKCluster::objects_owner_references_violates(key, eventual_owner_ref)).implies(lift_state(ZKCluster::garbage_collector_deletion_enabled(key))),
         lift_state(ZKCluster::desired_state_is(zookeeper)),
-        lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper))
+        lift_state(resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))
     );
     ZKCluster::lemma_eventually_objects_owner_references_satisfies(spec, key, eventual_owner_ref);
     temp_pred_equality(
@@ -1481,6 +1514,7 @@ pub proof fn lemma_eventually_always_stateful_set_not_exists_or_matches_or_no_mo
         spec.entails(always(lift_state(cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))),
         spec.entails(always(lift_state(sub_resource_state_matches(SubResource::ConfigMap, zookeeper)))),
         spec.entails(always(lift_state(no_update_status_request_msg_not_from_bc_in_flight_of_stateful_set(zookeeper)))),
+        spec.entails(always(lift_state(no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_action(cm_rv_stays_unchanged(zookeeper)))),
     ensures spec.entails(true_pred().leads_to(always(lift_state(stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper))))),
 {
@@ -1591,6 +1625,7 @@ pub proof fn lemma_always_cm_rv_stays_unchanged(spec: TempPred<ZKCluster>, zooke
                 let req = input.get_Some_0();
                 assert(!resource_delete_request_msg(cm_key)(req));
                 assert(!resource_update_status_request_msg(cm_key)(req));
+                generated_name_is_unique(s.kubernetes_api_state);
                 if resource_update_request_msg(cm_key)(req) {} else {}
             },
             _ => {},
diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs
index 987a453aa..64f847810 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/unchangeable.rs
@@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{
     api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*,
 };
 use crate::kubernetes_cluster::spec::{
+    api_server::state_machine::generated_name_is_unique,
     cluster::*,
     cluster_state_machine::Step,
     controller::types::{ControllerActionInput, ControllerStep},
@@ -128,6 +129,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<Z
         &&& object_in_every_create_request_msg_satisfies_unchangeable(sub_resource, zookeeper)(s)
         &&& response_at_after_get_resource_step_is_resource_get_response(sub_resource, zookeeper)(s)
         &&& the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())(s)
+        &&& no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
     };
     ZKCluster::lemma_always_each_object_in_reconcile_has_consistent_key_and_valid_metadata(spec);
     ZKCluster::lemma_always_each_object_in_etcd_is_well_formed(spec);
@@ -137,6 +139,7 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<Z
     lemma_always_object_in_every_create_request_msg_satisfies_unchangeable(spec, sub_resource, zookeeper);
     lemma_always_response_at_after_get_resource_step_is_resource_get_response(spec, sub_resource, zookeeper);
     lemma_always_the_object_in_reconcile_satisfies_state_validation(spec, zookeeper.object_ref());
+    lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, zookeeper);
     combine_spec_entails_always_n!(
         spec, lift_action(next), lift_action(ZKCluster::next()),
         lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
@@ -146,7 +149,8 @@ pub proof fn lemma_always_object_in_etcd_satisfies_unchangeable(spec: TempPred<Z
         lift_state(object_in_resource_update_request_msg_has_smaller_rv_than_etcd(sub_resource, zookeeper)),
         lift_state(object_in_every_create_request_msg_satisfies_unchangeable(sub_resource, zookeeper)),
         lift_state(response_at_after_get_resource_step_is_resource_get_response(sub_resource, zookeeper)),
-        lift_state(the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref()))
+        lift_state(the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())),
+        lift_state(no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper))
     );
     assert forall |s: ZKCluster, s_prime: ZKCluster| inv(s) && #[trigger] next(s, s_prime) implies inv(s_prime) by {
         object_in_etcd_satisfies_unchangeable_induction(sub_resource, zookeeper, s, s_prime);
@@ -166,6 +170,7 @@ pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubRe
         ZKCluster::each_object_in_etcd_is_well_formed()(s_prime),
         object_in_resource_update_request_msg_has_smaller_rv_than_etcd(sub_resource, zookeeper)(s),
         object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)(s),
+        no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s),
     ensures object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)(s_prime),
 {
     let resource_key = get_request(sub_resource, zookeeper).key;
@@ -187,6 +192,7 @@ pub proof fn object_in_etcd_satisfies_unchangeable_induction(sub_resource: SubRe
                 let req = input.get_Some_0();
                 if resource_create_request_msg(resource_key)(req) {} else {}
                 if resource_update_request_msg(resource_key)(req) {} else {}
+                if resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(req) {} else {}
             },
             _ => {}
         }
diff --git a/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs b/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs
index ff2645f8d..dd2b70e63 100644
--- a/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs
+++ b/src/controller_examples/zookeeper_controller/proof/helper_invariants/validation.rs
@@ -7,6 +7,7 @@ use crate::kubernetes_api_objects::spec::{
     stateful_set::*,
 };
 use crate::kubernetes_cluster::spec::{
+    api_server::state_machine::generated_name_is_unique,
     cluster::*,
     cluster_state_machine::Step,
     controller::types::{ControllerActionInput, ControllerStep},
@@ -101,6 +102,7 @@ pub proof fn lemma_always_stateful_set_in_etcd_satisfies_unchangeable(spec: Temp
                         assert(owner_refs.get_Some_0()[0] != ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0().controller_owner_ref());
                     }
                 } else if s.resources()[key] != s_prime.resources()[key] {
+                    generated_name_is_unique(s.kubernetes_api_state);
                     assert(s.resources()[key].metadata.uid == s_prime.resources()[key].metadata.uid);
                     assert(ZookeeperClusterView::unmarshal(s.resources()[key]).get_Ok_0().controller_owner_ref() == ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0().controller_owner_ref());
                     assert(ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0()
@@ -114,6 +116,7 @@ pub proof fn lemma_always_stateful_set_in_etcd_satisfies_unchangeable(spec: Temp
                         let req = input.get_Some_0();
                         if resource_create_request_msg(sts_key)(req) {} else {}
                         if resource_update_request_msg(sts_key)(req) {} else {}
+                        generated_name_is_unique(s.kubernetes_api_state);
                     },
                     _ => {}
                 }
@@ -305,6 +308,7 @@ proof fn lemma_always_stateful_set_in_create_request_msg_satisfies_unchangeable(
                     assert(s.controller_state == s_prime.controller_state);
                     assert(s.in_flight().contains(msg));
                     if s.resources().contains_key(key) {
+                        generated_name_is_unique(s.kubernetes_api_state);
                         assert(ZookeeperClusterView::unmarshal(s_prime.resources()[key]).get_Ok_0()
                         .transition_validation(ZookeeperClusterView::unmarshal(s.resources()[key]).get_Ok_0()));
                     } else {
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs
index c5d57af70..377d7766f 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/proof.rs
@@ -380,6 +380,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred<ZKCluster>, sub
         spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper))))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(res, zookeeper))))),
         spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(res, zookeeper))))),
+        spec.entails(always(tla_forall(|res: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper))))),
     ensures
         spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))),
@@ -388,6 +389,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred<ZKCluster>, sub
         spec.entails(always(lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))),
 {
     always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(res, zookeeper)), sub_resource);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(res, zookeeper)), sub_resource);
@@ -396,6 +398,7 @@ proof fn always_tla_forall_apply_for_sub_resource(spec: TempPred<ZKCluster>, sub
     always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(res, zookeeper)), sub_resource);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(res, zookeeper)), sub_resource);
     always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(res, zookeeper)), sub_resource);
+    always_tla_forall_apply(spec, |res: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(res, zookeeper)), sub_resource);
 }
 
 }
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 fd9ae2625..63ae78bd2 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/resource_match.rs
@@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{
     api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*,
 };
 use crate::kubernetes_cluster::spec::{
+    api_server::state_machine::generated_name_is_unique,
     builtin_controllers::types::BuiltinControllerChoice,
     cluster::*,
     cluster_state_machine::Step,
@@ -43,6 +44,7 @@ pub proof fn lemma_from_after_get_resource_step_to_resource_matches(
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::no_update_status_request_msg_in_flight_of_except_stateful_set(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(sub_resource, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)))),
@@ -99,6 +101,7 @@ pub proof fn lemma_from_after_get_resource_step_and_key_not_exists_to_resource_m
         spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))),
         spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))),
     ensures
         spec.entails(
@@ -445,6 +448,7 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou
         spec.entails(always(lift_state(ZKCluster::crash_disabled()))),
         spec.entails(always(lift_state(ZKCluster::busy_disabled()))),
         spec.entails(always(lift_state(ZKCluster::every_in_flight_msg_has_unique_id()))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))),
     ensures
         spec.entails(
@@ -461,12 +465,13 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou
             ))
         ),
 {
+    let resource_key = get_request(sub_resource, zookeeper).key;
     let pre = |s: ZKCluster| {
-        &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key)
+        &&& !s.resources().contains_key(resource_key)
         &&& req_msg_is_the_in_flight_pending_req_at_after_get_resource_step(sub_resource, zookeeper, req_msg)(s)
     };
     let post = |s: ZKCluster| {
-        &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key)
+        &&& !s.resources().contains_key(resource_key)
         &&& at_after_get_resource_step_and_exists_not_found_resp_in_flight(sub_resource, zookeeper)(s)
     };
     let input = Some(req_msg);
@@ -475,6 +480,7 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou
         &&& ZKCluster::crash_disabled()(s)
         &&& ZKCluster::busy_disabled()(s)
         &&& ZKCluster::every_in_flight_msg_has_unique_id()(s)
+        &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
         &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)(s)
     };
     combine_spec_entails_always_n!(
@@ -483,6 +489,7 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou
         lift_state(ZKCluster::crash_disabled()),
         lift_state(ZKCluster::busy_disabled()),
         lift_state(ZKCluster::every_in_flight_msg_has_unique_id()),
+        lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)),
         lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper))
     );
 
@@ -490,7 +497,8 @@ proof fn lemma_from_key_not_exists_to_receives_not_found_resp_at_after_get_resou
         let step = choose |step| ZKCluster::next_step(s, s_prime, step);
         match step {
             Step::ApiServerStep(input) => {
-                assert(!resource_create_request_msg(get_request(sub_resource, zookeeper).key)(input.get_Some_0()));
+                assert(!resource_create_request_msg(resource_key)(input.get_Some_0()));
+                assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0()));
                 if input.get_Some_0() == req_msg {
                     let resp_msg = ZKCluster::handle_get_request_msg(req_msg, s.kubernetes_api_state).1;
                     assert({
@@ -532,6 +540,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(
         spec.entails(always(lift_state(ZKCluster::each_object_in_etcd_is_well_formed()))),
         spec.entails(always(lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))),
         spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))),
     ensures
@@ -547,14 +556,15 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(
             }))
         ),
 {
+    let resource_key = get_request(sub_resource, zookeeper).key;
     let pre = |s: ZKCluster| {
-        &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key)
+        &&& !s.resources().contains_key(resource_key)
         &&& resp_msg_is_the_in_flight_resp_at_after_get_resource_step(sub_resource, zookeeper, resp_msg)(s)
         &&& resp_msg.content.get_get_response().res.is_Err()
         &&& resp_msg.content.get_get_response().res.get_Err_0().is_ObjectNotFound()
     };
     let post = |s: ZKCluster| {
-        &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key)
+        &&& !s.resources().contains_key(resource_key)
         &&& pending_req_in_flight_at_after_create_resource_step(sub_resource, zookeeper)(s)
     };
     let input = (Some(resp_msg), Some(zookeeper.object_ref()));
@@ -565,6 +575,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(
         &&& ZKCluster::each_object_in_etcd_is_well_formed()(s)
         &&& ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
         &&& ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())(s)
+        &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
         &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)(s)
         &&& helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)(s)
     };
@@ -577,6 +588,7 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(
         lift_state(ZKCluster::each_object_in_etcd_is_well_formed()),
         lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
         lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())),
+        lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)),
         lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)),
         lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper))
     );
@@ -585,7 +597,8 @@ proof fn lemma_from_after_get_resource_step_to_after_create_resource_step(
         let step = choose |step| ZKCluster::next_step(s, s_prime, step);
         match step {
             Step::ApiServerStep(input) => {
-                assert(!resource_create_request_msg(get_request(sub_resource, zookeeper).key)(input.get_Some_0()));
+                assert(!resource_create_request_msg(resource_key)(input.get_Some_0()));
+                assert(!resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0()));
             },
             _ => {}
         }
@@ -608,6 +621,7 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step(
         spec.entails(always(lift_state(ZKCluster::each_object_in_etcd_is_well_formed()))),
         spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))),
         spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)))),
     ensures
         spec.entails(
@@ -622,8 +636,9 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step(
             )
         ),
 {
+    let resource_key = get_request(sub_resource, zookeeper).key;
     let pre = |s: ZKCluster| {
-        &&& !s.resources().contains_key(get_request(sub_resource, zookeeper).key)
+        &&& !s.resources().contains_key(resource_key)
         &&& req_msg_is_the_in_flight_pending_req_at_after_create_resource_step(sub_resource, zookeeper, req_msg)(s)
     };
     let input = Some(req_msg);
@@ -635,6 +650,7 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step(
         &&& ZKCluster::each_object_in_etcd_is_well_formed()(s)
         &&& helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())(s)
         &&& helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)(s)
+        &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)(s)
         &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper)(s)
     };
     combine_spec_entails_always_n!(
@@ -646,6 +662,7 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step(
         lift_state(ZKCluster::each_object_in_etcd_is_well_formed()),
         lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())),
         lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)),
+        lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)),
         lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(sub_resource, zookeeper))
     );
 
@@ -671,7 +688,8 @@ proof fn lemma_resource_state_matches_at_after_create_resource_step(
         let step = choose |step| ZKCluster::next_step(s, s_prime, step);
         match step {
             Step::ApiServerStep(input) => {
-                if resource_create_request_msg(get_request(sub_resource, zookeeper).key)(input.get_Some_0()) {} else {}
+                if resource_create_request_msg(resource_key)(input.get_Some_0()) {} else {}
+                if resource_create_request_msg_with_empty_name(resource_key.kind, resource_key.namespace)(input.get_Some_0()) {} else {}
             },
             _ => {},
         }
@@ -847,6 +865,7 @@ proof fn lemma_resource_state_matches_at_after_update_resource_step(spec: TempPr
                 assert(!resource_delete_request_msg(resource_key)(input.get_Some_0()));
                 assert(!resource_update_status_request_msg(resource_key)(input.get_Some_0()));
                 if resource_update_request_msg(resource_key)(input.get_Some_0()) {} else {}
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {},
         }
@@ -881,6 +900,7 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(spec:
     let pre = resp_msg_is_the_in_flight_ok_resp_at_after_get_resource_step(sub_resource, zookeeper, resp_msg);
     let post = pending_req_in_flight_at_after_update_resource_step(sub_resource, zookeeper);
     let input = (Some(resp_msg), Some(zookeeper.object_ref()));
+    let resource_key = get_request(sub_resource, zookeeper).key;
     let stronger_next = |s, s_prime: ZKCluster| {
         &&& ZKCluster::next()(s, s_prime)
         &&& ZKCluster::crash_disabled()(s)
@@ -917,9 +937,10 @@ proof fn lemma_from_after_get_resource_step_to_after_update_resource_step(spec:
         match step {
             Step::ApiServerStep(input) => {
                 let req = input.get_Some_0();
-                assert(!resource_update_status_request_msg(get_request(sub_resource, zookeeper).key)(req));
-                assert(!resource_delete_request_msg(get_request(sub_resource, zookeeper).key)(req));
-                if resource_update_request_msg(get_request(sub_resource, zookeeper).key)(req) {} else {}
+                assert(!resource_update_status_request_msg(resource_key)(req));
+                assert(!resource_delete_request_msg(resource_key)(req));
+                if resource_update_request_msg(resource_key)(req) {} else {}
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {},
         }
@@ -968,9 +989,10 @@ pub proof fn lemma_resource_object_is_stable(spec: TempPred<ZKCluster>, sub_reso
         match step {
             Step::ApiServerStep(input) => {
                 let req = input.get_Some_0();
-                assert(!resource_delete_request_msg(get_request(sub_resource, zookeeper).key)(req));
-                assert(!resource_update_status_request_msg(get_request(sub_resource, zookeeper).key)(req));
-                if resource_update_request_msg(get_request(sub_resource, zookeeper).key)(req) {} else {}
+                assert(!resource_delete_request_msg(resource_key)(req));
+                assert(!resource_update_status_request_msg(resource_key)(req));
+                if resource_update_request_msg(resource_key)(req) {} else {}
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {},
         }
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs b/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs
index 35fe922d2..8299ee76e 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/spec.rs
@@ -230,6 +230,7 @@ pub open spec fn derived_invariants_since_beginning(zookeeper: ZookeeperClusterV
     .and(always(tla_forall(|res: SubResource| lift_state(ZKCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(get_request(res, zookeeper).key)))))
     .and(always(lift_state(helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(zookeeper))))
     .and(always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper)))))
+    .and(always(tla_forall(|sub_resource: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper)))))
 }
 
 pub proof fn derived_invariants_since_beginning_is_stable(zookeeper: ZookeeperClusterView)
@@ -241,6 +242,7 @@ pub proof fn derived_invariants_since_beginning_is_stable(zookeeper: ZookeeperCl
     let a_to_p_4 = |res: SubResource| lift_state(helper_invariants::response_at_after_get_resource_step_is_resource_get_response(res, zookeeper));
     let a_to_p_5 = |res: SubResource| lift_state(ZKCluster::object_in_ok_get_resp_is_same_as_etcd_with_same_rv(get_request(res, zookeeper).key));
     let a_to_p_6 = |sub_resource: SubResource| lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(sub_resource, zookeeper));
+    let a_to_p_7 = |sub_resource: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper));
     stable_and_always_n!(
         lift_state(ZKCluster::every_in_flight_msg_has_unique_id()),
         lift_state(ZKCluster::object_in_ok_get_response_has_smaller_rv_than_etcd()),
@@ -268,7 +270,8 @@ pub proof fn derived_invariants_since_beginning_is_stable(zookeeper: ZookeeperCl
         tla_forall(a_to_p_4),
         tla_forall(a_to_p_5),
         lift_state(helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(zookeeper)),
-        tla_forall(a_to_p_6)
+        tla_forall(a_to_p_6),
+        tla_forall(a_to_p_7)
     );
 }
 
@@ -535,6 +538,13 @@ pub proof fn sm_spec_entails_all_invariants(zookeeper: ZookeeperClusterView)
         }
         spec_entails_always_tla_forall(spec, a_to_p_6);
     });
+    let a_to_p_7 = |sub_resource: SubResource| lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(sub_resource, zookeeper));
+    assert_by(spec.entails(always(tla_forall(a_to_p_7))), {
+        assert forall |sub_resource: SubResource| spec.entails(always(#[trigger] a_to_p_7(sub_resource))) by {
+            helper_invariants::lemma_always_no_create_resource_request_msg_with_empty_name_in_flight(spec, sub_resource, zookeeper);
+        }
+        spec_entails_always_tla_forall(spec, a_to_p_7);
+    });
 
     entails_always_and_n!(
         spec,
@@ -564,7 +574,8 @@ pub proof fn sm_spec_entails_all_invariants(zookeeper: ZookeeperClusterView)
         tla_forall(a_to_p_4),
         tla_forall(a_to_p_5),
         lift_state(helper_invariants::stateful_set_in_etcd_satisfies_unchangeable(zookeeper)),
-        tla_forall(a_to_p_6)
+        tla_forall(a_to_p_6),
+        tla_forall(a_to_p_7)
     );
 }
 
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs b/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs
index 37b008d32..389c8b070 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/stateful_set_match.rs
@@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{
     api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*,
 };
 use crate::kubernetes_cluster::spec::{
+    api_server::state_machine::generated_name_is_unique,
     builtin_controllers::types::BuiltinControllerChoice,
     cluster::*,
     cluster_state_machine::Step,
@@ -41,6 +42,7 @@ pub proof fn lemma_from_after_get_stateful_set_step_to_stateful_set_matches(
         spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::stateful_set_not_exists_or_matches_or_no_more_status_update(zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(SubResource::StatefulSet, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::cm_rv_is_the_same_as_etcd_server_cm_if_cm_updated(zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(SubResource::StatefulSet, zookeeper)))),
@@ -256,6 +258,7 @@ proof fn lemma_from_key_exists_to_receives_ok_resp_at_after_get_stateful_set_ste
                 assert(!resource_delete_request_msg(resource_key)(req));
                 assert(!resource_update_request_msg(resource_key)(req));
                 assert(!resource_update_status_request_msg(resource_key)(req));
+                generated_name_is_unique(s.kubernetes_api_state);
                 if input.get_Some_0() == req_msg {
                     let resp_msg = ZKCluster::handle_get_request_msg(req_msg, s.kubernetes_api_state).1;
                     assert({
@@ -374,6 +377,7 @@ proof fn lemma_from_after_get_stateful_set_step_to_after_update_stateful_set_ste
                 assert(!resource_delete_request_msg(resource_key)(req));
                 assert(!resource_update_request_msg(resource_key)(req));
                 assert(!resource_update_status_request_msg(resource_key)(req));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -471,6 +475,7 @@ proof fn lemma_stateful_set_state_matches_at_after_update_stateful_set_step(spec
                 assert(!resource_delete_request_msg(resource_key)(req));
                 assert(!resource_update_status_request_msg(resource_key)(req));
                 if resource_update_request_msg(resource_key)(req) {} else {}
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -520,6 +525,7 @@ pub proof fn lemma_stateful_set_is_stable(
                 let req = input.get_Some_0();
                 assert(!resource_delete_request_msg(resource_key)(req));
                 if resource_update_request_msg(resource_key)(req) {} else {}
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
diff --git a/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs b/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs
index a93a2fd3b..1a1a11f9c 100644
--- a/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs
+++ b/src/controller_examples/zookeeper_controller/proof/liveness/zookeeper_api.rs
@@ -6,6 +6,7 @@ use crate::kubernetes_api_objects::spec::{
     api_method::*, common::*, dynamic::*, owner_reference::*, prelude::*, resource::*,
 };
 use crate::kubernetes_cluster::spec::{
+    api_server::state_machine::generated_name_is_unique,
     builtin_controllers::types::BuiltinControllerChoice,
     cluster::*,
     cluster_state_machine::Step,
@@ -41,6 +42,7 @@ pub proof fn lemma_from_after_exists_stateful_set_step_to_after_get_stateful_set
         spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(SubResource::StatefulSet, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::StatefulSet, zookeeper)))),
@@ -82,6 +84,7 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_not_exists_to_after_g
         spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))),
         spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))),
     ensures
         spec.entails(
             lift_state(|s: ZKCluster| {
@@ -160,6 +163,7 @@ proof fn lemma_from_after_exists_stateful_set_step_and_key_exists_to_after_get_s
         spec.entails(always(lift_state(helper_invariants::the_object_in_reconcile_satisfies_state_validation(zookeeper.object_ref())))),
         spec.entails(always(lift_state(helper_invariants::every_resource_update_request_implies_at_after_update_resource_step(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::no_delete_resource_request_msg_in_flight(SubResource::StatefulSet, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_only_has_owner_reference_pointing_to_current_cr(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::object_in_etcd_satisfies_unchangeable(SubResource::StatefulSet, zookeeper)))),
         spec.entails(always(lift_state(helper_invariants::resource_object_has_no_finalizers_or_timestamp_and_only_has_controller_owner_ref(SubResource::StatefulSet, zookeeper)))),
@@ -494,6 +498,7 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state
         spec.entails(always(lift_state(ZKCluster::busy_disabled()))),
         spec.entails(always(lift_state(ZKCluster::every_in_flight_msg_has_unique_id()))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))),
     ensures
         spec.entails(
             lift_state(|s: ZKCluster| {
@@ -506,12 +511,13 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state
                 }))
         ),
 {
+    let key = get_request(SubResource::StatefulSet, zookeeper).key;
     let pre = |s: ZKCluster| {
-        &&& !s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key)
+        &&& !s.resources().contains_key(key)
         &&& req_msg_is_the_in_flight_pending_req_at_after_exists_stateful_set_step(zookeeper, req_msg)(s)
     };
     let post = |s: ZKCluster| {
-        &&& !s.resources().contains_key(get_request(SubResource::StatefulSet, zookeeper).key)
+        &&& !s.resources().contains_key(key)
         &&& at_after_exists_stateful_set_step_and_exists_not_found_resp_in_flight(zookeeper)(s)
     };
     let input = Some(req_msg);
@@ -521,6 +527,7 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state
         &&& ZKCluster::busy_disabled()(s)
         &&& ZKCluster::every_in_flight_msg_has_unique_id()(s)
         &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)(s)
+        &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)(s)
     };
     combine_spec_entails_always_n!(
         spec, lift_action(stronger_next),
@@ -528,14 +535,16 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_state
         lift_state(ZKCluster::crash_disabled()),
         lift_state(ZKCluster::busy_disabled()),
         lift_state(ZKCluster::every_in_flight_msg_has_unique_id()),
-        lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper))
+        lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)),
+        lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper))
     );
 
     assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by {
         let step = choose |step| ZKCluster::next_step(s, s_prime, step);
         match step {
             Step::ApiServerStep(input) => {
-                assert(!resource_create_request_msg(get_request(SubResource::StatefulSet, zookeeper).key)(input.get_Some_0()));
+                assert(!resource_create_request_msg(key)(input.get_Some_0()));
+                assert(!resource_create_request_msg_with_empty_name(key.kind, key.namespace)(input.get_Some_0()));
                 if input.get_Some_0() == req_msg {
                     let resp_msg = ZKCluster::handle_get_request_msg(req_msg, s.kubernetes_api_state).1;
                     assert({
@@ -574,6 +583,7 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_
         spec.entails(always(lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()))),
         spec.entails(always(lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())))),
         spec.entails(always(lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)))),
+        spec.entails(always(lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)))),
     ensures
         spec.entails(
             lift_state(|s: ZKCluster| {
@@ -602,6 +612,7 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_
         &&& ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()(s)
         &&& ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())(s)
         &&& helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)(s)
+        &&& helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper)(s)
     };
 
     combine_spec_entails_always_n!(
@@ -613,7 +624,8 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_
         lift_state(ZKCluster::every_in_flight_req_msg_has_different_id_from_pending_req_msg_of(zookeeper.object_ref())),
         lift_state(ZKCluster::each_object_in_reconcile_has_consistent_key_and_valid_metadata()),
         lift_state(ZKCluster::pending_req_of_key_is_unique_with_unique_id(zookeeper.object_ref())),
-        lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper))
+        lift_state(helper_invariants::every_resource_create_request_implies_at_after_create_resource_step(SubResource::StatefulSet, zookeeper)),
+        lift_state(helper_invariants::no_create_resource_request_msg_with_empty_name_in_flight(SubResource::StatefulSet, zookeeper))
     );
 
     assert forall |s, s_prime| pre(s) && #[trigger] stronger_next(s, s_prime) implies pre(s_prime) || post(s_prime) by {
@@ -622,6 +634,7 @@ proof fn lemma_from_at_after_exists_stateful_set_step_to_after_get_stateful_set_
             Step::ApiServerStep(input) => {
                 let sts_key = get_request(SubResource::StatefulSet, zookeeper).key;
                 assert(!resource_create_request_msg(sts_key)(input.get_Some_0()));
+                assert(!resource_create_request_msg_with_empty_name(sts_key.kind, sts_key.namespace)(input.get_Some_0()));
             },
             _ => {}
         }
@@ -868,6 +881,7 @@ proof fn lemma_from_pending_req_to_receives_ok_resp_at_after_exists_zk_node_step
             Step::ApiServerStep(input) => {
                 assert(!resource_delete_request_msg(resource_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(resource_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -960,6 +974,7 @@ proof fn lemma_from_after_exists_zk_node_step_to_after_update_zk_node_step(spec:
             Step::ApiServerStep(input) => {
                 assert(!resource_delete_request_msg(sts_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(sts_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -1045,6 +1060,7 @@ proof fn lemma_from_pending_req_to_receives_ok_resp_at_after_update_zk_node_step
             Step::ApiServerStep(input) => {
                 assert(!resource_delete_request_msg(sts_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(sts_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -1199,6 +1215,7 @@ proof fn lemma_from_pending_req_to_receives_not_found_resp_at_after_exists_zk_no
             Step::ApiServerStep(input) => {
                 assert(!resource_delete_request_msg(sts_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(sts_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -1291,6 +1308,7 @@ proof fn lemma_from_after_exists_zk_node_step_to_after_create_zk_parent_node_ste
                 let sts_key = get_request(SubResource::StatefulSet, zookeeper).key;
                 assert(!resource_delete_request_msg(sts_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(sts_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -1386,6 +1404,7 @@ proof fn lemma_from_pending_req_to_receives_ok_or_already_exists_resp_at_after_c
                 let sts_key = get_request(SubResource::StatefulSet, zookeeper).key;
                 assert(!resource_delete_request_msg(sts_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(sts_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             }
             _ => {}
         }
@@ -1482,6 +1501,7 @@ proof fn lemma_from_after_create_zk_parent_node_step_to_after_create_zk_node_ste
             Step::ApiServerStep(input) => {
                 assert(!resource_delete_request_msg(sts_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(sts_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
@@ -1567,6 +1587,7 @@ proof fn lemma_from_pending_req_to_receives_ok_resp_at_after_create_zk_node_step
             Step::ApiServerStep(input) => {
                 assert(!resource_delete_request_msg(sts_key)(input.get_Some_0()));
                 assert(!resource_update_request_msg(sts_key)(input.get_Some_0()));
+                generated_name_is_unique(s.kubernetes_api_state);
             },
             _ => {}
         }
diff --git a/src/kubernetes_cluster/proof/builtin_controllers.rs b/src/kubernetes_cluster/proof/builtin_controllers.rs
index bb61334f3..b17403aaf 100644
--- a/src/kubernetes_cluster/proof/builtin_controllers.rs
+++ b/src/kubernetes_cluster/proof/builtin_controllers.rs
@@ -51,9 +51,10 @@ pub open spec fn no_create_msg_that_uses_generate_name(
     kind: Kind, namespace: StringView
 ) -> StatePred<Self> {
     |s: Self| {
-        forall |msg: MsgType<E>|
-            #[trigger] resource_create_request_msg_with_empty_name(kind, namespace)(msg)
-            ==> !s.in_flight().contains(msg)
+        forall |msg: MsgType<E>| !{
+            &&& s.in_flight().contains(msg)
+            &&& #[trigger] resource_create_request_msg_with_empty_name(kind, namespace)(msg)
+        }
     }
 }