Proofs and Intuitions

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 he

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

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 i

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 futu

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 f

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.

Welcome to Proofs and Intuitions! This is a blog about mathematics, formal verification, and the ideas that connect them.