Cryspen collaborates with the Prosecco team at Inria to develop a usable, robust, development environment and verification toolchain for security critical software.

The toolchain supports security analysis and full functional verification of production software. Software engineers, cryptographers, and proof engineers work together to implement the software and formalise critical properties. Once verification is complete, the toolchain guarantees clean, well-documented, deployable code in Rust, C, or WebAssembly. Conversely, if an attack or bug is found, it is presented back to the cryptography or software engineer.