The initial goal of the project was to have a total control on the TCB (Trusted Computing Base) of a webmail for high security environments, in order to be able

The initial goal of the project was to have a total control on the TCB (Trusted Computing Base) of a webmail for high security environments, in order to be able to pass certifications such as Common Criteria (EAL). Our protocol implementations use a specific DSL, that generates Opa code which is strongly statically typed with high-level types such as variants/rows. Although we currently lack many features or optimizations, the approach is clean and much easier to certify.