A Proof-oriented Programming Language

programming-language dependent-types ocaml theorem-proving verification f-sharp proof-assistant smt c-language fstar interactive-theorem-proving program-proof dijkstra-monads

• Updated Nov 12, 2026
• F*

A verification toolchain for Rust programs

rust compiler ocaml coq rust-lang lean formal-methods proofs program-verification formal-verification fstar hol4 deductive-reasoning

• Updated Nov 12, 2026
• OCaml

F* library for verifying neural networks.

neural-networks smt-solver fstar

• Updated Mar 25, 2023
• F*

🦅 VSCode extension for F* with IDE features

ide vscode-extension fstar lsp language-server-client

• Updated Mar 21, 2020
• TypeScript

Various ideas in OCaml, Haskell, and F*

haskell ocaml fstar

• Updated Dec 6, 2024
• Haskell

Sample how to perform export of F* to F# with Nuget

fstar

• Updated Sep 18, 2024
• F*

F* MSBuild SDK

fstar msbuild-sdk

• Updated Aug 25, 2026
• F*

Proof or it didn't ship! ✅ A curated list of resources for formally verified code, written by people and by AI.

awesome coq theorem-proving proof-assistant awesome-list formal-methods code-generation isabelle dafny smt program-verification formal-verification fstar ai-agents verus lean4 llm rocq neural-theorem-proving vericoding

• Updated Oct 12, 2026
• Python

A formally verified implementation of a bolt-on security device for ICS networks. Designed with TLA+ and written/proved in F*

security proof verification formal-methods fstar ics-security sel4 tlaplus

• Updated Jan 11, 2020
• C

Working through the F* tutorial (https://www.fstar-lang.org/tutorial/)

tutorial nix theorem-proving sphinx literate-programming exercises learning-by-doing fstar

• Updated Aug 22, 2018
• Nix

Translates FStar official docs to reStructuredText

fsharp fstar

• Updated Jan 16, 2019
• F#

FStar Documentations in readthedocs

docs fstar documentations

• Updated Jan 16, 2019

Virtualization-based code protector and V-ISA synthesizer in OCaml: lifts x86-64/ARM64/RISC-V into a hardened C++20 VM runtime with CFF, MBA and metamorphic handlers, plus a differential-fuzzing test bed.

emulator security obfuscation virtual-machine x86-64 ocaml reverse-engineering arm64 formal-verification risc-v dune fstar sail anti-analysis code-protection devirtualization

• Updated Nov 2, 2026
• OCaml

🧠️🖥️2️⃣️0️⃣️0️⃣️1️⃣️💾️📜️ The sourceCode:FStar category for AI2001, containing F* programming language datasets

ai gplv3 artificial-intelligence dataset r-language md txt fstar gpl3 fstar-lang fstar-language rmarkdown-language ai2001 ai-2001 ai2001-dataset ai-2001-dataset ai2001-development ai-2001-development source-code-dataset fstar-sc-dataset

• Updated Oct 22, 2023
• R

collection fstar

• Updated Jul 25, 2020

A repository for showcasing my knowledge of the F* programming language, and continuing to learn the language.

knowledge article dotnet gplv3 learn md txt fstar gpl3 seanpm2001 seanpm2001-education seanpm2001-learn fstar-lang fstar-language learn-fstar learn-fstar-lang learn-fstar-language fstar-collection

• Updated Sep 13, 2022
• F*

[WIP] Writing low* code to implement dlists

wip fstar

• Updated Aug 6, 2019
• F*

My solutions for the F* turorial

tutorial-exercises fstar

• Updated Jul 27, 2022
• F*

The F* Programming language IDE submodule for SNU Programming Tools.

web-development programming web-ide ide snu fstar snu2d-programmingtools snu-2d snu-programming-tools snu-2d-programmingtools snu-development snu-2d-programming-tools snuprogrammingtools snu2dprogrammingtools fstar-lang fstar-language

• Updated Sep 13, 2022
• F*

implementation of gcd function in fstar.

proof-assistant gcd fstar

• Updated Jul 6, 2018
• Makefile