Track D: Verus deductive proofs for the wohl-alert dedup invariant

.gitignore

@@ -14,3 +14,9 @@ bazel-*
 # OS
 .DS_Store
 Thumbs.db
+
+# Verus produces a binary next to each input file when invoked as
+# `verus proofs/verus/<name>.rs` (default `--compile` behaviour).
+/alert_dedup
+/proofs/verus/alert_dedup
+

MODULE.bazel

@@ -8,6 +8,23 @@ bazel_dep(name = "rules_wasm_component", version = "0.1.0")
 bazel_dep(name = "bazel_skylib", version = "1.9.0")
 bazel_dep(name = "platforms", version = "1.0.0")
 
+# ── rules_verus (Verus SMT verification) ────────────────────────────────
+# Used by //proofs/verus for the AlertDispatcher dedup + rate-limit proofs.
+
+bazel_dep(name = "rules_verus", version = "0.1.0")
+
+git_override(
+    module_name = "rules_verus",
+    remote = "https://github.com/pulseengine/rules_verus.git",
+    commit = "fc7b63692b1d2d91511f04507b814187932cd733",
+)
+
+verus = use_extension("@rules_verus//verus:extensions.bzl", "verus")
+verus.toolchain(version = "0.2026.02.15")
+use_repo(verus, "verus_toolchains")
+
+register_toolchains("@verus_toolchains//:all")
+
 local_path_override(
     module_name = "rules_wasm_component",
     path = "../rules_wasm_component",

crates/wohl-alert/plain/src/engine.rs

@@ -6,6 +6,16 @@
 //!
 //! Wohl provides DEDUP + RATE LIMITING + CHANNEL MAPPING.
 //! Relay provides VERIFIED SUBSCRIPTION FILTERING.
+//!
+//! # Verification
+//!
+//! - Kani BMC harnesses (bounded): see [`kani_proofs`] below.
+//! - Verus deductive proofs (unbounded): see
+//!   `proofs/verus/alert_dedup.rs` at the repo root.  The Verus file mirrors
+//!   the phase 1 + phase 2 state machine of [`AlertDispatcher::process_alert`]
+//!   into a ghost model and proves the dedup invariant (Issue #7) and the
+//!   rate-limit invariant for all `u64` timestamps.  Run with
+//!   `verus proofs/verus/alert_dedup.rs`.
 
 use relay_to::engine::{SubscriptionTable, ToDecision};
 

proofs/verus/BUILD.bazel

@@ -0,0 +1,33 @@
+# Verus formal verification targets for Wohl.
+#
+# Invokes the Verus SMT-backed verifier on the AlertDispatcher dedup +
+# rate-limit proofs. Verification is separate from `cargo build` and only
+# runs under `bazel test` — `cargo build/test/clippy` and the Kani BMC
+# harnesses are unaffected.
+#
+# Usage:
+#   bazel build //proofs/verus:alert_dedup         # verify, produce stamp
+#   bazel test  //proofs/verus:alert_dedup_verify  # verify as a test
+
+load("@rules_verus//verus:defs.bzl", "verus_library", "verus_test")
+
+# ── Verified library ────────────────────────────────────────────────────
+# Runs Verus on the dedup proof module. On success, produces a stamp file
+# downstream targets can depend on as proof evidence.
+
+verus_library(
+    name = "alert_dedup",
+    srcs = ["alert_dedup.rs"],
+    crate_name = "wohl_alert_dedup",
+    visibility = ["//visibility:public"],
+)
+
+# ── Verification test ───────────────────────────────────────────────────
+# Same verification wrapped as a Bazel test so `bazel test //...` and CI
+# pick it up.
+
+verus_test(
+    name = "alert_dedup_verify",
+    srcs = ["alert_dedup.rs"],
+    crate_name = "wohl_alert_dedup",
+)

proofs/verus/README.md

@@ -0,0 +1,64 @@
+# Verus proofs for Wohl
+
+This directory holds [Verus](https://github.com/verus-lang/verus) deductive
+proofs for selected Wohl components.  Verus is an SMT-backed verifier for
+a superset of Rust; it lets us state and discharge correctness obligations
+that go beyond what Kani's bounded model checker can rule out (e.g.
+properties that quantify over all `u64` timestamps).
+
+## Current proofs
+
+| File | Component | Invariants |
+|---|---|---|
+| `alert_dedup.rs` | `wohl-alert` (`AlertDispatcher`) | dedup, rate-limit (Issue [#7](https://github.com/pulseengine/wohl/issues/7)) |
+
+## Running
+
+Verus runs via Bazel through the [rules_verus][rules_verus] ruleset — the
+toolchain is downloaded hermetically, no manual install needed:
+
+```bash
+bazel test //proofs/verus:alert_dedup_verify
+```
+
+The Verus toolchain version is pinned in `MODULE.bazel` (the `verus`
+extension). `cargo build` / `cargo test` / `cargo clippy` / Kani are
+unaffected — Verus is a separate `bazel test` gate.
+
+Expected: the test passes with `verification results:: 8 verified, 0 errors`.
+
+## Relationship to the executable code
+
+Verus and the runtime Rust are **two specifications of the same state
+machine**.  The `proofs/verus/` files mirror the relevant portion of the
+runtime data structures into Verus's `nat`/`Seq`/`Set` ghost types and
+prove the invariants on the ghost.  Each file documents the
+correspondence with the source.
+
+We chose this *separate-file* layout (rather than inline Verus annotations
+in `engine.rs`) so that:
+
+- Plain `cargo build` / `cargo test` / `cargo clippy` / Kani are unaffected.
+  Verus's macro syntax (`requires`, `ensures`, `forall`, `&&&`, ...)
+  doesn't parse under stock rustc, so inline annotations would require
+  a `verus-strip` preprocessing step that we don't have today.
+- A reviewer can read the proof file in isolation.
+
+The trade-off is that the Verus model and the runtime code can drift.
+Mitigations:
+
+1. Constants (`DEDUP_COOLDOWN_SEC`, `MAX_ALERTS_PER_MINUTE`, etc.) are
+   declared as `spec const` in the Verus file with the same values as in
+   `engine.rs`.  A drift here is immediately visible.
+2. The Kani harnesses (`crates/wohl-alert/plain/src/engine.rs::kani_proofs`)
+   already check the same properties on the *executable* code with bounded
+   inputs — they catch drift between the model and the implementation.
+
+## CI integration
+
+The `bazel test //proofs/verus:alert_dedup_verify` target above is
+CI-ready. Wiring it into `.github/workflows/ci.yml` as a job is tracked
+as a follow-up — Issue [#7](https://github.com/pulseengine/wohl/issues/7)
+stays open until that job lands.
+
+[rules_verus]: https://github.com/pulseengine/rules_verus