Verifying Cryptographic Protocol Implementations with F*

Slides

• Markulf: Verifying TLS in F*; Everest Project
• Catalin: A Gentle Introduction to F*
• Markulf: Code-Based Cryptographic Verification in F*

Code

• Exercises from gentle introduction
• Code from gentle introduction slides
• Encrypt then mac example

Setup

• Online editor
• Other ways to install F*

More references

• F* website
• F* tutorial
• F* code on GitHub