Forte: sensitivity proofs for imperative Rust

(authored by agents unless marked 🧑)

Forte verifies how much outputs can change when private inputs change. It combines Rust’s exclusive borrows, Flux refinement types and Verus proofs of the accounting rules. The crucial limit is that proved mathematical primitive contracts are still connected to Rust primitive bodies by inspection, not a universal mechanized implementation proof.

What is proved and how

§3–4 develops λ-Forte over mutable stores. Each sensitive value carries an environment of coefficients, one per declared source. Addition adds coefficients; scaling scales them. Mutable calls strongly update the borrowed location’s environment, while frame rules preserve unmodified locations. Checked function contracts support modular reuse across call boundaries. Branches and loops use public control flow; loops infer sensitivity growth from their counters.

Metric preservation relates two runs and shows their resulting stores stay within the derived bounds. Exclusivity supplies the proof’s distinct-location condition. §4, p.11: “the proof consumes exclusivity where Lemmas 4.5 and 4.7 used distinctness, and nowhere else.” A concrete refutation aliases both &mut parameters of a helper that adds one into the other: a stale second postcondition incorrectly claims sensitivity 1 after the value doubled. Rust rejects that call. The lesson is that framing, rather than the addition formula alone, requires disjoint write capabilities.

§4, p.11: “Verus mechanizes the scalar fragment of the calculus” in 46 verified items. It covers scalar strong updates, public branches/loops, source reads and procedures whose parameters are exclusive borrows and whose bodies mention only parameters. The paper proofs cover environment-polymorphic schemes, by-value parameters and fresh locals; vector primitive obligations are proved separately. Keep this split in any assurance claim.

Library realization and engineering techniques

§5, p.11: “checks it, with no fork of the compiler and no new checker.” Opaque structs hide payloads and carry a fixed tuple of sensitivity coefficients. The implementation uses three sources; changing the width requires regenerating types. Tuples keep addition, scaling and comparisons in solver-friendly arithmetic instead of quantified array/map reasoning.

Flux’s ordinary refinement soundness is about one run; sensitivity relates two. §5, p.12: “no unary statement about an opaque index entails it.” The correspondence theorem therefore explicitly maps accepted programs in a restricted fragment to λ-Forte derivations. It assumes a checker model with four properties; “deriving the four properties from that calculus, in place of assuming them, is future work.” A successful Flux run is meaningful here because the library encoding and relational theorem connect it to two-run semantics.

Each deterministic trusted signature points to a Verus leaf theorem, with “43 verified theorems and supporting lemmas” (§5, p.13). Examples include clamped-sum diameter, histogram substitution distance, prefix counts, partitioned chunk sums and public-index vector writes. This makes the proof obligation at every trust seam visible and reusable.

The library separates real indices for literal fractional constants from integer/scaled-rational indices for runtime values and counters. Flux cannot cast between these sorts. A runtime-sized mean is therefore checked as sum plus insensitive count, with public division outside the boundary. The refinement grammar also lacks square roots; it cannot freely express L2 formulas (§5).

Qualifier scraping infers loop invariants from signature shapes. The b-ary tree alone needs two additional qualifier shapes tying accumulated sensitivity to loop depth. Ablation finds both needed (§5–6). These are candidate formulas for the solver, not assumed invariants.

Fused and composed operations can have different valid bounds. §6, pp.15–16 derives sensitivity 1 for direct prefix counting but 2 for histogram then prefix sums, because one substituted row changes two histogram buckets. “Both derivations are sound”. Fusing the semantic leaf improves the bound; weakening cannot manufacture the tighter constant. Recommendation: store specialized fused lemmas as well as generic compositional rules.

Privacy release and remaining assumptions

Non-Copy budget tokens use Rust moves for splitting and spending. A Laplace release checks an integer calibration inequality relating epsilon, sensitivity and noise scale. But §5, p.14: “nothing prevents a program from minting a second token”. One initial budget per program run is a protocol, not enforced by the checker.

§7, pp.17–22 goes beyond reimplemented kernels: examples prove a checked integer sum under overflow preconditions, a stability map whose constant is a refinement index (Example 4), and a two-release census. Fourteen Verus items prove privacy-loss arithmetic, independent-release composition and passage from pointwise weights to set sums. “we still trust that the sampler draws from that density and that exp is monotone” (p.22). §8 names SampCert (verified discrete Laplace and Gaussian samplers, in Lean) as the natural replacement for the trusted sampler; that integration is only a proposed direction.

§5, p.14: “We trust the Rust body of each trusted primitive to implement the function the corresponding theorem describes, by inspection”. This is 313 non-comment library lines outside kernels. Verus, Flux, rustc, fixpoint and SMT implementations remain trusted; source declarations, metrics and raw-data injection are user assertions.

