ArkLib
Formally Verified Arguments of Knowledge in Lean
Tech stack & purpose
ArkLib is a Lean 4 formalization of SNARK-related theory, interactive oracle reductions, and proof systems. The project formalizes arguments of knowledge with a focus on zero-knowledge and cryptographic proof systems. The codebase is organized into reusable mathematical foundations in the Data module, core abstractions for interactive oracle reductions, protocol formalizations, and commitment schemes, along with local extensions to Mathlib and the VCV-io library intended for upstream contribution. The repository includes extensive documentation covering papers, concepts, audits, and operational workflows to support both human and agent contributors working on formally verified cryptographic theory.
Community & reference links
Languages
Contributors (top 30 of 40)
- Quang Dao426 commits · 104 followers
- Alexander Hicks162 commits · 46 followers
- Frantisek Silvasi153 commits · 25 followers
- Ilia Vlasov148 commits · 69 followers
- Katy Hristova141 commits · 11 followers
- Julian Sutherland107 commits
- Pietro Monticone41 commits · 1,160 followers
- Lucendio28 commits · 15 followers
- dependabot[bot]25 commits · 0 followers
- Chung Thai Nguyen18 commits · 0 followers
- Bolton Bailey16 commits · 58 followers
- Devon Tuma11 commits · 22 followers
- Tobias Rothmann11 commits · 10 followers
- Vladislav Isenbaev11 commits · 45 followers
- X9 commits · 10 followers
- Sunghyeon Jo7 commits
- Elias Judin5 commits
- Derek Sorensen4 commits
- Stefano Rocca4 commits
- aleph-prover[bot]4 commits
- AryaETHn4 commits · 3 followers
- ErVinuelas4 commits · 6 followers
- Desmond4 commits · 3 followers
- jeinryu3 commits · 3 followers
- Gabe3 commits · 91 followers
- Poulami Das3 commits
- github-actions[bot]3 commits · 0 followers
- Apoth3osis2 commits · 6 followers
- Gregor Mitscha-Baude2 commits · 216 followers
- Latif Kasuli2 commits
