SPARKNaCl: A Verified, Fast Re-implementation of TweetNaCl
summary
SPARKNaCl re-implements the TweetNaCl crypto API in the SPARK language and provides fully automated, complete proofs of type- and memory-safety plus key correctness properties. It describes applying verification-friendly transformations and optimizations so the SPARK code is competitive with — and for Ed25519 Sign on a bare-metal 32-bit RISC‑V — about 3× faster than the original TweetNaCl C implementation, while remaining small and BSD-licensed.
AI-written summary · about
related talks
39mPrivacy and Evolution of SNARKs
54mSnarky: Algebraic effects in the Coda cryptocurrency
23mSonic: Nearly Trustless SNARK Setups
18mSoK: Understanding zk-SNARKs: The Gap Between Research and Practice
48mzkSNARKs — Cryptographic Proofs for Scaling and Security Challenges
36mScalable Zero-Knowledge Proof Made Easy
25mGemini: Elastic SNARKs for Diverse Environments
01h 00mError-Correcting Codes That Enable Efficient SNARKs