Cryspen is a boutique development and consulting studio focused on bringing state-of-the-art privacy and cryptography solutions to customers, using cutting-edge formal methods. We closely collaborate with research groups at Inria and elsewhere to help them improve their research software analysis tools and apply them to industrial design and software development.

Few companies have the expertise or resources to establish dedicated formal methods teams. Cryspen makes formal methods instantly accessible, enabling its customers to adopt the new benchmark in terms of software security and reliability, without sacrificing performance or having to adopt new programming languages.

Design & Analysis

The workflow involves several stages that are typically repeated iteratively until the final product or system meets the desired requirements.

The workflow begins with a design stage, where the requirements and specifications of the product or system are defined. This stage involves brainstorming, sketching, and creating prototypes to explore and refine different designs.

After the design is finalized, the next stage is writing the formal specification of the design. We make use of tools such as hacspec that we develop in-house that makes the specifications accessible for everyone involved.

Based on the formal specification we perform a rigorous security analysis of the design. This stage involves using tools such as F* or ProVerif to create mechanized, reproducible security proofs. This can lead to another iteration of the design stage, where changes are incorporated into the design to achieve the desired security goals. The modified design is then specified and evaluated again through analysis, and the process continues until the designed system meets all requirements and specifications.

Throughout the workflow, it is important to maintain clear communication and collaboration between our team and the customer. This ensures that design decisions are based on accurate and relevant information, and that any issues or limitations are identified and addressed as early as possible.

After the design meets all requirements and specifications it is documented in systems and security whitepaper.

High-Assurance Software Development

Based on a (formal) specification we produce a production-ready, efficient implementation of the specification. This implementation can be in Rust, C, OCaml, or WebAssembly, as needed by the customer.

In addition to using state-of-the-art software engineering practices, we aim for the highest level of assurance by using formal verification tools (see circus) to develop security and correctness proofs for the implementation code.

We offer long-term support and maintenance contract for our code and its proofs.