diff --git a/.gitignore b/.gitignore
index b5885de..5ef4022 100644
--- a/.gitignore
+++ b/.gitignore
@@ -48,3 +48,6 @@ bindings/ruby/bin/
 bindings/java/.classpath
 bindings/java/.project
 bindings/java/.settings/
+
+# Emacs temporary files
+*~
diff --git a/Cargo.lock b/Cargo.lock
index 9eb995c..a6aa618 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -545,6 +545,12 @@ dependencies = [
  "zerocopy",
 ]
 
+[[package]]
+name = "hashbrown"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
+
 [[package]]
 name = "hashbrown"
 version = "0.14.5"
@@ -695,6 +701,16 @@ dependencies = [
  "icu_properties",
 ]
 
+[[package]]
+name = "indexmap"
+version = "1.9.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bd070e393353796e801d209ad339e89596eb4c8d430d18ede6a1cced8fafbd99"
+dependencies = [
+ "autocfg",
+ "hashbrown 0.12.3",
+]
+
 [[package]]
 name = "indexmap"
 version = "2.13.0"
@@ -1239,7 +1255,7 @@ dependencies = [
  "dashmap",
  "data-encoding",
  "globset",
- "indexmap",
+ "indexmap 2.13.0",
  "ipnet",
  "jsonschema",
  "lazy_static",
@@ -1260,6 +1276,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
  "walkdir",
 ]
 
@@ -1359,7 +1376,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.13.0",
  "itoa",
  "ryu",
  "serde",
@@ -1505,7 +1522,7 @@ version = "0.22.27"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "41fe8c660ae4257887cf66394862d21dbca4a6ddd26f04a3560410406a2f819a"
 dependencies = [
- "indexmap",
+ "indexmap 2.13.0",
  "toml_datetime",
  "toml_write",
  "winnow",
@@ -1594,12 +1611,64 @@ version = "0.9.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
+[[package]]
+name = "verus_builtin"
+version = "0.0.0-2026-02-24-1505"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-02-24-1505"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "syn 2.0.114",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-02-24-1505"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-02-24-1505"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-02-24-1505"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.44",
+ "unicode-ident",
+]
+
 [[package]]
 name = "vsimd"
 version = "0.8.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5c3082ca00d5a5ef149bb8b555a72ae84c9c59f7250f013ac822ac2e49b19c64"
 
+[[package]]
+name = "vstd"
+version = "0.0.0-2026-02-24-1505"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "walkdir"
 version = "2.5.0"
