F*: a starting point for coding agents
====================================

F* is a proof-oriented language and multi-language verification framework.
Pulse provides concurrent separation logic. Kuiper targets GPU programs.
PAL and PAL-CS translate annotated C and C# into Pulse for verification.

Start here
----------

Website and examples: index.html
Machine-readable example index: examples/manifest.json
Short documentation index: llms.txt
Tutorial: tutorial/book/intro.html
Pulse tutorial: tutorial/book/pulse/pulse.html
Installation: https://github.com/FStarLang/FStar/blob/master/INSTALL.md
Ready-to-use environment: https://github.com/FStarLang/TryFStar

Agent tooling
-------------

F* Proof Copilot supplies an F*/Pulse coding agent and skills for specification
review, verification, proof debugging, SMT profiling, incremental typechecking,
project setup, source builds, and C extraction.

Canonical instructions and installation for Copilot CLI and Claude Code:
https://github.com/FStarLang/proof-copilot

Use the repository's current instructions rather than assuming a plugin
includes the compiler, solver, or every related DSL. F* and Z3 are separate
toolchain prerequisites. Dedicated Kuiper and other DSL support is not implied.

Working with the examples
------------------------

The HTML contains real source and generated output, readable without JavaScript.
Tabs are a presentation convenience, not the only way to retrieve the code.
Fetch complete files using the Full file links or examples/manifest.json.
Resolve manifest file paths relative to examples/. Each entry records a SHA-256
hash and an inclusive, one-based range of displayed lines; the complete file
may include imports, supporting declarations, or launch code not shown on screen.

Read the relevant example instructions or generation script:

Functional F*: examples/functional/generate.sh
Pulse: examples/pulse/README.md
Kuiper / CUDA: examples/kuiper/README.md
PAL / C: examples/pal/README.md
PAL-CS / C#: examples/pal-cs/generate.sh

The functional and PAL-CS directories also contain test.sh and toolchain.txt.
From a checkout of the website directory, their reproduction commands are:

FSTAR_EXE=/path/to/fstar.exe bash examples/functional/generate.sh
FSTAR_EXE=/path/to/fstar.exe bash examples/functional/test.sh
PAL_CS_ROOT=/path/to/pal-csharp bash examples/pal-cs/generate.sh
PAL_CS_ROOT=/path/to/pal-csharp bash examples/pal-cs/test.sh

Follow each example's documented tool versions and reproduction commands.
The directories contain the source, generated artifacts, and, where provided,
provenance and test drivers. Generated files are not handwritten equivalents.
Do not install or run unrelated toolchains just to read an example.

Proof-oriented workflow
-----------------------

1. Review the intended specification and input preconditions.
2. Implement against that specification.
3. Run F* and use its actual diagnostics to repair failures.
4. Re-run verification after source changes, before extraction.
5. Extract, compile, and run the relevant backend tests.

Do not weaken the intended specification just to obtain a successful check.
Do not introduce admits, lax mode, or admitted SMT queries and describe the
result as verified. Report unresolved obligations and assumptions explicitly.
Tests complement verification; they do not discharge proof obligations.

Keep claims within the checked specification. Check separately for termination,
overflow conditions, functional correctness, and specification completeness.
Some examples rely on axiomatized primitives or research libraries with unfinished
proofs. In particular, read the Kuiper README's trust-boundary notes. A successful
check is not a claim that the compiler, runtime, libraries, or application intent
are all formally verified.

Research bibliography: research.html
F* sources: https://github.com/FStarLang/FStar