Hi Vero team,
I’m a maintainer of Benchmark Radar. I read your paper and really enjoyed your work on repository-level verified code generation. After reading it, I searched for Vero on Benchmark Radar, but couldn’t find it.
I investigated our discovery pipeline and found that it uses the GitHub repository’s About description as its summary, without falling back to the README. Vero currently has no description, so our relevance checks receive only the repository name, which does not provide enough information to identify it as a benchmark. Your README explains the project clearly; our pipeline simply wasn’t using that information.
I’ve now added sunblaze-ucb to Benchmark Radar’s research-group organization watchlist through PR #556, which has been merged.
I’d also recommend adding a short About description to help Vero be discovered more broadly through GitHub search and tools that rely on repository metadata. For example:
An AI agent benchmark for repository-level verified code generation in Lean 4, evaluating implementation and proof synthesis.
Topics such as benchmark, ai-agents, code-generation, formal-verification, and lean4 could also help people find it.
On our side, discovery still uses time windows, so adding the organization and updating metadata will not automatically backfill the historical repository. We’re tracking that limitation separately in Benchmark Radar #555.
Thanks for sharing Vero! I’d love to help more people discover and use your benchmark.
Hi Vero team,
I’m a maintainer of Benchmark Radar. I read your paper and really enjoyed your work on repository-level verified code generation. After reading it, I searched for Vero on Benchmark Radar, but couldn’t find it.
I investigated our discovery pipeline and found that it uses the GitHub repository’s About description as its summary, without falling back to the README. Vero currently has no description, so our relevance checks receive only the repository name, which does not provide enough information to identify it as a benchmark. Your README explains the project clearly; our pipeline simply wasn’t using that information.
I’ve now added
sunblaze-ucbto Benchmark Radar’s research-group organization watchlist through PR #556, which has been merged.I’d also recommend adding a short About description to help Vero be discovered more broadly through GitHub search and tools that rely on repository metadata. For example:
Topics such as
benchmark,ai-agents,code-generation,formal-verification, andlean4could also help people find it.On our side, discovery still uses time windows, so adding the organization and updating metadata will not automatically backfill the historical repository. We’re tracking that limitation separately in Benchmark Radar #555.
Thanks for sharing Vero! I’d love to help more people discover and use your benchmark.