Verifying Lowlevel Code for Security and Correctness in F*
Videos of the lectures are here.
The material I presented represents work by a large team of people working on F* and Project Everest.
For questions about F* join fstar.zulipchat.com.

Lecture 1
 Wednesday, June 26: Overview, Functional core of F*, Basic effects, WPgeneration, Richer memory models
 Thursday, June 27: lenses; then EverParse: parsers, parser generators
 EverParse, Paper at USENIX Security 2019
 EverParse software on GitHub

Lecture 2: Thursday, June 27: Modeling and Proving Cryptographic Security
Code: In the examples/crypto directory: Make it using `make f Makefile.oplss verifyall`

Authenticated Encryption: AE.fsti

UFCMA MAC: MAC.fst

INDCPA Encryption: CPA.fst

Lecture 3: Friday, June 28: Relational proofs of equivalence

Relational proofs by monadic reification (lecture slides)
Based on a CPP 18 paper.
I also mentioned these other papers:

Simple relational correctness proofs for static analyses and program transformation, Nick Benton, 2004

Turing completeness totally for free, Conor McBride

Perfect secrecy of Onetime pads:
OTP.fst

Semantic secrecy of El Gamal encryption:
ElGamal.fst

Setoids, modules, functors, epsilon equivalences
Setoids.fst

Lecture 4: Saturday, June 29: Verified cryptographic primitives, EverCrypt and Vale.

Lecture slides (Thanks Jonathan and Chris!)
Vale @ POPL '19
EverCrypt paper
EverCrypt code

Efficient, extensible VC generation with typeclasses and normalization MiniValeSemantics.fst

Generic programming, for a model of verified interoperability between Low* and Vale (calling conventions only)
Interop.fst
Altenkirch and McBride, Generic Programming within Dependently Typed Programming