Ada

84 readers

1 users here now

A community about the programming language, Ada.

About Ada Language

Ada is a modern, high-level programming language designed for developing reliable, efficient, and maintainable software systems. It was developed by the U.S. Department of Defense and is widely used in safety-critical and mission-critical applications. This community is dedicated to all things related to Ada, including discussions, tutorials, news, and projects.

Rules:

Be respectful: Treat fellow community members with kindness and respect. Personal attacks, harassment, or any form of discrimination will not be tolerated.
Stay on topic: Keep discussions focused on Ada language-related topics. Off-topic posts may be removed.
No spam or self-promotion: Avoid excessive self-promotion or spamming of external links. Share relevant content and engage in meaningful discussions.
Provide helpful and constructive feedback: When offering feedback on code or projects, be constructive and supportive. Help others learn and grow.
Follow the instance wide rules.

founded 1 year ago

MODERATORS

ada

Post-quantum key exchange in Ada & SPARK (github.com)

submitted 9 months ago by ada to c/ada

0 comments fedilink hide all child comments

LibMLKEM: a brand new, formally verified implementation of the post-quantum key exchange algorithm ML-KEM, built with the Ada & SPARK.

Why LibMLKEM?

Rock-solid security: SPARK's formal verification guarantees no errors, leaks, or type issues.
Independent & transparent: a completely new take on ML-KEM, free from existing code biases.
Pushing the boundaries: a benchmark for formal verification tools like SPARK, CBMC, and Kani.

Not production-ready yet!

LibMLKEM is for research and demonstration purposes only. It prioritizes security and verifiability over optimization. The constant time property hasn't verified yet.

no comments (yet)

sorted by: hot top controversial new old

there doesn't seem to be anything here