Proofs and Intuitions

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.