diff --git a/internals/Cargo.toml b/internals/Cargo.toml
index 0b9b6c252..12a5daa1d 100644
--- a/internals/Cargo.toml
+++ b/internals/Cargo.toml
@@ -35,4 +35,4 @@ all-features = true
 rustdoc-args = ["--cfg", "docsrs"]
 
 [lints.rust]
-unexpected_cfgs = { level = "deny" }
+unexpected_cfgs = { level = "deny", check-cfg = ['cfg(kani)'] }
diff --git a/internals/src/array_vec.rs b/internals/src/array_vec.rs
index 49fca83d8..24003e14b 100644
--- a/internals/src/array_vec.rs
+++ b/internals/src/array_vec.rs
@@ -188,3 +188,45 @@ mod tests {
         av.extend_from_slice(b"abc");
     }
 }
+
+#[cfg(kani)]
+mod verification {
+    use super::*;
+
+    #[kani::unwind(16)]         // One greater than 15 (max number of elements).
+    #[kani::proof]
+    fn no_out_of_bounds_less_than_cap() {
+        const CAP: usize = 32;
+        let n = kani::any::<u32>();
+        let elements = (n & 0x0F) as usize; // Just use 4 bits.
+
+        let val = kani::any::<u32>();
+
+        let mut v = ArrayVec::<u32, CAP>::new();
+        for _ in 0..elements {
+            v.push(val);
+        }
+
+        for i in 0..elements {
+            assert_eq!(v[i], val);
+        }
+    }
+
+    #[kani::unwind(16)]         // One grater than 15.
+    #[kani::proof]
+    fn no_out_of_bounds_upto_cap() {
+        const CAP: usize = 15;
+        let elements = CAP;
+
+        let val = kani::any::<u32>();
+
+        let mut v = ArrayVec::<u32, CAP>::new();
+        for _ in 0..elements {
+            v.push(val);
+        }
+
+        for i in 0..elements {
+            assert_eq!(v[i], val);
+        }
+    }
+}
diff --git a/units/src/amount/verification.rs b/units/src/amount/verification.rs
index 0310e19e9..ae970e186 100644
--- a/units/src/amount/verification.rs
+++ b/units/src/amount/verification.rs
@@ -23,7 +23,12 @@ use super::*;
 fn u_amount_homomorphic() {
     let n1 = kani::any::<u64>();
     let n2 = kani::any::<u64>();
-    kani::assume(n1.checked_add(n2).is_some()); // assume we don't overflow in the actual test
+    // Assume we don't overflow in the actual tests.
+    kani::assume(n1.checked_add(n2).is_some()); // Adding u64s doesn't overflow.
+    let a1 = Amount::from_sat(n1);              // TODO: If from_sat enforces invariant assume this `is_ok()`.
+    let a2 = Amount::from_sat(n2);
+    kani::assume(a1.checked_add(a2).is_some()); // Adding amounts doesn't overflow.
+
     assert_eq!(Amount::from_sat(n1) + Amount::from_sat(n2), Amount::from_sat(n1 + n2));
 
     let mut amt = Amount::from_sat(n1);
@@ -37,30 +42,6 @@ fn u_amount_homomorphic() {
     let mut amt = Amount::from_sat(max);
     amt -= Amount::from_sat(min);
     assert_eq!(amt, Amount::from_sat(max - min));
-
-    assert_eq!(
-        Amount::from_sat(n1).to_signed(),
-        if n1 <= i64::MAX as u64 {
-            Ok(SignedAmount::from_sat(n1.try_into().unwrap()))
-        } else {
-            Err(OutOfRangeError::too_big(true))
-        },
-    );
-}
-
-#[kani::unwind(4)]
-#[kani::proof]
-fn u_amount_homomorphic_checked() {
-    let n1 = kani::any::<u64>();
-    let n2 = kani::any::<u64>();
-    assert_eq!(
-        Amount::from_sat(n1).checked_add(Amount::from_sat(n2)),
-        n1.checked_add(n2).map(Amount::from_sat),
-    );
-    assert_eq!(
-        Amount::from_sat(n1).checked_sub(Amount::from_sat(n2)),
-        n1.checked_sub(n2).map(Amount::from_sat),
-    );
 }
 
 #[kani::unwind(4)]
@@ -68,8 +49,14 @@ fn u_amount_homomorphic_checked() {
 fn s_amount_homomorphic() {
     let n1 = kani::any::<i64>();
     let n2 = kani::any::<i64>();
-    kani::assume(n1.checked_add(n2).is_some()); // assume we don't overflow in the actual test
-    kani::assume(n1.checked_sub(n2).is_some()); // assume we don't overflow in the actual test
+    // Assume we don't overflow in the actual tests.
+    kani::assume(n1.checked_add(n2).is_some()); // Adding i64s doesn't overflow.
+    kani::assume(n1.checked_sub(n2).is_some()); // Subbing i64s doesn't overflow.
+    let a1 = SignedAmount::from_sat(n1); // TODO: If from_sat enforces invariant assume this `is_ok()`.
+    let a2 = SignedAmount::from_sat(n2);
+    kani::assume(a1.checked_add(a2).is_some()); // Adding amounts doesn't overflow.
+    kani::assume(a1.checked_sub(a2).is_some()); // Subbing amounts doesn't overflow.
+
     assert_eq!(
         SignedAmount::from_sat(n1) + SignedAmount::from_sat(n2),
         SignedAmount::from_sat(n1 + n2)
@@ -85,33 +72,4 @@ fn s_amount_homomorphic() {
     let mut amt = SignedAmount::from_sat(n1);
     amt -= SignedAmount::from_sat(n2);
     assert_eq!(amt, SignedAmount::from_sat(n1 - n2));
-
-    assert_eq!(
-        SignedAmount::from_sat(n1).to_unsigned(),
-        if n1 >= 0 {
-            Ok(Amount::from_sat(n1.try_into().unwrap()))
-        } else {
-            Err(OutOfRangeError { is_signed: false, is_greater_than_max: false })
-        },
-    );
-}
-
-#[kani::unwind(4)]
-#[kani::proof]
-fn s_amount_homomorphic_checked() {
-    let n1 = kani::any::<i64>();
-    let n2 = kani::any::<i64>();
-    assert_eq!(
-        SignedAmount::from_sat(n1).checked_add(SignedAmount::from_sat(n2)),
-        n1.checked_add(n2).map(SignedAmount::from_sat),
-    );
-    assert_eq!(
-        SignedAmount::from_sat(n1).checked_sub(SignedAmount::from_sat(n2)),
-        n1.checked_sub(n2).map(SignedAmount::from_sat),
-    );
-
-    assert_eq!(
-        SignedAmount::from_sat(n1).positive_sub(SignedAmount::from_sat(n2)),
-        if n1 >= 0 && n2 >= 0 && n1 >= n2 { Some(SignedAmount::from_sat(n1 - n2)) } else { None },
-    );
 }