Community

Source Code

Velvet is open source under the Apache 2.0 license. The source code is on GitHub.

Get Help

Ask questions tagging any of the maintainer in Program verification channel on the Lean Zulip.

We are happy to help with questions about using Velvet, reporting bugs, or discussing program verification.

Report Issues

If you encounter bugs or have feature requests, please open an issue: Issue Tracker

Velvet in Action

Teaching

CS5232: Formal Specification and Design Techniques, National University of Singapore, Spring 2026.
Programming with Proofs, a lecture course at Neapolis University Pafos, November 2025.

Programming Competitions

Team VVV won the Best Student Team award at VerifyThis 2026 using Velvet.
A one-person team took first place in a category of the VeHa 2025 verification competition using Velvet.
The memAlloc case study was set as a task in the 2025 CCF ChinaSoft Theorem Proving Contest.

If you use (or plan to use) Velvet for a project, a course, or a competition, we would like to hear about it.

Citing Velvet

If Velvet is useful in your research, please cite the CAV 2026 paper:

@inproceedings{gladshtein2026velvet,
  author    = {Gladshtein, Vladimir and Kurin, Vitaly and Feng, Yueyang and
               Kafle, Dipesh and P{\^i}rlea, George and Zhao, Qiyuan and
               Sergey, Ilya},
  title     = {Velvet: A Foundational Multi-Modal Verifier for Imperative
               Programs in Lean},
  booktitle = {CAV},
  series    = {Lecture Notes in Computer Science},
  volume    = {16683},
  pages     = {228--242},
  year      = {2026},
  publisher = {Springer},
  doi       = {10.1007/978-3-032-32526-6\_11}
}

BibTeX entries for the related papers are on the publications page.

Copyright

Velvet is developed by the members of VERSE Lab at the National University of Singapore, with external contributions.