From 156772c523e51c4203009f7931bfe78c2e3fb052 Mon Sep 17 00:00:00 2001
From: Jay Lorch <jaylorch@gmail.com>
Date: Tue, 17 Feb 2026 13:25:11 -0800
Subject: [PATCH] Add Verus dependencies

---
 Cargo.toml              |  8 ++++++++
 src/builtins/numbers.rs | 12 ++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/Cargo.toml b/Cargo.toml
index 400250c..934b95c 100644
--- a/Cargo.toml
+++ b/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"
diff --git a/src/builtins/numbers.rs b/src/builtins/numbers.rs
index 9cbc8af..8e6c896 100644
--- a/src/builtins/numbers.rs
+++ b/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,
+    {
+    }
+}