Welcome to the F* wiki! This wiki contains additional, usually more in-depth, technical documentation on top of the F* tutorial. If you add a new page, please add it to the table of contents below!

This is a best effort thing, so it might be unpolished, inconsistent, or out of date. Please help us improve it! This wiki might one day expand into a full-fledged "reference manual", or something. Use the search feature of GitHub or table of contents on the right to navigate.

• F* tutorial
• Installing F*
• Editor-support-for-F*
• Executing F* code
• What is verified, what is extracted?
• Early stumbling blocks, FAQ
• Different types of equality in F*
• Sliding admit verification style
• rlimits: Machine Independent Resource Limits for Deterministic Execution
• Quantifiers and patterns
• F* symbols reference
• Calculational proofs
• Sugar for manipulating connectives in classical logic

• Dealing-with-F★-dependencies
• F★-Interfaces (simple version)
• F★ interfaces (split-file, more complicated version)
• Generating documentation with fsdoc comments

• Using SMT fuel and the normalizer
• Robust, replayable proofs using unsat cores, (aka, hints, or how to replay verification in milliseconds instead of minutes)
• Running F* from a docker image
• Profiling z3 queries
• Tactics
• Wrapping OCaml modules for use in F*
• Lambda Literals in SMT Proof

• The syntax of arrow types and default effects
• Recent backward incompatible changes
• Qualifiers-for-definitions-and-declarations
• Custom attributes
• Migrating-code-to-universes
• Parsing and operator precedence
• Machine integers
• Deriving hasEq predicate for inductive types, and types of equalities in F*
• Modules, namespaces and name resolution
• Local opens
• Explicit universes
• Partial evaluation before extraction
• Tactic meeting minutes
• Unicode Support in F★
• New modifies clauses with buffers, references and regions
• SMT-Equality-and-Extensionality-in-F*

• Working with files with huge verification times
• Error-locations-in-generated-OCaml-code
• Pragmas (#set-options, #reset-options)
• Debugging FStar
• F* Heap Model
• Some-issues-and-workarounds-when-writing-interfaces
• Running F* Programs Interactively with the OCaml Interactive Toplevel

• Some general guidelines about src syntax, the core AST
• Bootstrap-process-of-F★-(the-gory-details)
• Editing F* compiler sources
• Structure of src dir
• The-many-Makefile-targets
• Editing files in the library
• Writing code in the intersection of F★, F# and OCaml
• Profiling F* (Linux/OCaml)
• Creating binary packages for your platform
• F* release process; Release notes for F* 0.9.5
• Moving to menhir
• The unification algorithm
• Timing your changes
• Contributing to master
• Some day, maybe

• Top-level effects
• Cheap functors
• Indexed effects
• F* Lean Integration
• Style guide
• let mutable
• Large-scale separate verification & compilation
• Roadmap for usable interfaces
• Getting better mileage out of Z3
• Improving the sequence library
• Uniform effects

• Efficient execution of F* tactics (native compilation scheme)
• F* tactics proposal (original design of tactics in relation to Lean)
• Generalizing tactics to customize the behavior of F*

• Elements-of-Low*-v3
• Abstractions-for-Reasoning-about-Memory-in-F*-Low*
• Low*-v3-surface-language-:-Steel

• Project topics on F*

• Steel (outdated)
• Steel-(Outline) (outdated)
• Steel:-surface-language (outdated)
• Steel:wishlist

• CI wishlist
• Compiling tactics