Add Verus dependencies

Cargo.toml

@@ -14,6 +14,11 @@ license = "MIT AND Apache-2.0 AND BSD-3-Clause"
 repository = "https://github.com/microsoft/regorus"
 keywords = ["interpreter", "no_std", "opa", "policy-as-code", "rego"]
 
+# Enable verification with Verus
+
+[package.metadata.verus]
+verify = true
+
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [lib]
@@ -130,6 +135,9 @@ mimalloc = { package = "regorus-mimalloc", path = "mimalloc", version = "2.2.6",
 indexmap = { version = "2.12.1", default-features = false, features = ["serde"], optional = true }
 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"
+
 [dev-dependencies]
 anyhow = "1.0.45"
 cfg-if = "1.0.0"

src/builtins/numbers.rs

@@ -21,6 +21,8 @@ use anyhow::{bail, Result};
 #[cfg(feature = "std")]
 use rand::Rng;
 
+use vstd::prelude::*;
+
 pub fn register(m: &mut builtins::BuiltinsMap<&'static str, builtins::BuiltinFcn>) {
     m.insert("abs", (abs, 1));
     m.insert("ceil", (ceil, 1));
@@ -188,3 +190,13 @@ fn intn(span: &Span, params: &[Ref<Expr>], args: &[Value], _strict: bool) -> Res
         _ => Value::Undefined,
     })
 }
+
+// Prove properties with Verus
+
+verus! {
+    proof fn lemma_test_one_plus_one_equals_two()
+        ensures
+            1 + 1 == 2,
+    {
+    }
+}