SPARKNaCl
SPARKNaCl reimplements TweetNaCl in SPARK, proving high-assurance code can be performant, efficient, versatile, and deployable across diverse platforms.
Originally aimed at re-implementing the cryptography library TweetNaCl in SPARK, the project exceeded its initial goal, demonstrating SPARK's capacity to handle complex and high-performance applications.
This achievement, combined with its competitive performance and efficient code size, makes SPARKNaCl not only a theoretical showcase of high-assurance programming but also a practical, deployable library. Furthermore, SPARKNaCl's compatibility with the GNAT Light runtime library (previously known as "Zero Footprint") showcases its versatility, allowing deployment across diverse platforms. This blend of technical sophistication and practical applicability makes SPARKNaCl a valuable asset to the Alire ecosystem.