I Tried to Verify Popular Rust OSS with Lean 4, but Found Bugs Instead

From proof attempt to upstream finding

The benchmark repository contains published ports and their proof projects. For example, its documented checks for the RustFS port and the full corpus are:

h5i app doctor ports/rustfs
h5i app extract --check ports/rustfs
h5i app check --all ports

These commands check the port and proof workspace; they do not reproduce any vulnerability. The last command is a strict gate and can fail on unfinished proofs. The RustiCal case discussed below was still being prepared for publication when the research account appeared. Distinguishing a port from its original application is essential: an omitted upstream check can create a false counterexample in the port.

RustiCal: the checked object and deleted rows diverged

A calendar object is identified by principal, calendar ID, and object ID. The hard-delete path authorized the caller's own object, but the database operation selected rows using only the latter two identifiers. In simplified SQL, the vulnerable scope was:

DELETE FROM calendarobjects
WHERE cal_id = ? AND id = ?;
-- The principal is missing from the selection.

The property worth proving is a frame condition: after Alice deletes one of her objects, Bob's objects are unchanged. The telling reproduction uses Alice and Bob with the same local calendar and object names. A direct attempt to delete Bob's object can be denied, yet deleting Alice's matching object can still remove Bob's row because the write is wider than the authorization decision. The RustiCal advisory documents the confirmed issue.

OxiCloud: playlist access did not imply file access

The playlist path crossed a different boundary. A user could modify a playlist they owned, refer to another user's private file, and then receive that file's metadata in a track response. The permissions are on two objects, not one:

can edit playlist  ≠  can read every referenced file
             │
             └── response may include filename, size, MIME type, metadata

A property over playlist ownership alone would pass while the leak remained. The useful property quantifies over the response: every file represented in the returned tracks must be readable by the caller. The upstream fix discussion shows how the missing file check was addressed.

RustFS: the outer limit did not bound the inner work

RustFS expanded policy variables through nested substitution. An iteration cap guarded an outer loop, but a nested scan could rebuild an expression and continue without consuming that cap. A tiny input could drive disproportionate resolver work. A useful termination argument must show that every substitution decreases a measure or consumes a shared budget; merely finding a counter in the outer loop is insufficient.

The benchmark's ported resolver models the corrected resume point explicitly:

pub struct Pending {
    pub text: Vec<u8>,
    pub resume: usize,
}
// A newly substituted placeholder waits for a bounded later pass.

The resume position stops one scan from immediately restarting at the beginning of its newly substituted text. The RustFS advisory records the upstream denial-of-service condition; the port's code shows the related model used for differential checks.

What the three cases teach

They fail for different reasons: a write scope wider than its check, a reference to an object with its own permission, and a nested computation outside its intended bound. The common method is to state the invariant, inspect the exact implementation path, and reproduce any suspected failure in the original application before calling it a finding.

Formal verification did not automatically diagnose these bugs. An unsuccessful proof could also mean a missing lemma, a bad model, or unsupported Rust. Its value was forcing a precise question that could be tested against real behavior. This article is an original synthesis of the original research account, the benchmark, and the linked upstream reports.