Notices: This section not yet converted to new layout. Download stats are rolling back out.

This is not the latest version of F* language available.

F* language

Package test results are passing.

Private CDN cached downloads available for licensed customers. Never experience 404 breakages again! Learn more...

This package was approved by moderator gep13 on 8/31/2018.

F*: An ML-like language aimed at program verification

Build status


This package will install F* language with compatable version of z3.
It is recommended that you remove your z3 package and then install F*

F* website

More information on F* can be found at




The F* tutorial provides a first taste of verified programming in
F*, explaining things by example.


The F* wiki contains additional, usually more in-depth, technical
documentation on F*.

Editing F* code

You can edit F* code using your favourite text editor, but Emacs,
Atom, and Vim have extensions that add special support for F*,
including syntax highlighting and interactive development. More
details on editor support on the F* wiki .

Executing F* code

By default F* only verifies the input code, it does not compile or execute it.
To execute F* code one needs to translate it to either OCaml or F#, using
F*'s code extraction facility---this is invoked using the command line
argument --codegen OCaml or --codegen FSharp. More details on
executing F* code on the F* wiki .

Community mailing list

The fstar-club mailing list is dedicated to F* users. Here is where
all F* announcements are made to the general public (e.g. for
releases, new papers, etc) and where users can ask questions, ask for
help, discuss, provide feedback, announce jobs requiring at least 10
years of F* experience, etc.

List archives are public, but only members can post.
Join here!

Slack channel

Users can also ask questions on the #fstar Slack channel at
< >

Reporting issues

Please report issues using the F* issue tracker on GitHub.
Before filing please use search to make sure the issue doesn't already exist.
We don't maintain old releases, so if possible please use the
online F* editor or directly the GitHub sources to check
that your problem still exists on the master branch.


The F* for the masses blog is also expected to become an important
source of information and news on the F* project.


This new variant of F* is released under the Apache 2.0 license;
see LICENSE for more details.

To install F* language, run the following command from the command line or from PowerShell:

C:\> choco install fstar --version

To upgrade F* language, run the following command from the command line or from PowerShell:

C:\> choco upgrade fstar --version


  • tools\chocolateyinstall.ps1 Show
    $ErrorActionPreference = 'Stop'; # stop on all errors
    Install-ChocolateyZipPackage -packageName 'FStar' -UnzipLocation $(Split-Path -Parent $MyInvocation.MyCommand.Definition) -Url64 '' -checksum64 '566139126C1F8DCB0B2A398E6C3779FA16EE15E2B9C96EA7749DADE5B7F05806' -checksumType64 'sha256'

Virus Scan Results

In cases where actual malware is found, the packages are subject to removal. Software sometimes has false positives. Moderators do not necessarily validate the safety of the underlying software, only that a package retrieves software from the official distribution point and/or validate embedded software against official distribution point (where distribution rights allow redistribution).

Chocolatey Pro provides runtime protection from possible malware.


This package has no dependencies.

Package Maintainer(s)

Software Author(s)

  • FStarLang


Release Notes

A large number of people contributed to this release: thanks to all!

Here are a few highlights:

Main new features

  • Meta-F*: A metaprogramming and tactic framework, as described in this report. Code samples are in examples/tactics, examples/native_tactics and the FStar.Tactics and FStar.Reflection libraries. Many people contributed a lot to this work, especially Guido Martinez.

  • Improved type inference with two-phase typechecking: We now build verification conditions for a program after a first phase of type inference. This improves inference of implicit arguments and reduces our trust in the type inference. Thanks to Aseem Rastogi!

  • Caching typechecked modules: F* emits ".checked" files, an on-disk representation of a typechecked module that can be read back later. This significantly reduces the time to load a module's dependences.

Many other improvements

A sampling of improvements across the entire tool chain:

  • Resolving several syntactic ambiguities in the parser

  • A correct pretty printer for surface terms, using fstar --indent

  • A new dependence analysis to support incremental compilation for larger projects

  • Overhauling the higher order unification algorithm, both in the representation of meta-variables and in the handling of unfolding, leading to significant performance and robustness improvements (see

  • Automatic generation of interfaces for modules and tighter enforcement of abstraction boundaries (see's-interface)

  • Improvements to the SMT encoding, removing axioms that lead to performance problems and reducing brittleness related to optimizations in the encoding, notably shallow vs deep encodings

  • Improved type-based erasure for extraction

  • Several new and improved libraries, including a revised treatment of footprints for Low* programs, in FStar.Modifies

  • And work by many people in Project Everest whose use of F* drove a lot of the work in this release.

  • Plus many other improvements and changes as described in

  • And 180 closed github issues

Version History

Version Downloads Last updated Status
F* language 50 Tuesday, August 28, 2018 approved
F* language 290 Tuesday, September 5, 2017 approved
F* language 241 Wednesday, May 3, 2017 approved

Discussion for the F* language Package

Ground rules:

  • This discussion is only about F* language and the F* language package. If you have feedback for Chocolatey, please contact the google group.
  • This discussion will carry over multiple versions. If you have a comment about a particular version, please note that in your comments.
  • The maintainers of this Chocolatey Package will be notified about new comments that are posted to this Disqus thread, however, it is NOT a guarantee that you will get a response. If you do not hear back from the maintainers after posting a message below, please follow up by using the link on the left side of this page or follow this link to contact maintainers. If you still hear nothing back, please follow the package triage process.
  • Tell us what you love about the package or F* language, or tell us what needs improvement.
  • Share your experiences with the package, or extra configuration or gotchas that you've found.
  • If you use a url, the comment will be flagged for moderation until you've been whitelisted. Disqus moderated comments are approved on a weekly schedule if not sooner. It could take between 1-5 days for your comment to show up.

comments powered by Disqus uses cookies to enhance the user experience of the site.