diff --git a/.github/workflows/regression-testing.yml b/.github/workflows/regression-testing.yml
index bb9183c5b..f3058fdcf 100644
--- a/.github/workflows/regression-testing.yml
+++ b/.github/workflows/regression-testing.yml
@@ -35,3 +35,5 @@ jobs:
         run: VERUS_DIR=$PWD/verus ./build.sh zookeeper_controller.rs --rlimit 30 --time
       - name: Build rabbitmq controller
         run: VERUS_DIR=$PWD/verus ./build.sh rabbitmq_controller.rs --rlimit 30 --time
+      - name: Build fluent controller
+        run: VERUS_DIR=$PWD/verus ./build.sh fluent_controller.rs --rlimit 30 --time
diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs
index 2c1a5b100..e2b656ac6 100644
--- a/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs
@@ -7,9 +7,10 @@ use crate::fluent_controller::fluentbit::exec::types::*;
 use crate::fluent_controller::fluentbit::spec::reconciler as fluent_spec;
 use crate::kubernetes_api_objects::resource::ResourceWrapper;
 use crate::kubernetes_api_objects::{
-    api_method::*, common::*, config_map::*, daemon_set::*, label_selector::*, object_meta::*,
-    owner_reference::*, persistent_volume_claim::*, pod::*, pod_template_spec::*, resource::*,
-    resource_requirements::*, role::*, role_binding::*, secret::*, service::*, service_account::*,
+    api_method::*, common::*, config_map::*, container::*, daemon_set::*, label_selector::*,
+    object_meta::*, owner_reference::*, persistent_volume_claim::*, pod::*, pod_template_spec::*,
+    resource::*, resource_requirements::*, role::*, role_binding::*, secret::*, service::*,
+    service_account::*, volume::*,
 };
 use crate::pervasive_ext::string_map::StringMap;
 use crate::pervasive_ext::string_view::*;
diff --git a/src/controller_examples/fluent_controller/fluentbit/spec/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit/spec/reconciler.rs
index 537908972..964f61f6a 100644
--- a/src/controller_examples/fluent_controller/fluentbit/spec/reconciler.rs
+++ b/src/controller_examples/fluent_controller/fluentbit/spec/reconciler.rs
@@ -5,9 +5,9 @@ use crate::external_api::spec::*;
 use crate::fluent_controller::fluentbit::common::*;
 use crate::fluent_controller::fluentbit::spec::types::*;
 use crate::kubernetes_api_objects::{
-    api_method::*, common::*, config_map::*, daemon_set::*, label_selector::*, object_meta::*,
-    persistent_volume_claim::*, pod::*, pod_template_spec::*, resource::*, role::*,
-    role_binding::*, secret::*, service::*, service_account::*,
+    api_method::*, common::*, config_map::*, container::*, daemon_set::*, label_selector::*,
+    object_meta::*, persistent_volume_claim::*, pod::*, pod_template_spec::*, resource::*, role::*,
+    role_binding::*, secret::*, service::*, service_account::*, volume::*,
 };
 use crate::kubernetes_cluster::spec::message::*;
 use crate::pervasive_ext::string_view::*;
diff --git a/src/controller_examples/fluent_controller/fluentbit_config/spec/types.rs b/src/controller_examples/fluent_controller/fluentbit_config/spec/types.rs
index ad51721c2..16dba2810 100644
--- a/src/controller_examples/fluent_controller/fluentbit_config/spec/types.rs
+++ b/src/controller_examples/fluent_controller/fluentbit_config/spec/types.rs
@@ -92,6 +92,8 @@ impl ResourceView for FluentBitConfigView {
     #[verifier(external_body)]
     proof fn spec_integrity_is_preserved_by_marshal() {}
 
+    proof fn from_dynamic_object_result_determined_by_unmarshal() {}
+
     open spec fn rule(obj: FluentBitConfigView) -> bool {
         true
     }