Ilya Sergey used AI to formalize a new reference checker for the Move blockchain language in 27 working days
Ilya Sergey used AI to formalize a new reference checker for the Move blockchain language in 27 working days
On August 14, Ilya Sergey, a coauthor of a paper accepted at the OOPSLA’26 programming languages conference, described its formal model. Lean is an environment in which a program checks whether a proof follows from a predefined set of rules.
Move is a language for smart contracts, which are blockchain programs that manage digital assets. Its borrow checker requires every temporary reference to point to existing data and permits only one mutable reference to access a given memory location at any one time.
The authors proposed a new set of rules for this check. In the simplified MoveLight model, the path from a reference to its data is represented by a regular expression, which specifies a pattern for a sequence of object fields. If a write could affect memory addressed by another reference, the algorithm detects the overlap between the paths and rejects the operation. The authors integrated this design into the Move checker used by Sui. Lean verifies both the safety proof for the rules and the executable algorithm, while also comparing the algorithm against tests from the production Move compiler.
After discussions with the Move developers, Sergey defined the MoveLight model and its typing rules. The Claude Code AI assistant, using the Opus 4.5 and 4.6 models, constructed the semantics, lemmas, and proofs. Sergey reviewed the code, divided the problem into smaller parts, and revised the proof plan. After 27 working days, this process produced an artifact containing roughly 39 thousand lines of Lean, including the executable algorithm and tests.
In the paper’s section on the formalization process, the authors write: “For new statements, the AI often chose incorrect proof strategies.” The failed attempts revealed three errors. Two were in the formalization of the typing rules. The third concerned the check performed when returning from a function, which included references that were no longer active and therefore rejected safe code. The Move team confirmed and fixed this issue.
In March, Terence Tao demonstrated that when Claude Code works with Lean, the mathematician selects the lemmas and keeps the proof process under control. In the Move project, this human role begins even earlier, with choosing the model, stating the invariants, and checking that the formalization describes the actual system.
In an essay, Sergey connects this experience to the pace of research. AI can complete repetitive mechanization in weeks, leaving the researcher to formulate the problem and evaluate the design. Formal verification turns rapidly produced code into an object that can be checked, but a human still determines the quality of the question and the model.