The F⭑ implementation is available on Github and is known to work well on Windows, Mac, and Linux. We made a binary release on Oct 13, 2015, and instructions for installing and using are available in INSTALL.md and README.md.
As a backup plan we have also prepared a VirtualBox Linux VM with everything installed (F⭑ source, F⭑ binary built from source, emacs mode, OCaml, Z3, etc). The VM password is fstar, and all the path variables are already set, so you can just open files in emacs and use F⭑.
An online tutorial is also available. In fact, the easiest way to try out F⭑ yourself is directly in your browser by using the online F⭑ editor that's part of the tutorial. For trying out more complex examples, like the samples below, we recommend using the binary release or the VM though, which include the proper Makefiles, etc.
The encoding of accessibility predicates is available in examples/termination/wf.fst. It deeply relies on Property (4) of the built-in well-founded ordering detailed in Section 3.3.1 of our paper.
We proved the termination of a normalizer for the simply-typed lambda-calculus via hereditary substitutions. This development is available in examples/metatheory/hs.fst (now in examples/metatheory/HereditarySubst.fst on stratified_last branch). This formalization is based on an existing Agda formalization (Keller and Altenkirch 2010). It illustrates the termination checker, and in particular the lexicographical ordering on measures applied to arguments of recursive functions.
See examples/crypto/statefulEnc-multi-frame.fst and examples/crypto/statefulEnc-twoLevelHeap.fst for two developments for stateful authenticated encryption, the first with a heap, the second with a hyperheap taking roughly 1m20s and 20s to verify on a typical laptop.
This supplemental archive is an extract of an ongoing port of miTLS to F⭑. It includes 8 verified modules (out of 45 of the whole project), plus supporting files. We chose to include these modules because they can be read and understood in isolation, and because they illustrate the difference in the coding style between F⭑ and F7. For more details, please refer to the enclosed README.txt file.
A separate archive contains the proof of injectivity of message formats used during the TLS handshake. This proof was earlier done in Coq and we have ported it to F⭑. Bear in mind that verifying this proof is resource-intensive: in our experiments verification took more than one hour and memory usage peaked at 16GB.
back to paper page