diff --git a/tools/hermes/tests/cases/success/repro_box_anyhow.rs b/tools/hermes/tests/cases/success/repro_box_anyhow.rs
new file mode 100644
index 0000000000..edc2d6a6b9
--- /dev/null
+++ b/tools/hermes/tests/cases/success/repro_box_anyhow.rs
@@ -0,0 +1,25 @@
+
+///@ lean spec foo(x : U32)
+///@ ensures |ret| ret.val = x.val
+///@ proof
+///@   simp [foo]
+pub fn foo(x: u32) -> u32 {
+    x
+}
+
+pub fn trigger_box_error(fail: bool) -> Result<(), Box<dyn std::fmt::Debug>> {
+    let e = if fail {
+        Box::new("failed")
+    } else {
+        Box::new("succeeded")
+    };
+    if fail {
+        return Err(e);
+    }
+    Ok(())
+}
+
+fn main() {
+    let _ = foo(42);
+    let _ = trigger_box_error(true);
+}
diff --git a/tools/hermes/tests/cases/success/repro_box_branch.rs b/tools/hermes/tests/cases/success/repro_box_branch.rs
new file mode 100644
index 0000000000..4d94d5be83
--- /dev/null
+++ b/tools/hermes/tests/cases/success/repro_box_branch.rs
@@ -0,0 +1,20 @@
+///@ lean spec foo(x : U32)
+///@ ensures |ret| ret.val = x.val
+///@ proof
+///@   simp [foo]
+pub fn foo(x: u32) -> u32 {
+    x
+}
+
+pub fn trigger_branch_box(cond: bool) -> Box<u32> {
+    if cond {
+        Box::new(1)
+    } else {
+        Box::new(2)
+    }
+}
+
+fn main() {
+    foo(42);
+    trigger_branch_box(true);
+}
diff --git a/tools/hermes/tests/cases/success/repro_dyn_trait.rs b/tools/hermes/tests/cases/success/repro_dyn_trait.rs
new file mode 100644
index 0000000000..2987fb1902
--- /dev/null
+++ b/tools/hermes/tests/cases/success/repro_dyn_trait.rs
@@ -0,0 +1,16 @@
+///@ lean spec foo(x : U32)
+///@ ensures |ret| ret.val = x.val
+///@ proof
+///@   simp [foo]
+pub fn foo(x: u32) -> u32 {
+    x
+}
+
+pub fn trigger_dyn_trait() {
+    let _x: Box<dyn std::fmt::Debug> = Box::new(42);
+}
+
+fn main() {
+    foo(42);
+    trigger_dyn_trait();
+}