Need help with FStar?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

FStarLang
2.0K Stars 186 Forks Apache License 2.0 29.4K Commits 420 Opened issues

Description

Verification system for effectful programs

Services available

!
?

Need anything else?

Contributors list

# 75,229
F#
Shell
f-sharp
theorem...
5532 commits
# 83,250
F#
Shell
f-sharp
theorem...
4602 commits
# 88,913
F#
Shell
f-sharp
theorem...
3963 commits
# 142,478
Shell
coq
f-sharp
theorem...
1375 commits
# 123,038
Shell
blockly
f-sharp
theorem...
1135 commits
# 162,145
F#
Shell
f-sharp
theorem...
997 commits
# 150,996
F#
Shell
formal-...
formal-...
753 commits
# 196,263
F#
Shell
formal-...
formal-...
452 commits
# 166,170
F#
Shell
formal-...
formal-...
440 commits
# 246,376
f-sharp
F#
Shell
theorem...
352 commits
# 119,495
Emacs
coq
f-sharp
integra...
339 commits
# 242,894
Shell
formal-...
f-sharp
F#
291 commits
# 145,335
Shell
OCaml
formal-...
f-sharp
274 commits
# 171,034
Shell
formal-...
formal-...
f-sharp
274 commits
# 257,528
coq
theorem...
Shell
sed
264 commits
# 125,252
Shell
formal-...
formal-...
f-sharp
263 commits
# 258,629
Shell
formal-...
formal-...
f-sharp
201 commits
# 287,331
Shell
coq
sed
f-sharp
194 commits
# 63,065
opam
coq
stock-p...
currenc...
178 commits
# 299,283
f-sharp
F#
Shell
theorem...
178 commits

F*: Verification system for effectful programs

F* website

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

Installation

See INSTALL.md

Tutorial

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

Wiki

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, Visual Studio Code, Atom, and Vim have extensions that add special support for F*, including for instance syntax highlighting, code completion, quick navigation, type hints, and interactive development. More details on editor support on the F* wiki.

You can also edit simple examples directly in your browser by using either the online F* editor that's part of the F* tutorial.

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 a C-like shalowly embedded DSL can be extracted to C or WASM by the KreMLin tool, and code written in an ASM-like deeply embedded DSL can be extracted to ASM by the Vale tool.

Chatting about F* on Zulip

Users can chat about F* or ask questions at https://fstar.zulipchat.com (Zulip is a good open source alternative to Slack)

Community mailing list

The fstar-club mailing list is where various 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 and searchable, but only members can post. Join here!

Blog

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

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.

Contributing

See CONTRIBUTING.md

License

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

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.