Arto's Notes re: F*

Installation

https://github.com/FStarLang/FStar/blob/master/INSTALL.md

macOS

$ brew install fstar

$ fstar.exe --version

# Compiling code extracted to OCaml requires Batteries etc:
$ brew install opam
$ opam install batteries zarith stdint

# Compiling code extracted to F# requires Mono:
$ brew install mono

Projects

Libraries

  • HaCl*,
    a formally verified cryptographic library
  • miTLS,
    a formally verified reference implementation of TLS

Tools

  • KreMLin, a tool to extract F* programs to readable C code

Talks

See Also