Forte: A sensitivity type system for imperative Rust

What it claims

Forte is a sensitivity type system for imperative Rust whose soundness "rests on ownership": the exclusivity of a Rust &mut borrow is the single fact that licenses framing a sensitivity claim across a mutating call. This closes a structural gap the existing systems could not: pure graded calculi (Fuzz, DFuzz, Duet, Jazz, Solo) forbid mutation, and imperative sensitivity analyses (Fuzzi, LightDP, Chaudhuri et al.) allow assignment to first-order variables but no references — so neither can host the deployed differential-privacy code, which accumulates into totals, histograms and trees through mutable borrows. The target is OpenDP's trusted stability map closures, which the paper notes are largely unproven: 109 hand-written proof documents reach only 14 of the 68 trusted stability closures, and every bounded sum variant lacks one.

How it works

The core calculus is λ-Forte, a first-order store-based language with mutable locals, exclusive borrows at call sites, functions taking &mut parameters, and loops over public counters. A value carries a sensitivity environment (one non-negative coefficient per declared source); a call performs a strong update of that environment in place. The key duality: environment-indexed sensitivity is alias-tolerant for the arithmetic (a double read of one location prices as x+x = 2s), but aliasing breaks the frame — two aliased &mut borrows suffice to derive a false claim, which Rust's borrow checker rejects before the refinement checker runs.

Two tools carry the proof burden, with no compiler fork:

flowchart TD
  A[λ-Forte calculus] --> B[Verus: mechanizes metric-preservation theorem, function rule, aliased-borrow counterexample]
  A --> C[forte-rs library]
  C --> D[Flux: checks it as ordinary library, &mut ensures clauses = strong updates, infers loop invariants]
  D --> E[Correspondence theorem: transports metric preservation to accepted programs]
  B --> F[43 verified theorems/lemmas backing every deterministic primitive signature]

Flux's own soundness is unary (one run); a sensitivity claim relates two runs, so metric preservation is supplied by the correspondence theorem (§5) rather than by Flux.

Evidence

Evaluated on OpenDP mechanism kernels chosen for genuine in-place mutation. Forte turns trusted stability constants into checked obligations, covering the 54 constructors with no proof document; it rejects the real bug classes Casacuberta et al. documented — off-by-one diameters, tightened bounds, the "1-sensitivity" Lipschitz misreading of a clamp — plus under-calibrated releases and overspent budgets. The unbounded-vector type has no sum rule, making the bounded-sum bug class unrepresentable rather than merely detectable. One trusted OpenDP constant was re-derived as a Flux-inferred loop invariant. The trusted base is 43 Verus-checked theorems and lemmas. (Baseline is OpenDP's own trusted maps at commit 4198f76, Sept 2026; the paper reports matching them, not a speed/accuracy delta.)

Limits

Scope is deliberately narrow, and the author states it plainly. The arithmetic is idealized: unbounded integers, exact reals — overflow and floating-point rounding are out of scope, and the floating-point half of the failures Casacuberta et al. report is explicitly excluded. Threat model is "honest but fallible" author; no defense against a malicious author. The probabilistic release step (noise addition, budget accounting beyond affine token discipline) is outside the checked fragment. The calculus excludes borrows outliving a call, references stored in data structures, closures over sensitive data, sensitive control flow, and data-dependent write indices. Exact loop bounds depend on the environment sharing an integer sort with the counter; at least one case-study loop needed an invariant hint. This is a preprint (arXiv:2609.30254v1); the fetched text cuts off mid-§3, so the full typing/evaluation rules and complete case-study table are not visible here.