Vero composition: 43 Lean 4 repos, 743 APIs, 2,705 formal specs

dawnsongtweets · x · 2026-08-23

Vero consists of 43 multi-module Lean 4 instances curated from real-world repositories in Python, Dafny, Verus, and Coq, each with fixed data types and API signatures (743 scored APIs), human-curated formal specifications (2,705 total), and reference implementations for every API. Domains span cryptographic protocols, smart contracts, distributed systems, and data structures, plus a semi-automated curation pipeline extensible to new source languages.

Related event: Dawn Song's Team Releases Vero, First Repo-Level Formal Verification Benchmark(8 posts)→

Original post →

More from Research

Research channel →