Prosecco is a research team at Inria Paris that does formal and practical security research on cryptographic protocols, software security, web security, and hardware protection mechanisms. To this end, we design and implement programming languages, formal verification tools, dynamic monitors, testing frameworks, verified compilers, etc. Software Tools HACL*: High-Assurance Cryptographic Library F*