diff --git a/.gitignore b/.gitignore
index b27d684..102131e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,5 @@ clover_mbpp/exp_results_k_10.log
 clover_mbpp/clover_mbpp_results.json
 *.swp
 **/tmp/
+target/
+*.code-workspace
diff --git a/dataset/verus_humaneval/Cargo.lock b/dataset/verus_humaneval/Cargo.lock
new file mode 100644
index 0000000..5d6515a
--- /dev/null
+++ b/dataset/verus_humaneval/Cargo.lock
@@ -0,0 +1,7 @@
+# This file is automatically @generated by Cargo.
+# It is not intended for manual editing.
+version = 3
+
+[[package]]
+name = "verus_humaneval"
+version = "0.1.0"
diff --git a/dataset/verus_humaneval/Cargo.toml b/dataset/verus_humaneval/Cargo.toml
new file mode 100644
index 0000000..b656ffd
--- /dev/null
+++ b/dataset/verus_humaneval/Cargo.toml
@@ -0,0 +1,8 @@
+[package]
+name = "verus_humaneval"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/dataset/verus_humaneval/Notes.md b/dataset/verus_humaneval/Notes.md
new file mode 100644
index 0000000..ce011ad
--- /dev/null
+++ b/dataset/verus_humaneval/Notes.md
@@ -0,0 +1,6 @@
+# HumanEval to Verus Compatibility Notes
+
+Features that are not supported by Verus are reported here.
+
+- 0: `f32::abs` is not supported.
+- 43: iterator `enumerate` is not supported, but you can use `for` loop to achieve the same effect.
diff --git a/dataset/verus_humaneval/src/_rust_0.rs b/dataset/verus_humaneval/src/_rust_0.rs
new file mode 100644
index 0000000..b1cef57
--- /dev/null
+++ b/dataset/verus_humaneval/src/_rust_0.rs
@@ -0,0 +1,61 @@
+fn main() {}
+use vstd::{prelude::*};
+/*
+ Check if in given list of numbers, are any two numbers closer to each other than
+    given threshold.
+
+*/
+verus! {
+fn has_close_elements(numbers: Vec<f32>, threshold: f32) -> (r: bool)
+    ensures
+        r == (exists |i: int, j: int| 0 <= i < numbers.len() && 0 <= j < numbers.len() && i != j && (numbers[i] - numbers[j]).abs() < threshold)
+{
+    for i in 0..numbers.len() {
+        for j in 1..numbers.len() {
+            if i != j {
+                let distance: f32 = numbers[i] - numbers[j];
+
+                if distance.abs() < threshold {
+                    return true;
+                }
+            }
+        }
+    }
+
+    return false;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_has_close_elements() {
+        assert_eq!(
+            has_close_elements(vec![11.0, 2.0, 3.9, 4.0, 5.0, 2.2], 0.3),
+            true
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 3.9, 4.0, 5.0, 2.2], 0.05),
+            false
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 5.9, 4.0, 5.0], 0.95),
+            true
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 5.9, 4.0, 5.0], 0.8),
+            false
+        );
+        assert_eq!(
+            has_close_elements(vec![1.0, 2.0, 3.0, 4.0, 5.0, 2.0], 0.1),
+            true
+        );
+        assert_eq!(has_close_elements(vec![1.1, 2.2, 3.1, 4.1, 5.1], 1.0), true);
+        assert_eq!(
+            has_close_elements(vec![1.1, 2.2, 3.1, 4.1, 5.1], 0.5),
+            false
+        );
+    }
+}
diff --git a/dataset/verus_humaneval/src/main.rs b/dataset/verus_humaneval/src/main.rs
new file mode 100644
index 0000000..edc5c93
--- /dev/null
+++ b/dataset/verus_humaneval/src/main.rs
@@ -0,0 +1 @@
+fn main () {}
diff --git a/dataset/verus_humaneval/src/rust_3.rs b/dataset/verus_humaneval/src/rust_3.rs
new file mode 100644
index 0000000..4c0ec5b
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_3.rs
@@ -0,0 +1,77 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+    You're given a list of deposit and withdrawal operations on a bank account that starts with
+    zero balance. Your task is to detect if at any point the balance of account fallls below zero, and
+    at that point function should return True. Otherwise it should return False.
+*/
+
+
+verus! {
+// spec fn sum(v: Vec<i32>, start: int, end: int) -> (r: int)
+//     recommends 0 <= start && start <= end && end <= v.len(),
+//     decreases end - start
+// {
+//     if start == end {
+//         0
+//     } else {
+//         v[start] + sum(v, start + 1, end)
+//     }
+// }
+spec fn sum(v: Vec<i32>, start: int, len: nat) -> (r: int)
+    recommends 0 <= start && start + len <= v.len(),
+    decreases len
+{
+    if len == 0 {
+        0
+    } else {
+        sum(v, start, (len - 1) as nat) + v[start + len as int - 1]
+    }
+}
+
+fn below_zero(operations: Vec<i32>) -> (r: bool)
+    requires
+        forall|i: int| 0 <= i < operations.len() ==> -0x1fff_ffff <= #[trigger] operations[i] <= 0x1fff_ffff,
+        forall|i: int| 0 <= i <= operations.len() ==> -0x1fff_ffff <= #[trigger] sum(operations, 0, i as nat) <= 0x1fff_ffff,
+    ensures
+        r == (exists |i: int| 0 <= i <= operations.len() && #[trigger] sum(operations, 0, i as nat) < 0),
+{
+    let mut balance: i32 = 0;
+    for n in 0..operations.len()
+        invariant
+            0 <= n <= operations.len(),
+            balance == sum(operations, 0, n as nat),
+            forall|i: int| 0 <= i <= n ==> #[trigger] sum(operations, 0, i as nat) >= 0,
+            // overflow checks
+            -0x1fff_ffff <= balance <= 0x1fff_ffff,
+            forall|i: int| 0 <= i < operations.len() ==> -0x1fff_ffff <= #[trigger] operations[i] <= 0x1fff_ffff,
+            forall|i: int| 0 <= i <= operations.len() ==> -0x1fff_ffff <= #[trigger] sum(operations, 0, i as nat) <= 0x1fff_ffff,
+    {
+        let op = operations[n];
+        assert(-0x1fff_ffff <= operations[n as int] <= 0x1fff_ffff);
+        balance = balance + op;
+        assert(balance == sum(operations, 0, (n + 1) as nat));
+        assert(-0x1fff_ffff <= balance <= 0x1fff_ffff);
+        if balance < 0 {
+            return true;
+        }
+    }
+    return false;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_below_zero() {
+        assert_eq!(below_zero(vec![]), false);
+        assert_eq!(below_zero(vec![1, 2, -3, 1, 2, -3]), false);
+        assert_eq!(below_zero(vec![1, 2, -4, 5, 6]), true);
+        assert_eq!(below_zero(vec![1, -1, 2, -2, 5, -5, 4, -4]), false);
+        assert_eq!(below_zero(vec![1, -1, 2, -2, 5, -5, 4, -5]), true);
+        assert_eq!(below_zero(vec![1, -2, 2, -2, 5, -5, 4, -4]), true);
+    }
+}
diff --git a/dataset/verus_humaneval/src/rust_31.rs b/dataset/verus_humaneval/src/rust_31.rs
new file mode 100644
index 0000000..82026eb
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_31.rs
@@ -0,0 +1,66 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return true if a given number is IsPrime, and false otherwise.
+*/
+
+verus! {
+// reference: https://github.com/verus-lang/verus/blob/55b24eea93ad3dc907a4219e8b58a2f5f3f43afb/source/rust_verify/example/rw2022_script.rs#L36C1-L69C2
+
+spec fn divides(factor: nat, candidate: nat) -> bool {
+    candidate % factor == 0
+}
+
+spec fn IsPrime(candidate: nat) -> bool {
+    1 < candidate &&
+    forall|factor: nat| 1 < factor < candidate ==> !divides(factor, candidate)
+}
+
+fn is_prime(n: u32) -> (result: bool)
+    requires
+        1 < n,
+    ensures
+        result == IsPrime(n as nat),
+{
+    if n < 2 {
+        return false;
+    }
+    for k in 2..n
+        invariant
+            1 < k <= n,
+            forall|smallerfactor: nat|
+                1 < smallerfactor < k ==> !divides(smallerfactor, n as nat),
+    {
+        assert(1 < k < n);
+        if n % k == 0 {
+            assert(divides(k as nat, n as nat));
+            assert(!IsPrime(n as nat));
+            return false;
+        }
+    }
+    return true;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_is_prime() {
+        assert!(is_prime(6) == false);
+        assert!(is_prime(101) == true);
+        assert!(is_prime(11) == true);
+        assert!(is_prime(13441) == true);
+        assert!(is_prime(61) == true);
+        assert!(is_prime(4) == false);
+        assert!(is_prime(1) == false);
+        assert!(is_prime(5) == true);
+        assert!(is_prime(11) == true);
+        assert!(is_prime(17) == true);
+        assert!(is_prime(5 * 17) == false);
+        assert!(is_prime(11 * 7) == false);
+        assert!(is_prime(13441 * 19) == false);
+    }
+}
diff --git a/dataset/verus_humaneval/src/rust_35.rs b/dataset/verus_humaneval/src/rust_35.rs
new file mode 100644
index 0000000..3dc5718
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_35.rs
@@ -0,0 +1,39 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return maximum element in the list.
+*/
+
+verus! {
+fn maximum(nmbs: Vec<i32>) -> (r: i32)
+    requires
+        nmbs.len() > 0,
+    ensures
+        forall|i: int| 0 <= i < nmbs.len() ==> nmbs[i] <= r,
+        exists|i: int| 0 <= i < nmbs.len() && r == nmbs[i],
+{
+    let mut max = nmbs[0];
+    for i in 1..nmbs.len()
+        invariant
+            forall|j: int| 0 <= j < i ==> nmbs[j] <= max,
+            exists|j: int| 0 <= j < i && max == nmbs[j],
+    {
+        if nmbs[i] > max {
+            max = nmbs[i];
+        }
+    }
+    max
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_maximum() {
+        assert!(maximum(vec![1, 2, 3]) == 3);
+        assert!(maximum(vec![5, 3, -5, 2, -3, 3, 9, 0, 124, 1, -10]) == 124);
+    }
+}
diff --git a/dataset/verus_humaneval/src/rust_43.rs b/dataset/verus_humaneval/src/rust_43.rs
new file mode 100644
index 0000000..7f78af9
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_43.rs
@@ -0,0 +1,59 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+    pairs_sum_to_zero takes a list of integers as an input.
+    it returns True if there are two distinct elements in the list that
+    sum to zero, and False otherwise.
+*/
+
+verus! {
+fn pairs_sum_to_zero(l: Vec<i32>) -> (r: bool)
+    requires
+        forall|i: int| 0 <= i < l.len() ==> -0x1000_0000 <= #[trigger] l[i] <= 0x1000_0000,
+    ensures
+        r == (exists |i: int, j: int| 0 <= i < j < l.len() && l[i as int] + l[j as int] == 0)
+{
+    for i in 0..l.len()
+        invariant
+            0 <= i <= l.len(),
+            forall|i_: int, j_: int| 0 <= i_ < i && i_ < j_ < l.len() ==> l[i_ as int] + l[j_ as int] != 0,
+            // overflow check
+            forall|i: int| 0 <= i < l.len() ==> -0x1000_0000 <= #[trigger] l[i] <= 0x1000_0000,
+    {
+        for j in i + 1..l.len()
+            invariant
+                i < j <= l.len(),
+                forall|j_: int| i < j_ < j ==> l[i as int] + l[j_ as int] != 0,
+                // overflow check
+                forall|i: int| 0 <= i < l.len() ==> -0x1000_0000 <= #[trigger] l[i] <= 0x1000_0000,
+        {
+            assert(-0x1000_0000 <= l[i as int] <= 0x1000_0000);
+            assert(-0x1000_0000 <= l[j as int] <= 0x1000_0000);
+            if l[i] + l[j] == 0 {
+                return true;
+            }
+        }
+    }
+
+    return false;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_pairs_sum_to_zero() {
+        assert!(pairs_sum_to_zero(vec![1, 3, 5, 0]) == false);
+        assert!(pairs_sum_to_zero(vec![1, 3, -2, 1]) == false);
+        assert!(pairs_sum_to_zero(vec![1, 2, 3, 7]) == false);
+        assert!(pairs_sum_to_zero(vec![2, 4, -5, 3, 5, 7]) == true);
+        assert!(pairs_sum_to_zero(vec![1]) == false);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 3, 2, 30]) == true);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 3, 2, 31]) == true);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 4, 2, 30]) == false);
+        assert!(pairs_sum_to_zero(vec![-3, 9, -1, 4, 2, 31]) == false);
+    }
+}
diff --git a/dataset/verus_humaneval/src/rust_49.rs b/dataset/verus_humaneval/src/rust_49.rs
new file mode 100644
index 0000000..628e7a4
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_49.rs
@@ -0,0 +1,54 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return 2^n modulo p (be aware of numerics).
+*/
+
+verus! {
+spec fn Modp(n: nat, p: nat) -> nat
+    decreases n
+{
+    if n == 0 {
+        1
+    } else {
+        (Modp((n - 1) as nat, p) * 2) % p
+    }
+}
+
+fn modp(n: u32, p: u32) -> (result: u32)
+    requires
+        p > 0,
+        p <= 0x1000_0000,
+    ensures
+        result == Modp(n as nat, p as nat),
+{
+    let mut res = 1;
+    let mut i = 0;
+    while i < n
+        invariant
+            i <= n, 0 < p <= 0x1000_0000, res <= 0x1000_0000,
+            res == Modp(i as nat, p as nat),
+    {
+        res = (res * 2) % p;
+        i = i + 1;
+    }
+    res
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_modp() {
+        assert!(modp(3, 5) == 3);
+        assert!(modp(1101, 101) == 2);
+        assert!(modp(0, 101) == 1);
+        assert!(modp(3, 11) == 8);
+        assert!(modp(100, 101) == 1);
+        assert!(modp(30, 5) == 4);
+        assert!(modp(31, 5) == 3);
+    }
+}
diff --git a/dataset/verus_humaneval/src/rust_52.rs b/dataset/verus_humaneval/src/rust_52.rs
new file mode 100644
index 0000000..ba05349
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_52.rs
@@ -0,0 +1,39 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return True if all numbers in the list l are below threshold t.
+*/
+
+verus! {
+fn below_threshold(l: Vec<i32>, t: i32) -> (r: bool)
+    ensures
+        r == (forall|i: int| 0 <= i < l.len() ==> l[i] < t),
+{
+    for i in 0..l.len()
+        invariant
+            0 <= i <= l.len(),
+            forall|i_: int| 0 <= i_ < i ==> l[i_] < t
+    {
+        if l[i] >= t {
+            return false;
+        }
+    }
+    return true;
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_below_threshold() {
+        assert!(below_threshold(vec![1, 2, 4, 10], 100));
+        assert!(!below_threshold(vec![1, 20, 4, 10], 5));
+        assert!(below_threshold(vec![1, 20, 4, 10], 21));
+        assert!(below_threshold(vec![1, 20, 4, 10], 22));
+        assert!(below_threshold(vec![1, 8, 4, 10], 11));
+        assert!(!below_threshold(vec![1, 8, 4, 10], 10));
+    }
+}
diff --git a/dataset/verus_humaneval/src/rust_55.rs b/dataset/verus_humaneval/src/rust_55.rs
new file mode 100644
index 0000000..88a2511
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_55.rs
@@ -0,0 +1,75 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return n-th Fibonacci number.
+*/
+
+verus! {
+spec fn Fibo(n: nat) -> nat
+    decreases n
+{
+    if n == 0 {
+        0
+    } else if n == 1 {
+        1
+    } else {
+        Fibo((n - 1) as nat) + Fibo((n - 2) as nat)
+    }
+}
+
+
+proof fn lemma_fibo_is_monotonic(i: nat, j: nat)
+    requires
+        i <= j,
+    ensures
+        Fibo(i) <= Fibo(j),
+    decreases j - i
+{
+   if i < 2 && j < 2 {
+   } else if i == j {
+   } else if i == j - 1 {
+       reveal_with_fuel(Fibo, 2);
+       lemma_fibo_is_monotonic(i, (j - 1) as nat);
+   } else {
+       lemma_fibo_is_monotonic(i, (j - 1) as nat);
+       lemma_fibo_is_monotonic(i, (j - 2) as nat);
+   }
+}
+
+fn fib(n: i32) -> (result: i32)
+    requires
+        n >= 0,
+        Fibo(n as nat) <= 0x1000_0000,
+    ensures
+        result == Fibo(n as nat) as i32,
+{
+    if n == 0 {
+        return 0;
+    }
+    if n == 1 {
+        return 1;
+    }
+    assert(Fibo((n - 1) as nat) <= 0x1000_0000) by {
+        lemma_fibo_is_monotonic((n - 1) as nat, n as nat);
+    }
+    assert(Fibo((n - 2) as nat) <= 0x1000_0000) by {
+        lemma_fibo_is_monotonic((n - 2) as nat, (n - 1) as nat);
+    }
+    return fib(n - 1) + fib(n - 2);
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_fib() {
+        assert!(fib(10) == 55);
+        assert!(fib(1) == 1);
+        assert!(fib(8) == 21);
+        assert!(fib(11) == 89);
+        assert!(fib(12) == 144);
+    }
+}
diff --git a/dataset/verus_humaneval/src/rust_55_variant1.rs b/dataset/verus_humaneval/src/rust_55_variant1.rs
new file mode 100644
index 0000000..73e4e24
--- /dev/null
+++ b/dataset/verus_humaneval/src/rust_55_variant1.rs
@@ -0,0 +1,78 @@
+use vstd::prelude::*;
+fn main() {}
+
+/*
+Return n-th Fibonacci number.
+*/
+
+verus! {
+// reference: https://github.com/verus-lang/verus/blob/55b24eea93ad3dc907a4219e8b58a2f5f3f43afb/source/rust_verify/example/nevd_script.rs#L61C1-L115C2
+
+spec fn fibo(n: nat) -> nat
+    decreases n
+{
+    if n == 0 { 0 } else if n == 1 { 1 }
+    else { fibo((n - 2) as nat) + fibo((n - 1) as nat) }
+}
+
+proof fn lemma_fibo_is_monotonic(i: nat, j: nat)
+    requires i <= j,
+    ensures fibo(i) <= fibo(j),
+    decreases j - i
+{
+    if i < 2 && j < 2 {
+    } else if i == j {
+    } else if i == j - 1 {
+        reveal_with_fuel(fibo, 2);
+        lemma_fibo_is_monotonic(i, (j - 1) as nat);
+    } else {
+        lemma_fibo_is_monotonic(i, (j - 1) as nat);
+        lemma_fibo_is_monotonic(i, (j - 2) as nat);
+    }
+}
+
+spec fn fibo_fits_u64(n: nat) -> bool {
+    fibo(n) <= 0xffff_ffff_ffff_ffff
+}
+
+exec fn fib(n: u64) -> (result: u64)
+    requires fibo_fits_u64(n as nat),
+    ensures result == fibo(n as nat),
+{
+    if n == 0 {
+        return 0;
+    }
+    let mut prev: u64 = 0;
+    let mut cur: u64 = 1;
+    let mut i: u64 = 1;
+    while i < n
+        invariant
+            0 < i <= n,
+            fibo_fits_u64(n as nat),
+            fibo_fits_u64(i as nat),
+            cur == fibo(i as nat),
+            prev == fibo((i - 1) as nat),
+    {
+        i = i + 1;
+        proof { lemma_fibo_is_monotonic(i as nat, n as nat); }
+        let new_cur = cur + prev;
+        prev = cur;
+        cur = new_cur;
+    }
+    cur
+}
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_fib() {
+        assert!(fib(10) == 55);
+        assert!(fib(1) == 1);
+        assert!(fib(8) == 21);
+        assert!(fib(11) == 89);
+        assert!(fib(12) == 144);
+    }
+}