Loom

We are thrilled to release Loom, a framework for embedding multi-modal verifiers in Lean. In particular, using Loom, we have implemented Velvet, a Dafny-style verifier allowing for both automated and interactive proofs. The accompanying paper (with Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, and Vitaly Kurin) is accepted at POPL’26.