Verifying Move Borrow Checker in Lean:An Experiment in AI-Assisted PL Metatheory

"The preservation proof contains 153 lemmas (mostly conjectured by AI), collectively showing that each of these steps preserves the 35-field invariant"

Proofs of features are notoriously harder than usage, but I think this illustrates something about how heavyweight the ownership design is and the complexity is forces users to content with.