Proofs and Intuitions

In this post, we discuss Vermilion, an experimental Lean backend for the Verus verifier for Rust, bringing interactive proofs and Lean’s mathematical libraries to programs with ordinary Verus specifications.

A few days ago, a paper I co-authored, Tracking Borrows with Regular Expressions, was accepted to OOPSLA’26. It presents a new type system for Move, a Rust-style smart contract language, built on a rather cute idea: using regular expressions to capture heap reachability. I won’t go into the technical details here. What I want to talk about instead is how the paper was made and how the publication culture in programming language research has changed in the past five months.

Safety property means “nothing bad happens during the run of a program”; liveness property means “the program eventually does something good”. In this post, we walk through a simple proof of a liveness property in Veil, using a basic consensus protocol as an example.

In this post, we show that property-based testing (PBT) is surprisingly effective for validating LLM-synthesised specifications of Lean programs: it is a cheap alternative to symbolic proofs, which helped to detect underspecification in 10% of the specs in state-of-the-art benchmarks for verified code generation.

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.

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.

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.