OpenMLS is growing!

We’re pleased to announce that we are engaging with INRIA Paris to cooperate on OpenMLS.

Professor Karthikeyan Bhargavan’s Prosecco team at INRIA decisively contributed to the formally verified cryptographic library HACL* (along with Microsoft Research and CMU) and was deeply involved in the design, analysis and standardization of TLS 1.3. More recently, the team published TreeKEM – the core algorithm of MLS.

While OpenMLS already builds on top of formally verified cryptography in HACL*, the cooperation covers new areas, such as exchanging knowledge and findings in the API design, code structure, real-world performance and usability concerns and last but not least exploring the idea of formally verifying parts of OpenMLS in the longer term.