F* subsumes several prior languages, including Fine, F7, FX and others. We have used it to verify nearly 50,000 lines of code, ranging from crypto protocol implementations to web browser extensions, and from cloud-hosted web applications to key parts of the F* compiler itself.
You can try it out on the web at rise4fun/FStar/tutorial/guide. A download of F* is no longer available on this site. We have moved to developing F* under a new open source license on github and expect to make an official release of the next version of the tools at the end of the summer (2014). You can track our progress at github.
Some recent projects based on F*
Self-certification of F*: We have verified the F* type checker using F* itself, using a novel bootstrapping technique called self-certification. You can read more about this in a paper from POPL 2012 available here.
Probabilistic relational verification: An extension of F* called rF* adapts the type checker to verify properties of multiple programs, or properties of more than one execution of a program, i.e., so called "hyperproperties". We have used rF* to verify a number of interesting programs implementing various cryptographic constructions and protocols. This work is described in this paper, with supplementary materials available here.
People currently working on F*
Karthikeyan Bhargavan (INRIA)
Antoine Delignat-Lavaud (INRIA)
Cedric Fournet (MSR)
Catalin Hritcu (INRIA)
Chantal Keller (MSR-INRIA)
Alfredo Pironti (INRIA)
Pierre-Yves Strub (IMDEA)
Nikhil Swamy (MSR)
- Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits, Verifying Higher-order Programs with the Dijkstra Monad, in ACM Programming Language Design and Implementation (PLDI) 2013, ACM, June 2013
- Jean-Baptiste Jeannin, Guido de Caso, Juan Chen, Yuri Gurevich, Prasad Naldurg, and Nikhil Swamy, DKAL*: Constructing Executable Specifications of Authorization Protocols, no. MSR-TR-2013-19, March 2013
- Cole Schlesinger and Nikhil Swamy, Verification Condition Generation with the Dijkstra State Monad, no. MSR-TR-2012-45, 22 April 2012
- Pierre-Yves Strub, Nikhil Swamy, Cedric Fournet, and Juan Chen, Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq, in In Proceedings of the ACM Symposium on Principles on Programming Languages, ACM, January 2012
- Nikhil Swamy, Juan Chen, Cedric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang, Secure Distributed Programming with Value-dependent Types, in The 16th ACM SIGPLAN International Conference on Functional Programming (ICFP 2011), ACM SIGPLAN, September 2011
- Matthew Fredrikson and Ben Livshits, RePriv: Re-Envisioning In-Browser Privacy, in Proceedings of the IEEE Symposium on Security and Privacy, IEEE Computer Society, 23 May 2011
- Arjun Guha, Matthew Fredrikson, Benjamin Livshits, and Nikhil Swamy, Verified Security for Browser Extensions, in Proceedings of the IEEE Symposium on Security and Privacy (Oakland), IEEE, 22 May 2011
- Pierre-Yves Strub, Cedric Fournet, and Nikhil Swamy, Mechanized soundness proofs for F*, 1 April 2011
- Nikhil Swamy, Juan Chen, Cedric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang, Secure Distributed Programming with Value-Dependent Types, no. MSR-TR-2011-37, 24 March 2011