diff --git a/src/controller_examples/zookeeper_controller/exec/reconciler.rs b/src/controller_examples/zookeeper_controller/exec/reconciler.rs
index 68734102a..a07618f39 100644
--- a/src/controller_examples/zookeeper_controller/exec/reconciler.rs
+++ b/src/controller_examples/zookeeper_controller/exec/reconciler.rs
@@ -24,14 +24,14 @@ pub struct ZookeeperReconcileState {
     // reconcile_step, like a program counter, is used to track the progress of reconcile_core
     // since reconcile_core is frequently "trapped" into the controller_runtime spec.
     pub reconcile_step: ZookeeperReconcileStep,
-    pub old_sts: Option<StatefulSet>,
+    pub sts_from_get: Option<StatefulSet>,
 }
 
 impl ZookeeperReconcileState {
     pub open spec fn to_view(&self) -> zk_spec::ZookeeperReconcileState {
         zk_spec::ZookeeperReconcileState {
             reconcile_step: self.reconcile_step,
-            old_sts: match &self.old_sts {
+            sts_from_get: match &self.sts_from_get {
                 Some(sts) => Option::Some(sts@),
                 None => Option::None,
             },
@@ -73,7 +73,7 @@ pub fn reconcile_init_state() -> (state: ZookeeperReconcileState)
 {
     ZookeeperReconcileState {
         reconcile_step: ZookeeperReconcileStep::Init,
-        old_sts: Option::None,
+        sts_from_get: Option::None,
     }
 }
 
@@ -186,7 +186,7 @@ pub fn reconcile_core(
                     if found_stateful_set.is_ok(){
                         let state_prime = ZookeeperReconcileState {
                             reconcile_step: ZookeeperReconcileStep::AfterUpdateZKNode,
-                            old_sts: Some(found_stateful_set.unwrap()),
+                            sts_from_get: Some(found_stateful_set.unwrap()),
                             ..state
                         };
                         let path = cluster_size_zk_node_path(zk);
@@ -252,8 +252,8 @@ pub fn reconcile_core(
             // update sts
             if resp_o.is_some() && resp_o.as_ref().unwrap().is_external_response()
             && resp_o.as_ref().unwrap().as_external_response_ref().is_reconcile_zk_node()
-            && state.old_sts.is_some() {
-                let found_stateful_set = state.old_sts;
+            && state.sts_from_get.is_some() {
+                let found_stateful_set = state.sts_from_get;
                 let mut new_stateful_set = found_stateful_set.unwrap();
                 let stateful_set = make_stateful_set(zk);
                 new_stateful_set.set_spec(stateful_set.spec().unwrap());
@@ -265,7 +265,7 @@ pub fn reconcile_core(
                 });
                 let state_prime = ZookeeperReconcileState {
                     reconcile_step: ZookeeperReconcileStep::AfterUpdateStatefulSet,
-                    old_sts: Option::None
+                    sts_from_get: Option::None
                 };
                 return (state_prime, Option::Some(Request::KRequest(req_o)));
             } else {
diff --git a/src/controller_examples/zookeeper_controller/exec/zookeeper_lib/helper_funcs.rs b/src/controller_examples/zookeeper_controller/exec/zookeeper_lib/helper_funcs.rs
index e342bafe7..828ba2db1 100644
--- a/src/controller_examples/zookeeper_controller/exec/zookeeper_lib/helper_funcs.rs
+++ b/src/controller_examples/zookeeper_controller/exec/zookeeper_lib/helper_funcs.rs
@@ -38,8 +38,7 @@ pub fn reconcile_zk_node(path: String, uri: String, replicas: String) -> ZKNodeR
     match path_look_up {
         Some(_) => {
             // Update the cluster size
-            if zk_client
-                .set_data(
+            if zk_client.set_data(
                     path.as_rust_string_ref(),
                     new_strlit("CLUSTER_SIZE=").to_string().concat(replicas.as_str())
                     .as_str()
@@ -47,15 +46,15 @@ pub fn reconcile_zk_node(path: String, uri: String, replicas: String) -> ZKNodeR
                     .as_bytes()
                     .to_vec(),
                     Some(-1),
-                ).is_err() {
-                    return ZKNodeResult{ res: Err(Error::ClusterSizeZKNodeUpdateFailed)};
-                }
-            return ZKNodeResult{ res: Ok(())};
+                )
+            .is_err() {
+                return ZKNodeResult{ res: Err(Error::ClusterSizeZKNodeUpdateFailed) };
+            }
+            return ZKNodeResult{ res: Ok(()) };
         },
         None => {
             // First create the parent node
-            if zk_client
-                .create(
+            if zk_client.create(
                     "/zookeeper-operator",
                     new_strlit("")
                         .into_rust_str()
@@ -63,11 +62,11 @@ pub fn reconcile_zk_node(path: String, uri: String, replicas: String) -> ZKNodeR
                         .to_vec(),
                     Acl::open_unsafe().clone(),
                     CreateMode::Persistent,
-                ).is_err() {
+                )
+            .is_err() {
                 return ZKNodeResult{ res: Err(Error::ClusterSizeZKNodeCreationFailed) };
             }
-            if zk_client
-                .create(
+            if zk_client.create(
                     path.as_rust_string_ref(),
                     new_strlit("CLUSTER_SIZE=").to_string().concat(replicas.as_str())
                         .as_str()
@@ -76,8 +75,9 @@ pub fn reconcile_zk_node(path: String, uri: String, replicas: String) -> ZKNodeR
                         .to_vec(),
                     Acl::open_unsafe().clone(),
                     CreateMode::Persistent,
-                ).is_err() {
-                return ZKNodeResult{ res: Err(Error::ClusterSizeZKNodeCreationFailed)};
+                )
+            .is_err() {
+                return ZKNodeResult{ res: Err(Error::ClusterSizeZKNodeCreationFailed) };
             }
             return ZKNodeResult{ res: Ok(()) };
         }
diff --git a/src/controller_examples/zookeeper_controller/spec/reconciler.rs b/src/controller_examples/zookeeper_controller/spec/reconciler.rs
index 4a66be775..75eeff480 100644
--- a/src/controller_examples/zookeeper_controller/spec/reconciler.rs
+++ b/src/controller_examples/zookeeper_controller/spec/reconciler.rs
@@ -20,7 +20,7 @@ verus! {
 
 pub struct ZookeeperReconcileState {
     pub reconcile_step: ZookeeperReconcileStep,
-    pub old_sts: Option<StatefulSetView>,
+    pub sts_from_get: Option<StatefulSetView>,
 }
 
 pub struct ZookeeperReconciler {}
@@ -56,7 +56,7 @@ impl Reconciler<ZookeeperClusterView> for ZookeeperReconciler {
 pub open spec fn reconcile_init_state() -> ZookeeperReconcileState {
     ZookeeperReconcileState {
         reconcile_step: ZookeeperReconcileStep::Init,
-        old_sts: Option::None,
+        sts_from_get: Option::None,
     }
 }
 
@@ -155,7 +155,7 @@ pub open spec fn reconcile_core(
                         let found_stateful_set = StatefulSetView::from_dynamic_object(get_sts_resp.get_Ok_0()).get_Ok_0();
                         let state_prime = ZookeeperReconcileState {
                             reconcile_step: ZookeeperReconcileStep::AfterUpdateZKNode,
-                            old_sts: Option::Some(found_stateful_set),
+                            sts_from_get: Option::Some(found_stateful_set),
                             ..state
                         };
                         let ext_req = ZKSupportInputView::ReconcileZKNode(
@@ -218,15 +218,15 @@ pub open spec fn reconcile_core(
         ZookeeperReconcileStep::AfterUpdateZKNode => {
             if resp_o.is_Some() && resp_o.get_Some_0().is_ExternalResponse()
             && resp_o.get_Some_0().get_ExternalResponse_0().is_ReconcileZKNode()
-            && state.old_sts.is_Some(){
-                let found_stateful_set = state.old_sts.get_Some_0();
+            && state.sts_from_get.is_Some(){
+                let found_stateful_set = state.sts_from_get.get_Some_0();
                 let req_o = APIRequest::UpdateRequest(UpdateRequest {
                     key: make_stateful_set_key(zk.object_ref()),
                     obj: update_stateful_set(zk, found_stateful_set).to_dynamic_object(),
                 });
                 let state_prime = ZookeeperReconcileState {
                     reconcile_step: ZookeeperReconcileStep::AfterUpdateStatefulSet,
-                    old_sts: Option::None,
+                    sts_from_get: Option::None,
                 };
                 (state_prime,  Option::Some(RequestView::KRequest(req_o)))
             } else {