F* is a new ML-like programming language. It also works as a general-purpose verification tool for higher-order stateful programs. It is based on (and subsumes) two prior projects from MSR: Fine and F7.