Program verification with F*

Guest lecture and accompanying lab session for the Advanced Programming Course (ITT8060) at the Tallinn University of Technology.

Lecture slides (6.12.2023)

Lab exercises (6-7.12.2023)

These exercises are mostly independent of each other, so you do not need to do them in the given order, but the earlier ones are generally more basic.

Out of all of them, Exercise 7 is probably the most involved. It lets you simultaneously practice the verification of both pure and stateful programs.

Verifying purely functional programs

Verifying stateful programs

Verifying purely functional and stateful programs

Verifying monotonic stateful programs


Useful code snippets

Sample solutions

Setup instructions

Using F* in your browser

Deploying F* on your computer

Using F* interactively

More references


The lecturer has received funding from the Air Force Office of Scientific Research under awards number FA9550-21-1-0024.