FStarLang/FStar

---

FStarLang/FStar.json

{
  "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": "2026-07-12T14:51:31Z",
  "stargazersCount": 3065,
  "topics": [
    "c-language",
    "dependent-types",
    "dijkstra-monads",
    "f-sharp",
    "fstar",
    "interactive-theorem-proving",
    "ocaml",
    "program-proof",
    "programming-language",
    "proof-assistant",
    "smt",
    "theorem-proving",
    "verification"
  ],
  "updatedAt": "2026-07-12T13:52:25Z",
  "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 available and updates are posted online periodically. 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

Editing F* code

You can edit F* code using various text editors, with Emacs and VSCode currently having the most substantial support, including syntax highlighting, code completion and navigation, and incremental, interactive development.

• [fstar-mode.el] !: Emacs mode for F*
• [fstar-vscode-assistant] !: VS Code plugin for F*

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 [fstar-vscode-assistant] !: https://github.com/FStarLang/fstar-vscode-assistant

AI Agents

AI agents are proficient at using F* and Pulse.

Especially if you are using Copilot CLI or Claude Code, we recommend installing the [proof-copilot] plugin, which provides agents and skills with prompts for specific features of the language and its tooling.

[proof-copilot] !: https://github.com/FStarLang/proof-copilot

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 Pulse, a DSL in F* for concurrent, imperative programming, can be extracted to C or Rust by the KaRaMeL tool.

Additionally, code written in an ASM-like deeply embedded DSL can be extracted to ASM by the Vale tool.

Chatting about F* on Zulip

F* developers and users can chat about F* or ask questions at this Zulip forum.

(An older forum on Slack is no longer used.)

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

Other Documentation

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

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