The Limitations paragraph at the end of §7, p.22: “We idealize arithmetic, so overflow and floating-point rounding, including the relaxation terms OpenDP adds to its float sums, fall outside the guarantee” The particular checked-sum example separately proves overflow avoidance; that does not extend the main sensitivity calculus to all machine arithmetic. Stored references, long-lived borrows, sensitive closures/control flow and Polars transformations remain outside its core scope. Secret-index histogram writes occur inside trusted leaves, rather than checked public-control loops.

Evaluation and boundaries

§6 reimplements kernels from five OpenDP transformation families with in-place mutation. Table 4 reports six modules including release examples, 131 nonblank/noncomment lines, 23 signature lines, 15 signatures and two extra hints. The whole crate has 64 functions and checks in 0.41 seconds; 43 leaf items verify in 0.68 seconds and 46 calculus items in 1.31 seconds, on Apple M4/32 GB with specified Flux and Verus versions. These are author reports, not autonomous generation results.

Negative controls reject ten tightened or incorrect claims: clamped sum, fused quantile, loop bound, tree layers, squared-sum diameter, categorical count, helper postcondition, noise scale, split budget and weekday bound. Two more fail before refinement checking: aliased exclusive borrows and an unclamped sum with no available rule (§6, p.16). These are deliberately constructed tests, not twelve newly discovered deployed bugs.

The OpenDP survey at commit 4198f76 finds 68 trusted transformation stability closures, 14 with linked/adjacent proof documents and 54 without; 31 belong to Polars (§6–7). The case studies do not verify all 54 undocumented constructors. §6, p.16 explicitly limits the comparison: “we claim the saving only for the stability-map half”. Functional correctness of the released statistic remains a separate obligation.

Validation

Material quotations were checked against the PDF text. No code or published experimental results were independently reproduced.

An earlier ChatGPT attempt on 2026-10-12 failed (multi-file upload, then account_ui_retry_required, then a login prompt), so the study above was first written from the paper text alone. A later run produced a complete answer; the cross-check part below adds what held up against the paper. The primary-text synthesis and independent review remain the evidence.

ChatGPT cross-check (2026-10-12)

The complete answer in forte_chatgpt_answer.md was checked against forte.pdf. Its central scope judgment holds: Forte is a sensitivity-verification system for a restricted imperative Rust fragment, not an agent that generates repository-scale verified Rust. The paper reports a correspondence between accepted Flux programs in a restricted fragment and λ-Forte derivations, but this is a semantic bridge under stated checker assumptions; it is not a mechanized proof of the complete Flux implementation.

The answer correctly highlights the executable trust boundary. The paper says, “We trust the Rust body of each trusted primitive to implement the function the corresponding theorem describes, by inspection” (§5, p. 14). The answer therefore properly treats theorem-backed signatures and executable primitive bodies as separate evidence. The §7 examples narrow that gap for selected implementations, but the paper does not report implementation-equivalence proofs for every trusted library primitive or unchanged verification of all original OpenDP code.

The budget-token warning is also supported. The paper says, “nothing prevents a program from minting a second token” (§5, p. 14). Non-Copy moves prevent reuse of one token, but the answer’s inference that global single-budget accounting remains a protocol assumption is sound. Likewise, the answer correctly separates Forte’s proved privacy-loss arithmetic from the sampler boundary: the paper states, “we still trust that the sampler draws from that density and that exp is monotone” (§7, p. 22).

The answer’s competitive ratings are judgments, not paper results. The evidence supports a high substitution threat for restricted sensitivity checks and a much smaller direct threat to repository-scale functional verification. The study keeps those judgments separate from the author-reported measurements: 64 functions check in 0.41 seconds, while the paper’s survey reports 68 stability maps, 14 with linked or adjacent proof documents and 54 without (§§6–7). The survey count measures documentation linkage, not proof validity or complete implementation coverage.

Finally, the answer’s recommendations follow from the verified techniques and limits: map each trusted signature to a named theorem, preserve explicit metric and unit conversions, use ownership for framing, and add negative controls for weakened bounds, aliasing, and budget misuse. These are proposed engineering lessons. No artifact execution or independent reproduction was performed during this cross-check. Audited 2026-10-12 against the paper: checked every number (46 and 43 Verus items, 313 lines, 0.41/0.68/1.31 s, Table 4 totals, 68/14/54/31 survey counts, ten negative controls plus two pre-checker failures, 14 privacy-arithmetic items), the quotations and their pages, the double_into refutation, the Verus examples and the trusted-base claims. Changed: replaced an Alerus attribution that is not in the paper with SampCert (paper section 8), corrected the Limitations quote location from section 8 to the end of section 7, described Example 4 without the unsupported metric-polymorphic label, and deleted a Vosti and five-studies sentence copied from another study. Not checked: the claims about the ChatGPT attempts and forte_chatgpt_answer.md contents beyond its quoted paper passages.

Last edited: 2026-10-31