FStarLang/FStar

A Proof-oriented Programming Language

Source code at GitHub https://fstar-lang.org

{
  "createdAt": "2014-04-03T17:32:49Z",
  "defaultBranch": "master",
  "description": "A Proof-oriented Programming Language",
  "fullName": "FStarLang/FStar",
  "homepage": "https://fstar-lang.org",
  "language": "F*",
  "name": "FStar",
  "pushedAt": "2025-11-26T00:58:28Z",
  "stargazersCount": 2928,
  "topics": [
    "c-language",
    "dependent-types",
    "f-sharp",
    "fstar",
    "ocaml",
    "programming-language",
    "proof-assistant",
    "smt",
    "theorem-proving",
    "verification"
  ],
  "updatedAt": "2025-11-26T00:14:36Z",
  "url": "https://github.com/FStarLang/FStar"
}

F*: A Proof-oriented Programming Language

F* website

More information on F* can be found at www.fstar-lang.org

Installation

See INSTALL.md

Online book

An online book Proof-oriented Programming In F* is in the works and regular updates are posted online. The book is available as a [PDF], or you can read it while trying out examples and exercises in your browser interface from this [tutorial page].

[tutorial page] !: https://www.fstar-lang.org/tutorial/ [PDF] !: http://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf

Wiki

The [F* wiki] contains additional technical documentation on F*, and is especially useful for topics that are not yet covered by the book.

[F* wiki] !: https://github.com/FStarLang/FStar/wiki

Editing F* code

You can edit F* code using various text editor. Emacs has the best support currently, providing syntax highlighting, code completion and navigation, and interactive development, using [fstar-mode.el]. However, other editors also have limited support. More details on [editor support] are available on the [F* wiki].

[editor support] !: https://github.com/FStarLang/FStar/wiki/Editor-support-for-F* [fstar-mode.el] !: https://github.com/FStarLang/fstar-mode.el

Extracting and 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 for instance to 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 via OCaml] on the [F* wiki].

[executing F* code via OCaml] !: https://github.com/FStarLang/FStar/wiki/Executing-F*-code

Also, code written in a C-like shallowly embedded DSL can be extracted to C or WASM by the KaRaMeL tool, and code written in an ASM-like deeply embedded DSL can be extracted to ASM by the Vale tool.

Chatting about F* on Slack and Zulip

The F* developers and many users interact on this Slack forum---you should be able to join automatically by clicking here, but if that doesn’t work, please contact the mailing list mentioned below.

Users can also chat about F* or ask questions at this Zulip forum.

Mailing list

We also have a [mailing list] which we use mainly for announcements.

[mailing list] !: https://groups.google.com/g/fstar-mailing-list

Reporting issues

Please report issues using the [F* issue tracker] on GitHub. Before filing please 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.

[F* issue tracker] !: https://github.com/FStarLang/FStar/issues [online F* editor] !: https://www.fstar-lang.org/run.php [the GitHub sources] !: [https://github.com/FStarLang/FStar/blob/master/INSTALL.md#building-f-from-sources

Contributing

See CONTRIBUTING.md

License

F* is released under the [Apache 2.0 license]; for more details see LICENSE

[Apache 2.0 license] !: https://www.apache.org/licenses/LICENSE-2.0