diff --git a/library/alloc/src/collections/binary_heap/mod.rs b/library/alloc/src/collections/binary_heap/mod.rs
index 59f10b09c73fd..b60b8ee91823e 100644
--- a/library/alloc/src/collections/binary_heap/mod.rs
+++ b/library/alloc/src/collections/binary_heap/mod.rs
@@ -143,6 +143,11 @@
 #![allow(missing_docs)]
 #![stable(feature = "rust1", since = "1.0.0")]
 
+use safety::requires;
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+use core::kani;
+
 use core::alloc::Allocator;
 use core::iter::{FusedIterator, InPlaceIterable, SourceIter, TrustedFused, TrustedLen};
 use core::mem::{self, ManuallyDrop, swap};
@@ -675,6 +680,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < self.len()`.
+    #[requires(pos < self.len())]
+    #[cfg_attr(kani, kani::modifies(self.data.as_ptr()))]
     unsafe fn sift_up(&mut self, start: usize, pos: usize) -> usize {
         // Take out the value at `pos` and create a hole.
         // SAFETY: The caller guarantees that pos < self.len()
@@ -704,6 +711,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < end <= self.len()`.
+    #[requires(pos < end && end <= self.len())]
+    #[cfg_attr(kani, kani::modifies(self.data.as_ptr()))]
     unsafe fn sift_down_range(&mut self, pos: usize, end: usize) {
         // SAFETY: The caller guarantees that pos < end <= self.len().
         let mut hole = unsafe { Hole::new(&mut self.data, pos) };
@@ -744,6 +753,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < self.len()`.
+    #[requires(pos < self.len())]
+    #[cfg_attr(kani, kani::modifies(self.data.as_ptr()))]
     unsafe fn sift_down(&mut self, pos: usize) {
         let len = self.len();
         // SAFETY: pos < len is guaranteed by the caller and
@@ -760,6 +771,8 @@ impl<T: Ord, A: Allocator> BinaryHeap<T, A> {
     /// # Safety
     ///
     /// The caller must guarantee that `pos < self.len()`.
+    #[requires(pos < self.len())]
+    #[cfg_attr(kani, kani::modifies(self.data.as_ptr()))]
     unsafe fn sift_down_to_bottom(&mut self, mut pos: usize) {
         let end = self.len();
         let start = pos;
@@ -1901,3 +1914,59 @@ impl<'a, T: 'a + Ord + Copy, A: Allocator> Extend<&'a T> for BinaryHeap<T, A> {
         self.reserve(additional);
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    // TODO: Kani reports as failing property "Only a single top-level call", which does not
+    // obviously make sense. Requires investigation.
+    // // unsafe fn sift_up(&mut self, start: usize, pos: usize) -> usize
+    // #[kani::proof_for_contract(BinaryHeap<T, A>::sift_up)]
+    // #[kani::unwind(1)]
+    // pub fn check_sift_up() {
+    //     // TODO: this isn't exactly an arbitrary heap
+    //     let mut heap = BinaryHeap::new_in(Global);
+    //     heap.push(kani::any::<usize>());
+    //     unsafe {
+    //         let _ = heap.sift_up(kani::any(), kani::any());
+    //     }
+    // }
+
+    // unsafe fn sift_down_range(&mut self, pos: usize, end: usize)
+    #[kani::proof_for_contract(BinaryHeap<T, A>::sift_down_range)]
+    #[kani::unwind(1)]
+    pub fn check_sift_down_range() {
+        // TODO: this isn't exactly an arbitrary heap
+        let mut heap = BinaryHeap::new_in(Global);
+        heap.push(kani::any::<usize>());
+        unsafe {
+            let _ = heap.sift_down_range(kani::any(), kani::any());
+        }
+    }
+
+    // unsafe fn sift_down(&mut self, pos: usize)
+    #[kani::proof_for_contract(BinaryHeap<T, A>::sift_down)]
+    #[kani::unwind(1)]
+    pub fn check_sift_down() {
+        // TODO: this isn't exactly an arbitrary heap
+        let mut heap = BinaryHeap::new_in(Global);
+        heap.push(kani::any::<usize>());
+        unsafe {
+            let _ = heap.sift_down(kani::any());
+        }
+    }
+
+    // unsafe fn sift_down_to_bottom(&mut self, mut pos: usize)
+    #[kani::proof_for_contract(BinaryHeap<T, A>::sift_down_to_bottom)]
+    #[kani::unwind(1)]
+    pub fn check_sift_down_to_bottom() {
+        // TODO: this isn't exactly an arbitrary heap
+        let mut heap = BinaryHeap::new_in(Global);
+        heap.push(kani::any::<usize>());
+        unsafe {
+            let _ = heap.sift_down_to_bottom(kani::any());
+        }
+    }
+}