diff --git a/.dir-locals.el b/.dir-locals.el
new file mode 100644
index 000000000..1542960e4
--- /dev/null
+++ b/.dir-locals.el
@@ -0,0 +1,12 @@
+;;; Directory Local Variables            -*- no-byte-compile: t; -*-
+;;; For more information see (info "(emacs) Directory Variables")
+
+;; Regorus is a cargo-verus project (package.metadata.verus.verify = true), so
+;; verus-mode.el runs `cargo verus verify' rather than the raw `verus' binary.
+;; The cargo-verus path ignores `package.metadata.verus.ide.extra_args' and
+;; instead reads `verus-cargo-verus-arguments'. We set it here so that Verus is
+;; invoked with the `verus' Cargo feature enabled.
+;;
+;; Everything before `--' is passed to cargo-verus; everything after `--' is
+;; forwarded to the Verus binary. The `--' is required by verus-mode.el.
+((verus-mode . ((verus-cargo-verus-arguments . ("--features" "verus" "--")))))
diff --git a/.github/workflows/verus.yml b/.github/workflows/verus.yml
new file mode 100755
index 000000000..ec7cf0e69
--- /dev/null
+++ b/.github/workflows/verus.yml
@@ -0,0 +1,80 @@
+# Copyright (c) Microsoft Corporation. All rights reserved.
+#
+name: verus
+
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+
+env:
+  CARGO_TERM_COLOR: always
+
+# This workflow only checks out code, downloads a pinned Verus release asset,
+# and runs verification. It never writes to the repository, so restrict the
+# GITHUB_TOKEN to read-only access to repository contents.
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+    - name: Setup Rust toolchain
+      uses: ./.github/actions/toolchains/rust
+      with:
+        components: ""
+    - name: Cache cargo
+      uses: Swatinem/rust-cache@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2.9.1
+      with:
+        shared-key: ${{ runner.os }}-regorus-verus
+    - name: Install Verus and run verification
+      shell: bash
+      run: |
+        set -euxo pipefail
+        asset_url=https://github.com/verus-lang/verus/releases/download/release%2F0.2026.07.12.0b42f4c/verus-0.2026.07.12.0b42f4c-x86-linux.zip
+        asset_sha256=f6f4f5d08e07d3e1ad721d775bda5ba96b9dd0c73b48fc17f2e071866fbd01c0
+        test -n "$asset_url"
+        curl -fsSL "$asset_url" -o verus.zip
+
+        # Verify the download integrity before trusting/executing its contents.
+        echo "${asset_sha256}  verus.zip" | sha256sum --check --strict
+
+        unzip -q verus.zip -d verus-dist
+
+        # Search under an absolute path so that `find` yields absolute paths;
+        # this keeps the PATH entries below valid regardless of the working
+        # directory.
+        verus_bin="$(find "$PWD/verus-dist" -type f -name verus -perm -u+x | head -n1)"
+        cargo_verus_bin="$(find "$PWD/verus-dist" -type f -name cargo-verus -perm -u+x | head -n1)"
+        version_json="$(find "$PWD/verus-dist" -type f -name version.json | head -n1)"
+        test -n "$verus_bin"
+        test -n "$cargo_verus_bin"
+        test -n "$version_json"
+
+        # Verus is built against a specific Rust toolchain and refuses to run
+        # against any other version. Read the required toolchain from the
+        # release metadata so we track it automatically instead of hardcoding.
+        required_toolchain="$(sed -n 's/.*"toolchain"[[:space:]]*:[[:space:]]*"\([^"]*\)".*/\1/p' "$version_json")"
+        test -n "$required_toolchain"
+        echo "Verus requires Rust toolchain: $required_toolchain"
+
+        # Install the exact toolchain Verus expects, including the extra
+        # components (rustc-dev, llvm-tools) that Verus links against and that
+        # are not part of the default rustup profile.
+        rustup toolchain install "$required_toolchain" \
+          --profile minimal \
+          --component rustc-dev --component llvm-tools --component rustfmt
+
+        # Force cargo/rustc to resolve to the Verus toolchain for the commands
+        # below, overriding any repository/directory toolchain override.
+        export RUSTUP_TOOLCHAIN="$required_toolchain"
+
+        # Put cargo-verus on PATH for the commands below.
+        export PATH="$(dirname "$cargo_verus_bin"):$(dirname "$verus_bin"):$PATH"
+        cargo verus --help
+        cargo fetch --locked
+        cargo verus verify --locked --features verus
diff --git a/Cargo.lock b/Cargo.lock
index c2495a003..32c6e3074 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -614,6 +614,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"
@@ -796,6 +802,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.14.0"
@@ -1381,7 +1397,7 @@ dependencies = [
  "globset",
  "hashbrown 0.17.1",
  "icu_casemap",
- "indexmap",
+ "indexmap 2.14.0",
  "ipnet",
  "jsonschema",
  "lazy_static",
@@ -1405,6 +1421,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
  "walkdir",
 ]
 
@@ -1504,7 +1521,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "itoa",
  "ryu",
  "serde",
@@ -1666,7 +1683,7 @@ version = "0.25.13+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6975367e4d2ef766d86af01ffad14b622fecc8d4357a998fbc4deb6e9bacaf9b"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "toml_datetime",
  "toml_parser",
  "toml_writer",
@@ -1768,12 +1785,76 @@ 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-05-17-0151"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.46",
+ "syn 2.0.119",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-06-14-0213"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2 1.0.106",
+ "quote 1.0.46",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
+dependencies = [
+ "proc-macro2 1.0.106",
+ "quote 1.0.46",
+ "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-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "walkdir"
 version = "2.5.0"
@@ -2087,7 +2168,7 @@ checksum = "2d04a6b5381502aa6087c94c669499eb1602eb9c5e8198e534de571f7154809b"
 dependencies = [
  "crc32fast",
  "flate2",
- "indexmap",
+ "indexmap 2.14.0",
  "memchr",
  "typed-path",
  "zopfli",
diff --git a/Cargo.toml b/Cargo.toml
index bc3757bb0..3da6dc28f 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"]
 
+# Support verification with Verus, a Rust verifier (https://github.com/verus-lang/verus)
+
+[package.metadata.verus]
+verify = true
+
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [lib]
@@ -21,6 +26,7 @@ doctest = false
 
 [features]
 default = ["full-opa", "arc", "rvm"]
+verus = ["dep:vstd"]
 
 arc = []
 ast = []
@@ -43,7 +49,7 @@ cache = ["dep:lru"]
 rvm = ["dep:postcard", "dep:indexmap"]
 semver = ["dep:semver"]
 allocator-memory-limits = ["std", "mimalloc", "mimalloc/allocator-memory-limits"]
-std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot" ]
+std = ["rand/std", "rand/std_rng", "serde_json/std", "indexmap?/std", "msvc_spectre_libs", "dep:parking_lot", "vstd?/std" ]
 time = ["dep:chrono", "dep:chrono-tz"]
 uuid = ["dep:uuid"]
 urlquery = ["dep:url"]
@@ -134,6 +140,11 @@ mimalloc = { package = "regorus-mimalloc", path = "mimalloc", version = "2.2.7",
 indexmap = { version = "2.13.1", default-features = false, features = ["serde"], optional = true }
 postcard = { version = "1.1.3", default-features = false, features = ["alloc"], optional = true }
 
+# Verus-related dependencies.
+# vstd is enabled via the `verus` feature. In no_std builds only the `alloc` feature is used;
+# the crate's `std` feature additionally enables `vstd/std` (matching vstd's default features).
+vstd = { version = "=0.0.0-2026-07-12-0122", optional = true, default-features = false, features = ["alloc"] }
+
 [dev-dependencies]
 anyhow = "1.0.102"
 cfg-if = "1.0.0"
@@ -214,3 +225,7 @@ doctest=false
 # RUSTDOCFLAGS="--cfg docsrs" cargo +nightly doc --all-features --no-deps
 all-features = true
 rustdoc-args = ["--cfg", "docsrs"]
+
+[lints.rust]
+# Allow `verus_keep_ghost` configuration flag (used by Verus)
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(verus_keep_ghost)'] }
diff --git a/bindings/csharp/Regorus.Tests/MemoryGrowthTests.cs b/bindings/csharp/Regorus.Tests/MemoryGrowthTests.cs
index e45331c1f..c3f850093 100644
--- a/bindings/csharp/Regorus.Tests/MemoryGrowthTests.cs
+++ b/bindings/csharp/Regorus.Tests/MemoryGrowthTests.cs
@@ -115,6 +115,10 @@ public void Engine_create_eval_dispose_does_not_grow_working_set()
 
                 if (i % LogEvery == 0)
                 {
+                    // Collect transient managed garbage so the working-set delta reflects
+                    // retained (leaked) memory rather than uncollected allocations. A real
+                    // native leak from a missed Dispose() would survive GC and still be caught.
+                    ForceFullGc();
                     process.Refresh();
                     var workingSet = process.WorkingSet64;
                     var managed = GC.GetTotalMemory(false);
@@ -228,6 +232,10 @@ public void Rvm_rehydrate_execute_dispose_does_not_grow_working_set()
 
                 if (i % LogEvery == 0)
                 {
+                    // Collect transient managed garbage so the working-set delta reflects
+                    // retained (leaked) memory rather than uncollected allocations. A real
+                    // native leak from a missed Dispose() would survive GC and still be caught.
+                    ForceFullGc();
                     process.Refresh();
                     var workingSet = process.WorkingSet64;
                     var managed = GC.GetTotalMemory(false);
diff --git a/bindings/ffi/Cargo.lock b/bindings/ffi/Cargo.lock
index 88d30cd16..6f9aa8391 100644
--- a/bindings/ffi/Cargo.lock
+++ b/bindings/ffi/Cargo.lock
@@ -159,7 +159,7 @@ checksum = "2ecb53484c9c167ba674026b656d8a27d7657a58e6066aa902bfb1a4aa00ae20"
 dependencies = [
  "clap",
  "heck",
- "indexmap",
+ "indexmap 2.14.0",
  "log",
  "proc-macro2",
  "quote",
@@ -472,6 +472,12 @@ dependencies = [
  "regex-syntax",
 ]
 
+[[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"
@@ -648,6 +654,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.14.0"
@@ -1107,7 +1123,7 @@ dependencies = [
  "globset",
  "hashbrown 0.17.1",
  "icu_casemap",
- "indexmap",
+ "indexmap 2.14.0",
  "ipnet",
  "jsonschema",
  "lazy_static",
@@ -1128,6 +1144,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
 ]
 
 [[package]]
@@ -1250,7 +1267,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "itoa",
  "ryu",
  "serde",
@@ -1371,7 +1388,7 @@ version = "0.9.12+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "cf92845e79fc2e2def6a5d828f0801e29a2f8acc037becc5ab08595c7d5e9863"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "serde_core",
  "serde_spanned",
  "toml_datetime",
@@ -1472,12 +1489,76 @@ 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-05-17-0151"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
+dependencies = [
+ "proc-macro2",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-06-14-0213"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2",
+ "quote",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "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-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "wasip2"
 version = "1.0.4+wasi-0.2.12"
diff --git a/bindings/java/Cargo.lock b/bindings/java/Cargo.lock
index 343827aef..170fdce54 100644
--- a/bindings/java/Cargo.lock
+++ b/bindings/java/Cargo.lock
@@ -350,6 +350,12 @@ dependencies = [
  "regex-syntax",
 ]
 
+[[package]]
+name = "hashbrown"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
+
 [[package]]
 name = "hashbrown"
 version = "0.17.1"
@@ -488,6 +494,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.14.0"
@@ -495,7 +511,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
  "equivalent",
- "hashbrown",
+ "hashbrown 0.17.1",
  "serde",
  "serde_core",
 ]
@@ -927,7 +943,7 @@ dependencies = [
  "ahash",
  "fluent-uri",
  "getrandom 0.3.4",
- "hashbrown",
+ "hashbrown 0.17.1",
  "itoa",
  "micromap",
  "parking_lot",
@@ -973,7 +989,7 @@ dependencies = [
  "chrono-tz",
  "data-encoding",
  "globset",
- "indexmap",
+ "indexmap 2.14.0",
  "ipnet",
  "jsonschema",
  "lazy_static",
@@ -994,6 +1010,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
 ]
 
 [[package]]
@@ -1111,7 +1128,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "itoa",
  "ryu",
  "serde",
@@ -1284,12 +1301,76 @@ 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-05-17-0151"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
+dependencies = [
+ "proc-macro2",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-06-14-0213"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2",
+ "quote",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "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-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "walkdir"
 version = "2.5.0"
diff --git a/bindings/python/Cargo.lock b/bindings/python/Cargo.lock
index 080e8e550..3e1c56ca9 100644
--- a/bindings/python/Cargo.lock
+++ b/bindings/python/Cargo.lock
@@ -334,6 +334,12 @@ dependencies = [
  "regex-syntax",
 ]
 
+[[package]]
+name = "hashbrown"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
+
 [[package]]
 name = "hashbrown"
 version = "0.17.1"
@@ -478,6 +484,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.14.0"
@@ -485,7 +501,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
  "equivalent",
- "hashbrown",
+ "hashbrown 0.17.1",
  "serde",
  "serde_core",
 ]
@@ -941,7 +957,7 @@ dependencies = [
  "ahash",
  "fluent-uri",
  "getrandom 0.3.4",
- "hashbrown",
+ "hashbrown 0.17.1",
  "itoa",
  "micromap",
  "parking_lot",
@@ -987,7 +1003,7 @@ dependencies = [
  "chrono-tz",
  "data-encoding",
  "globset",
- "indexmap",
+ "indexmap 2.14.0",
  "ipnet",
  "jsonschema",
  "lazy_static",
@@ -1008,6 +1024,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
 ]
 
 [[package]]
@@ -1108,7 +1125,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "itoa",
  "ryu",
  "serde",
@@ -1271,12 +1288,76 @@ 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-05-17-0151"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
+dependencies = [
+ "proc-macro2",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-06-14-0213"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2",
+ "quote",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "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-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "wasip2"
 version = "1.0.4+wasi-0.2.12"
diff --git a/bindings/ruby/Cargo.lock b/bindings/ruby/Cargo.lock
index 21c2e1e1f..919eca9d5 100644
--- a/bindings/ruby/Cargo.lock
+++ b/bindings/ruby/Cargo.lock
@@ -501,6 +501,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.14.0"
@@ -1013,7 +1023,7 @@ dependencies = [
  "chrono-tz",
  "data-encoding",
  "globset",
- "indexmap",
+ "indexmap 2.14.0",
  "ipnet",
  "jsonschema",
  "lazy_static",
@@ -1033,6 +1043,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
 ]
 
 [[package]]
@@ -1156,7 +1167,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "itoa",
  "ryu",
  "serde",
@@ -1331,12 +1342,70 @@ 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-05-17-0151"
+source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-06-14-0213"
+source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-05-31-0205"
+source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
+dependencies = [
+ "proc-macro2",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-06-14-0213"
+source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2",
+ "quote",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-05-31-0205"
+source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "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-06-14-0213"
+source = "git+https://github.com/verus-lang/verus.git#60c8383d70074f6c00d754b4fb47438995fcb79a"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "wasip2"
 version = "1.0.4+wasi-0.2.12"
diff --git a/bindings/wasm/Cargo.lock b/bindings/wasm/Cargo.lock
index 31f2a830a..0eedc774e 100644
--- a/bindings/wasm/Cargo.lock
+++ b/bindings/wasm/Cargo.lock
@@ -366,6 +366,12 @@ dependencies = [
  "regex-syntax",
 ]
 
+[[package]]
+name = "hashbrown"
+version = "0.12.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888"
+
 [[package]]
 name = "hashbrown"
 version = "0.17.1"
@@ -504,6 +510,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.14.0"
@@ -511,7 +527,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9"
 dependencies = [
  "equivalent",
- "hashbrown",
+ "hashbrown 0.17.1",
  "serde",
  "serde_core",
 ]
@@ -926,7 +942,7 @@ dependencies = [
  "ahash",
  "fluent-uri",
  "getrandom 0.3.4",
- "hashbrown",
+ "hashbrown 0.17.1",
  "itoa",
  "micromap",
  "parking_lot",
@@ -972,7 +988,7 @@ dependencies = [
  "chrono-tz",
  "data-encoding",
  "globset",
- "indexmap",
+ "indexmap 2.14.0",
  "ipnet",
  "jsonschema",
  "lazy_static",
@@ -992,6 +1008,7 @@ dependencies = [
  "thiserror",
  "url",
  "uuid",
+ "vstd",
 ]
 
 [[package]]
@@ -1103,7 +1120,7 @@ version = "0.9.34+deprecated"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6a8b1a1a2ebf674015cc02edccce75287f1a0130d394307b36743c2f5d504b47"
 dependencies = [
- "indexmap",
+ "indexmap 2.14.0",
  "itoa",
  "ryu",
  "serde",
@@ -1262,12 +1279,76 @@ 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-05-17-0151"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cab9266bfb5cf45a080f425c560b0e0be2bf81194f0e80258990c49c1829d8b9"
+
+[[package]]
+name = "verus_builtin_macros"
+version = "0.0.0-2026-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3fb60e3a141ababe618fbdb759f14aa8544f6346a98a44c1e3a7dbe20b1f2892"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+ "synstructure",
+ "verus_prettyplease",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_prettyplease"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3ffdc94c89109a67c59646f6b6e71b49de394020f45294247dd716470523245b"
+dependencies = [
+ "proc-macro2",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_state_machines_macros"
+version = "0.0.0-2026-06-14-0213"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6704a9ce586a5027f87933d9a84817411c937804090a9585c28bf335ac37eefc"
+dependencies = [
+ "indexmap 1.9.3",
+ "proc-macro2",
+ "quote",
+ "verus_syn",
+]
+
+[[package]]
+name = "verus_syn"
+version = "0.0.0-2026-05-31-0205"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "030b774330d5ec618691c2cd6fba8bbb13bd538f3884a1143450baec25749706"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "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-07-12-0122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd0a0d328e1d6382af99a65f71677cf4b9200ec24e09fcafa7b1a3af8c8f5111"
+dependencies = [
+ "verus_builtin",
+ "verus_builtin_macros",
+ "verus_state_machines_macros",
+]
+
 [[package]]
 name = "walkdir"
 version = "2.5.0"
diff --git a/src/number.rs b/src/number.rs
index 35e5b3bcf..e6d6d2e1f 100644
--- a/src/number.rs
+++ b/src/number.rs
@@ -27,10 +27,14 @@ use num_traits::{One, Signed, ToPrimitive, Zero};
 use serde::ser::Serializer;
 use serde::Serialize;
 
+#[cfg(feature = "verus")]
+use vstd::prelude::*;
+
 use crate::*;
 
 pub type BigInt = NumBigInt;
 
+#[cfg_attr(feature = "verus", verus_verify)]
 const F64_SAFE_INTEGER: f64 = 9_007_199_254_740_992.0; // 2^53
 
 #[derive(Clone)]
@@ -145,8 +149,8 @@ impl Number {
     }
 
     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)
     }
@@ -685,6 +689,7 @@ impl Number {
         }
     }
 
+    #[allow(clippy::if_then_some_else_none)]
     fn ensure_integers(a: &Number, b: &Number) -> Option<(BigInt, BigInt)> {
         if a.is_integer() && b.is_integer() {
             Some((a.to_bigint_owned()?, b.to_bigint_owned()?))
diff --git a/src/rvm/vm/comprehension.rs b/src/rvm/vm/comprehension.rs
index aafa52b3c..ba0dae110 100644
--- a/src/rvm/vm/comprehension.rs
+++ b/src/rvm/vm/comprehension.rs
@@ -226,6 +226,7 @@ impl RegoVM {
         }
     }
 
+    #[allow(clippy::if_then_some_else_none)]
     fn execute_comprehension_yield_run_to_completion(
         &mut self,
         value_reg: u8,
@@ -332,6 +333,7 @@ impl RegoVM {
         Ok(())
     }
 
+    #[allow(clippy::if_then_some_else_none)]
     fn execute_comprehension_yield_suspendable(
         &mut self,
         value_reg: u8,