Ilya Sergey

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

  March 18, 2026 · lean move types verification ai

  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.

• Verifying Distributed Protocols in Veil

  February 9, 2026 · verification distributed systems veil model checking lean

  In this post, we discuss how to formalise, test, and prove the correctness of a classic distributed protocol by combining model checking, automated deductive verification, and AI-powered invariant inference in Veil, a new auto-active Lean-based verifier for distributed protocols.

• Multi-Modal Program Verification in Velvet

  January 21, 2026 · programming verification lean velvet smt ai

  In this post, we will show how to specify and verify imperative programs in Lean 4 using Velvet—an embedded verifier, which relies on a combination of automated symbolic and AI-assisted theorem proving techniques.