Proofs and Intuitions

A blog about mathematics, computing, formal verification, and the ideas behind them

Posts by Author

Ilya Sergey

Ilya Sergey

  • Verifying Distributed Protocols in Veil

    · verification distributed systems veil model checking lean

    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.

  • Multi-Modal Program Verification in Velvet

    · programming verification lean velvet smt ai

    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.