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.

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.

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.

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.

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.

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.

Contributing

See CONTRIBUTING.md

License

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