Import projects from Beneficial AI Foundation

[Zhang-Liao]

In Beneficial AI, we develop several software verification projects that could serve as valuable benchmarks for SorryDB.

At the moment, we have two projects that are suitable for inclusion:

1. Dalek-lean
   This project verifies the Rust library curve25519-dalek, which implements cryptographic operations widely used across many systems and applications. A more detailed introduction is available in the repository documentation.

2. Vericoding Bench
   This benchmark was introduced in our paper: Vericoding paper.

At this stage, we prefer not to include our SPQR protocol verification library because it is still under active development, and many specifications remain unprovable at the moment. We would instead propose adding the SPQR library at a later stage once the project becomes more stable.

I would also like to discuss a possible extension of SorryDB: introducing an alternative evaluation mode in which every proof in a project is replaced with sorry, and LLM agents are evaluated on their ability to reconstruct the entire project proof set.

This setup is feasible because I have already implemented a script that automatically replaces proofs with sorrys. For each target library, we could:

1. initialize the project with all proofs removed,
2. later restore the completed proofs in a separate commit, and
3. upload both versions to SorryDB for evaluation.