diff --git a/quic/s2n-quic-core/src/ct.rs b/quic/s2n-quic-core/src/ct.rs
index 84c7d4793e..cc54eb2bff 100644
--- a/quic/s2n-quic-core/src/ct.rs
+++ b/quic/s2n-quic-core/src/ct.rs
@@ -346,6 +346,7 @@ mod tests {
     macro_rules! binop_test {
         ($op:ident, $checked_op:ident) => {
             #[test]
+            #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(kissat))]
             fn $op() {
                 check!()
                     .with_type::<(u8, u8)>()
@@ -371,6 +372,7 @@ mod tests {
     macro_rules! cmp_test {
         ($op:ident, $core_op:ident) => {
             #[test]
+            #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(kissat))]
             fn $op() {
                 check!()
                     .with_type::<(u8, u8)>()
diff --git a/quic/s2n-quic-core/src/inet/ipv4.rs b/quic/s2n-quic-core/src/inet/ipv4.rs
index ed8266d592..2fb76d26bf 100644
--- a/quic/s2n-quic-core/src/inet/ipv4.rs
+++ b/quic/s2n-quic-core/src/inet/ipv4.rs
@@ -740,6 +740,7 @@ mod tests {
 
     /// Asserts the Scope returned matches a known implementation
     #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(kissat))]
     fn scope_test() {
         let g = gen::<[u8; 4]>().map_gen(IpV4Address::from);
         check!().with_generator(g).cloned().for_each(|subject| {
@@ -808,6 +809,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(5), kani::solver(kissat))]
     fn header_getter_setter_test() {
         check!().with_type::<Header>().for_each(|expected| {
             let mut buffer = [255u8; core::mem::size_of::<Header>()];
diff --git a/quic/s2n-quic-core/src/inet/ipv6.rs b/quic/s2n-quic-core/src/inet/ipv6.rs
index cdf9a2fc0d..d8a0447311 100644
--- a/quic/s2n-quic-core/src/inet/ipv6.rs
+++ b/quic/s2n-quic-core/src/inet/ipv6.rs
@@ -667,6 +667,7 @@ mod tests {
 
     /// Asserts the UnicastScope returned matches a known implementation
     #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(2), kani::solver(kissat))]
     fn scope_test() {
         let g = gen::<[u8; 16]>().map_gen(IpV6Address::from);
         check!().with_generator(g).cloned().for_each(|subject| {
@@ -732,6 +733,7 @@ mod tests {
     }
 
     #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(17), kani::solver(kissat))]
     fn header_getter_setter_test() {
         check!().with_type::<Header>().for_each(|expected| {
             let mut buffer = [255u8; core::mem::size_of::<Header>()];
diff --git a/quic/s2n-quic-core/src/recovery/rtt_estimator.rs b/quic/s2n-quic-core/src/recovery/rtt_estimator.rs
index bb4a64f695..30376d262f 100644
--- a/quic/s2n-quic-core/src/recovery/rtt_estimator.rs
+++ b/quic/s2n-quic-core/src/recovery/rtt_estimator.rs
@@ -719,6 +719,7 @@ mod test {
     }
 
     #[test]
+    #[cfg_attr(kani, kani::proof, kani::unwind(3), kani::solver(kissat))]
     #[cfg_attr(miri, ignore)] // This test is too expensive for miri to complete in a reasonable amount of time
     fn weighted_average_test() {
         bolero::check!()