diff --git a/Cargo.toml b/Cargo.toml
index 934b95c..57f0b52 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -136,7 +136,7 @@ indexmap = { version = "2.12.1", default-features = false, features = ["serde"],
 bincode = { version = "2.0.1", default-features = false, features = ["alloc", "serde"], optional = true }
 
 # Use Verus for verification
-vstd = "0.0.0-2026-01-25-0057"
+vstd = { path = "../verus/source/vstd" }
 
 [dev-dependencies]
 anyhow = "1.0.45"
diff --git a/src/builtins/utils.rs b/src/builtins/utils.rs
index 65de2c9..51ef866 100644
--- a/src/builtins/utils.rs
+++ b/src/builtins/utils.rs
@@ -13,6 +13,8 @@ use alloc::collections::{BTreeMap, BTreeSet};
 
 use anyhow::{bail, Result};
 
+use vstd::prelude::*;
+
 #[inline]
 pub fn enforce_limit() -> Result<()> {
     crate::utils::limits::check_memory_limit_if_needed().map_err(anyhow::Error::new)
diff --git a/src/lib.rs b/src/lib.rs
index fd3cd43..4746692 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -3,7 +3,7 @@
 
 // Unsafe code should not be used.
 // Hard to reason about correctness, and maintainability.
-#![forbid(unsafe_code)]
+#![cfg_attr(not(verus_keep_ghost), forbid(unsafe_code))]
 // Ensure that all lint names are valid.
 #![deny(unknown_lints)]
 // Fail-fast lints: correctness, safety, and API surface
@@ -125,6 +125,7 @@ mod compiler;
 mod engine;
 mod indexchecker;
 mod interpreter;
+mod verusspec;
 
 pub mod languages {
     #[cfg(feature = "azure-rbac")]
diff --git a/src/number.rs b/src/number.rs
index 35e5b3b..15846bb 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -27,12 +27,21 @@ use num_traits::{One, Signed, ToPrimitive, Zero};
 use serde::ser::Serializer;
 use serde::Serialize;
 
+use vstd::prelude::*;
+use vstd::std_specs::convert::*;
+
 use crate::*;
+use crate::verusspec::bigint::*;
+use crate::verusspec::float::*;
+use crate::verusspec::utils::*;
+
+verus! {
 
 pub type BigInt = NumBigInt;
 
 const F64_SAFE_INTEGER: f64 = 9_007_199_254_740_992.0; // 2^53
 
+#[verifier::external_derive]
 #[derive(Clone)]
 pub enum Number {
     UInt(u64),
@@ -41,6 +50,31 @@ pub enum Number {
     BigInt(Rc<BigInt>),
 }
 
+pub assume_specification[ <Number as Clone>::clone ](n: &Number) -> (res: Number)
+    ensures
+        res == n,
+;
+
+pub enum NumberView {
+    Integer(int),
+    Float(f64),
+}
+
+impl View for Number
+{
+    type V = NumberView;
+
+    open spec fn view(&self) -> NumberView
+    {
+        match self {
+            Number::UInt(n) => NumberView::Integer(n as int),
+            Number::Int(n) => NumberView::Integer(n as int),
+            Number::Float(f) => NumberView::Float(*f),
+            Number::BigInt(b) => NumberView::Integer(b@),
+        }
+    }
+}
+
 impl Number {
     fn from_bigint_owned(value: BigInt) -> Self {
         if value.is_zero() {
@@ -74,7 +108,10 @@ impl Number {
         }
     }
 
-    fn to_bigint_owned(&self) -> Option<BigInt> {
+    fn to_bigint_owned(&self) -> (res: Option<BigInt>)
+        ensures
+            self@ matches NumberView::Integer(n) ==> res matches Some(b) && b@ == n,
+    {
         match self {
             Number::UInt(v) => Some(BigInt::from(*v)),
             Number::Int(v) => Some(BigInt::from(*v)),
@@ -93,13 +130,13 @@ impl Number {
         }
 
         if value >= 0.0 {
-            let u = value as u64;
-            if (u as f64) == value {
+            let u = f64_as_u64(value);
+            if u64_as_f64(u) == value {
                 return Some(BigInt::from(u));
             }
         } else {
-            let i = value as i64;
-            if (i as f64) == value {
+            let i = f64_as_i64(value);
+            if i64_as_f64(i) == value {
                 return Some(BigInt::from(i));
             }
         }
@@ -116,16 +153,16 @@ impl Number {
 
     fn to_f64_lossy(&self) -> f64 {
         match self {
-            Number::UInt(v) => *v as f64,
-            Number::Int(v) => *v as f64,
+            Number::UInt(v) => u64_as_f64(*v),
+            Number::Int(v) => i64_as_f64(*v),
             Number::Float(v) => *v,
             Number::BigInt(v) => {
                 if let Some(f) = v.to_f64() {
                     f
                 } else if v.is_negative() {
-                    f64::NEG_INFINITY
+                    f64_neg_infinity()
                 } else {
-                    f64::INFINITY
+                    f64_infinity()
                 }
             }
         }
@@ -140,13 +177,17 @@ impl Number {
         }
     }
 
-    fn ints_to_bigint(a: &Number, b: &Number) -> (BigInt, BigInt) {
+    fn ints_to_bigint(a: &Number, b: &Number) -> (res: (BigInt, BigInt))
+        requires
+            a@ is Integer,
+            b@ is Integer,
+    {
         (a.to_bigint_owned().unwrap(), b.to_bigint_owned().unwrap())
     }
 
     fn normalize_float(value: f64) -> Number {
-        if let Some(int) = Self::float_to_small_bigint(value) {
-            return Self::from_bigint_owned(int);
+        if let Some(i) = Self::float_to_small_bigint(value) {
+            return Self::from_bigint_owned(i);
         }
         Number::Float(value)
     }
@@ -161,6 +202,8 @@ impl Number {
     }
 }
 
+} // end verus!
+
 impl Debug for Number {
     fn fmt(&self, f: &mut Formatter<'_>) -> core::fmt::Result {
         f.write_str(&self.format_decimal())
diff --git a/src/verusspec/bigint.rs b/src/verusspec/bigint.rs
new file mode 100644
index 0000000..11f4afa
--- /dev/null
+++ b/src/verusspec/bigint.rs
@@ -0,0 +1,665 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+#![allow(
+    clippy::arithmetic_side_effects,
+    clippy::float_cmp,
+    clippy::unwrap_used,
+    clippy::unreachable,
+    clippy::option_if_let_else,
+    clippy::unseparated_literal_suffix,
+    clippy::as_conversions,
+    clippy::unused_trait_names,
+    clippy::pattern_type_mismatch
+)]
+
+use num_bigint::BigInt;
+use vstd::prelude::*;
+
+verus! {
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExNumBigInt(num_bigint::BigInt);
+
+pub assume_specification[ <BigInt as Clone>::clone ](n: &BigInt) -> (res: BigInt)
+    ensures
+        res == n,
+;
+
+pub trait BigIntAdditionalSpecFns {
+    spec fn view(&self) -> int;
+}
+
+impl BigIntAdditionalSpecFns for BigInt {
+    uninterp spec fn view(&self) -> int;
+}
+
+// Conditions
+
+pub assume_specification[ <BigInt as num_traits::Zero>::is_zero ](x: &BigInt) -> (res: bool)
+    ensures
+        res == (x@ == 0),
+;
+
+pub assume_specification[ <BigInt as num_traits::Signed>::is_negative ](x: &BigInt) -> (res: bool)
+    ensures
+        res == (x@ < 0),
+;
+
+// From
+
+pub assume_specification[ <BigInt as core::convert::From<i64>>::from ](i: i64) -> (res: BigInt)
+    ensures
+        res@ == i,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<i128>>::from ](i: i128) -> (res: BigInt)
+    ensures
+        res@ == i,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<u64>>::from ](u: u64) -> (res: BigInt)
+    ensures
+        res@ == u,
+;
+
+pub assume_specification[ <BigInt as core::convert::From<u128>>::from ](u: u128) -> (res: BigInt)
+    ensures
+        res@ == u,
+;
+
+// ToPrimitive
+
+#[verifier::external_trait_specification]
+#[verifier::external_trait_extension(ToPrimitiveSpec via ToPrimitiveSpecImpl)]
+pub trait ExToPrimitive {
+    type ExternalTraitSpecificationFor: num_traits::ToPrimitive;
+
+    spec fn obeys_to_primitive_spec() -> bool;
+
+    spec fn spec_to_int(&self) -> Option<int>;
+
+    fn to_isize(&self) -> (res: Option<isize>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(isize::MIN <= n <= isize::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i8(&self) -> (res: Option<i8>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i8::MIN <= n <= i8::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i16(&self) -> (res: Option<i16>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i16::MIN <= n <= i16::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i32(&self) -> (res: Option<i32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i32::MIN <= n <= i32::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_i64(&self) -> (res: Option<i64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i64::MIN <= n <= i64::MAX),
+                },
+    ;
+
+    fn to_i128(&self) -> (res: Option<i128>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(i128::MIN <= n <= i128::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_usize(&self) -> (res: Option<usize>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(usize::MIN <= n <= usize::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u8(&self) -> (res: Option<u8>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u8::MIN <= n <= u8::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u16(&self) -> (res: Option<u16>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u16::MIN <= n <= u16::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u32(&self) -> (res: Option<u32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u32::MIN <= n <= u32::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    fn to_u64(&self) -> (res: Option<u64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u64::MIN <= n <= u64::MAX),
+                },
+    ;
+
+    fn to_u128(&self) -> (res: Option<u128>)
+        ensures
+            Self::obeys_to_primitive_spec() ==>
+                match (self.spec_to_int(), res) {
+                    (None, None) => true,
+                    (None, Some(_)) => false,
+                    (Some(n1), Some(n2)) => n1 == n2,
+                    (Some(n), None) => !(u128::MIN <= n <= u128::MAX),
+                },
+        default_ensures
+            true,
+    ;
+
+    spec fn spec_to_f32(&self) -> Option<f32>;
+
+    fn to_f32(&self) -> (res: Option<f32>)
+        ensures
+            Self::obeys_to_primitive_spec() ==> res == self.spec_to_f32(),
+        default_ensures
+            true,
+    ;
+
+    spec fn spec_to_f64(&self) -> Option<f64>;
+
+    fn to_f64(&self) -> (res: Option<f64>)
+        ensures
+            Self::obeys_to_primitive_spec() ==> res == self.spec_to_f64(),
+        default_ensures
+            true,
+    ;
+}
+
+impl ToPrimitiveSpecImpl for num_bigint::BigInt
+{
+    open spec fn obeys_to_primitive_spec() -> bool
+    {
+        true
+    }
+
+    open spec fn spec_to_int(&self) -> Option<int>
+    {
+        Some(self@)
+    }
+
+    uninterp spec fn spec_to_f32(&self) -> Option<f32>;
+
+    uninterp spec fn spec_to_f64(&self) -> Option<f64>;
+}
+
+// These are the methods of ToPrimitive that BigInt implements because there is no default in ToPrimitive
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_i64 ](x: &BigInt) -> (res: Option<i64>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_u64 ](x: &BigInt) -> (res: Option<u64>);
+
+// These are the methods of ToPrimitive that BigInt overrides the defaults for because they'd otherwise be wrong
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_i128 ](x: &BigInt) -> (res: Option<i128>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_u128 ](x: &BigInt) -> (res: Option<u128>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_f32 ](x: &BigInt) -> (res: Option<f32>);
+pub assume_specification[ <num_bigint::BigInt as num_traits::ToPrimitive>::to_f64 ](x: &BigInt) -> (res: Option<f64>);
+
+// Negation
+
+pub assume_specification[ <BigInt as core::ops::Neg>::neg ](x: BigInt) -> (y: BigInt)
+    ensures
+        y@ == -x@,
+;
+
+// Addition
+
+pub assume_specification[ <BigInt as core::ops::Add>::add ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ + y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&BigInt>>::add ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ + (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Add<&BigInt>>::add ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ + (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u8>>::add ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u16>>::add ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u32>>::add ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u64>>::add ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<u128>>::add ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i8>>::add ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i16>>::add ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i32>>::add ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i64>>::add ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Add<i128>>::add ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ + y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u8>>::add ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u16>>::add ](x: BigInt, y: &u16) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u32>>::add ](x: BigInt, y: &u32) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u64>>::add ](x: BigInt, y: &u64) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&u128>>::add ](x: BigInt, y: &u128) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i8>>::add ](x: BigInt, y: &i8) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i16>>::add ](x: BigInt, y: &i16) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i32>>::add ](x: BigInt, y: &i32) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i64>>::add ](x: BigInt, y: &i64) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Add<&i128>>::add ](x: BigInt, y: &i128) -> (o: BigInt)
+    ensures
+        o@ == x@ + *y,
+;
+
+// Subtraction
+
+pub assume_specification[ <BigInt as core::ops::Sub>::sub ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ - y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&BigInt>>::sub ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ - (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Sub<&BigInt>>::sub ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ - (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u8>>::sub ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u16>>::sub ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u32>>::sub ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u64>>::sub ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<u128>>::sub ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i8>>::sub ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i16>>::sub ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i32>>::sub ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i64>>::sub ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Sub<i128>>::sub ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ - y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u8>>::sub ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u16>>::sub ](x: BigInt, y: &u16) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u32>>::sub ](x: BigInt, y: &u32) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u64>>::sub ](x: BigInt, y: &u64) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&u128>>::sub ](x: BigInt, y: &u128) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i8>>::sub ](x: BigInt, y: &i8) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i16>>::sub ](x: BigInt, y: &i16) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i32>>::sub ](x: BigInt, y: &i32) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i64>>::sub ](x: BigInt, y: &i64) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Sub<&i128>>::sub ](x: BigInt, y: &i128) -> (o: BigInt)
+    ensures
+        o@ == x@ - *y,
+;
+
+// Multiplication
+
+pub assume_specification[ <BigInt as core::ops::Mul>::mul ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ * y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Mul<&BigInt>>::mul ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ * (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Mul<&BigInt>>::mul ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ * (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u8>>::mul ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u16>>::mul ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u32>>::mul ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u64>>::mul ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<u128>>::mul ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i8>>::mul ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i16>>::mul ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i32>>::mul ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i64>>::mul ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification[ <BigInt as core::ops::Mul<i128>>::mul ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ * y,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Mul<&u8>>::mul ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ * *y,
+;
+
+// Division
+
+pub assume_specification[ <BigInt as core::ops::Div>::div ](x: BigInt, y: BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ / y@,
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Div<&BigInt>>::div ](x: BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == x@ / (*y)@,
+;
+
+pub assume_specification<'a, 'b>[ <&BigInt as core::ops::Div<&BigInt>>::div ](x: &'b BigInt, y: &BigInt) -> (o: BigInt)
+    ensures
+        o@ == (*x)@ / (*y)@,
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u8>>::div ](x: BigInt, y: u8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u16>>::div ](x: BigInt, y: u16) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u32>>::div ](x: BigInt, y: u32) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u64>>::div ](x: BigInt, y: u64) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<u128>>::div ](x: BigInt, y: u128) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i8>>::div ](x: BigInt, y: i8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i16>>::div ](x: BigInt, y: i16) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i32>>::div ](x: BigInt, y: i32) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i64>>::div ](x: BigInt, y: i64) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification[ <BigInt as core::ops::Div<i128>>::div ](x: BigInt, y: i128) -> (o: BigInt)
+    ensures
+        o@ == x@ / (y as int),
+;
+
+pub assume_specification<'a>[ <BigInt as core::ops::Div<&u8>>::div ](x: BigInt, y: &u8) -> (o: BigInt)
+    ensures
+        o@ == x@ / (*y as int),
+;
+
+} // end verus!
diff --git a/src/verusspec/float.rs b/src/verusspec/float.rs
new file mode 100644
index 0000000..51f8bcb
--- /dev/null
+++ b/src/verusspec/float.rs
@@ -0,0 +1,110 @@
+// Copyright (c) Microsoft Corporation.
+// Licensed under the MIT License.
+#![allow(
+    clippy::arithmetic_side_effects,
+    clippy::float_cmp,
+    clippy::unwrap_used,
+    clippy::unreachable,
+    clippy::option_if_let_else,
+    clippy::unseparated_literal_suffix,
+    clippy::as_conversions,
+    clippy::unused_trait_names,
+    clippy::pattern_type_mismatch
+)]
+
+use vstd::prelude::*;
+
+verus! {
+
+pub uninterp spec fn spec_f64_as_u64(f: f64) -> u64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_as_u64(f: f64) -> (res: u64)
+    ensures
+        res == spec_f64_as_u64(f),
+{
+    f as u64
+}
+
+pub uninterp spec fn spec_u64_as_f64(u: u64) -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn u64_as_f64(u: u64) -> (res: f64)
+    ensures
+        res == spec_u64_as_f64(u),
+{
+    u as f64
+}
+
+pub uninterp spec fn spec_f64_as_i64(f: f64) -> i64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_as_i64(f: f64) -> (res: i64)
+    ensures
+        res == spec_f64_as_i64(f),
+{
+    f as i64
+}
+
+pub uninterp spec fn spec_i64_as_f64(u: i64) -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn i64_as_f64(i: i64) -> (res: f64)
+    ensures
+        res == spec_i64_as_f64(i),
+{
+    i as f64
+}
+
+pub uninterp spec fn spec_f64_is_finite(f: f64) -> bool;
+
+pub assume_specification [ f64::is_finite ](f: f64) -> (res: bool)
+    ensures
+        res == spec_f64_is_finite(f),
+;
+
+pub uninterp spec fn spec_f64_fract(f: f64) -> f64;
+
+pub assume_specification [ f64::fract ](f: f64) -> (res: f64)
+    requires
+        spec_f64_is_finite(f),
+    ensures
+        res == spec_f64_fract(f),
+;
+
+pub uninterp spec fn spec_f64_abs(f: f64) -> f64;
+
+pub assume_specification [ f64::abs ](f: f64) -> (res: f64)
+    requires
+        spec_f64_is_finite(f),
+    ensures
+        res == spec_f64_abs(f),
+;
+
+pub uninterp spec fn spec_f64_neg_infinity() -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_neg_infinity() -> (res: f64)
+    ensures
+        res == spec_f64_neg_infinity(),
+{
+    f64::NEG_INFINITY
+}
+
+pub uninterp spec fn spec_f64_infinity() -> f64;
+
+#[inline]
+#[verifier::external_body]
+pub fn f64_infinity() -> (res: f64)
+    ensures
+        res == spec_f64_infinity(),
+{
+    f64::INFINITY
+}
+
+} // end verus!
diff --git a/src/verusspec/mod.rs b/src/verusspec/mod.rs
new file mode 100644
index 0000000..6319b84
--- /dev/null
+++ b/src/verusspec/mod.rs
@@ -0,0 +1,3 @@
+pub(crate) mod bigint;
+pub(crate) mod float;
+pub(crate) mod utils;
diff --git a/src/verusspec/utils.rs b/src/verusspec/utils.rs
new file mode 100644
index 0000000..534318a
--- /dev/null
+++ b/src/verusspec/utils.rs
@@ -0,0 +1,60 @@
+use anyhow::{bail, Result};
+use std::format;
+use std::string::String;
+
+use vstd::prelude::*;
+
+verus! {
+
+#[verifier::external_body]
+pub fn verus_format_helper() -> String
+{
+    format!("who cares")
+}
+
+macro_rules! verus_format {
+    ( $( $tt0:tt )* ) => {
+        {
+            #[cfg(not(verus_keep_ghost))]
+            { format!($($tt0)*) }
+            #[cfg(verus_keep_ghost)]
+            { verus_format_helper() }
+        }
+    }
+}
+
+fn my_test_verus_format(fcn: &'static str, x: u32) -> String
+{
+    verus_format!("The parameters are `{fcn}` and `{x}`")
+}
+
+#[verifier::external_type_specification]
+#[verifier::external_body]
+pub struct ExAnyhowError(anyhow::Error);
+
+#[verifier::external_body]
+pub fn verus_bail_helper<T>() -> Result<T>
+{
+    bail!("who cares")
+}
+
+macro_rules! verus_bail {
+    ( $( $tt0:tt )* ) => {
+        {
+            #[cfg(not(verus_keep_ghost))]
+            { bail!($($tt0)*) }
+            #[cfg(verus_keep_ghost)]
+            { return verus_bail_helper(); }
+        }
+    }
+}
+
+fn my_test_verus_bail(fcn: &'static str, x: u32) -> Result<()>
+{
+    if x > 0 {
+        verus_bail!(format!("Invalid parameters `{fcn}` and `{x}`").as_str())
+    }
+    Ok(())
+}
+
+} // end verus!