Blog

My research lab now has a new blog “Proofs and Intuitions”. There, we will share our findings, updates, and practical insights on formal verification, machine-assisted proofs, programming languages, and related topics. In our first post, we show how to specify and verify imperative programs in Lean using Velvet—an embedded verifier that combines automated symbolic reasoning with AI-assisted theorem proving.