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

I formalised and proved the correctness of Move’s new borrow checker in Lean: 39,000 lines of mechanised metatheory, produced in under a month with the help of an AI coding assistant. This post tells the story of how it went and what it means for the future of PL research.