Owner

FStarLang

14 indexed repositories · View on GitHub

FStar
A Proof-oriented Programming Language

F* · 3107 stars
karamel
KaRaMeL is a tool for extracting low-level F* programs to readable C code

OCaml · 519 stars
fstar-mode.el
Emacs support for F*

Emacs Lisp · 71 stars
steel
The Steel separation logic library for F*

F* · 40 stars
AlgoStar
Auto formalization of the CLRS text book

F* · 40 stars
pulse
The Pulse separation logic DSL for F*

36 stars
fstar-vscode-assistant
An interactive mode for F* in VS Code

TypeScript · 27 stars
VimFStar
A Vim mode for FStar

Vim Script · 26 stars
kuiper
GPU kernel verification with Pulse

F* · 14 stars
pal
Proof Annotation Language: inline Pulse annotations for C

Rust · 11 stars
fstar-layer
Spacemacs layer for fstar (wrapper for fstar-mode.el)

Emacs Lisp · 10 stars
pulse-verified-gc
Verified garbage collectors in Pulse

F* · 9 stars
fstarlang.github.io
The website of all things F*

HTML · 8 stars
fstar_dataset

Python · 2 stars

Open All

Consistency with proof general? Open

FStarLang/fstar-layer#1 · 5 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Dash package doesn't get installed Open

FStarLang/fstar-layer#8 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Don't start the fstar process unless user starts interactive verification Open

FStarLang/VimFStar#14 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Opening a FStar file raises an exception Open

FStarLang/VimFStar#15 · 2 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
--ide support? Open

FStarLang/VimFStar#16 · 2 comments · 1 reaction · 0 assignees · Indexed Sep 16, 2026
Syntax highlighting is wrong for comments Open

FStarLang/VimFStar#17 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
module syntax line not correctly ended Open

FStarLang/VimFStar#19 · 2 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
I don't use Windows, but interactive still returns Busy for me Open

FStarLang/VimFStar#22 · 2 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Should support Python 3, not (just) Python 2 Open

FStarLang/VimFStar#23 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Archival of Repository Open

FStarLang/VimFStar#24 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Tactic blocks are desugared Open

FStarLang/fstar_dataset#2 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Multiple `(decreases ...)` clauses Open

FStarLang/fstar_dataset#6 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
"Could not find source file named dummy" Open

FStarLang/fstar_dataset#8 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Automatically generated `val` sigelt does not elaborate Open

FStarLang/fstar_dataset#9 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Provenance information Open

FStarLang/fstar_dataset#11 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Licensing information Open

FStarLang/fstar_dataset#12 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Flag for definitions with subsingleton types Open

FStarLang/fstar_dataset#13 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Training/validation/test split Open

FStarLang/fstar_dataset#14 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Classification of easy/hard problems Open

FStarLang/fstar_dataset#15 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Clarify duplicate definitions Open

FStarLang/fstar_dataset#16 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Some files are not built with checked files Open

FStarLang/fstar_dataset#17 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Include source text for types/etc. Open

FStarLang/fstar_dataset#19 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Check whole solutions Open

FStarLang/fstar_dataset#20 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Automatic case splits Open

FStarLang/fstar-mode.el#58 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Advancing does not recognize [@"substitute"] qualifier Open

FStarLang/fstar-mode.el#64 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Collapsing computationally irrelevant code Open

FStarLang/fstar-mode.el#72 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
JSON decoding warnings Open

FStarLang/fstar-mode.el#81 · 22 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Ability to use "fstar --indent" Open

FStarLang/fstar-mode.el#84 · 6 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Too much RAM and CPU usage when printing semi-large goals Open

FStarLang/fstar-mode.el#94 · 4 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
F* over TRAMP crashes Open

FStarLang/fstar-mode.el#102 · 17 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
fstar-jump-to-definition on a module should jump to the fsti if it exists Open

enhancement

FStarLang/fstar-mode.el#107 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Cleanup of compiler hacking subp-prover args in fstar-mode.el Open

FStarLang/fstar-mode.el#113 · 6 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
fslit seems to no longer work very well Open

FStarLang/fstar-mode.el#117 · 6 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Weird display of the highlighted blocks Open

FStarLang/fstar-mode.el#124 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
c-c c-v verify should ask to save the current file Open

FStarLang/fstar-mode.el#129 · 5 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
fstar literate setup problems on Ubuntu 22.04 and emacs 28 Open

FStarLang/fstar-mode.el#130 · 4 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Not all errors going to *Flycheck errors* Open

FStarLang/fstar-mode.el#131 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
c-c c-r reload better description Open

FStarLang/fstar-mode.el#133 · 3 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
elaborate trace mode Open

FStarLang/fstar-mode.el#134 · 2 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
F* Mode does not accept empty lines between attributes and functions Open

FStarLang/fstar-mode.el#141 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Icons not showing on menu Open

FStarLang/fstar-mode.el#144 · 5 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
KreMLin user manual: "Indices and tables" links in the ToC blank or broken Open

FStarLang/fstarlang.github.io#2 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Library docmenation appears to be broken Open

FStarLang/fstarlang.github.io#8 · 4 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Long tap does not work in tutorial Open

FStarLang/fstarlang.github.io#18 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Definition on `length` incorrect in one spot Open

FStarLang/fstarlang.github.io#25 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Outline is empty Open

FStarLang/fstar-vscode-assistant#10 · 1 comment · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Error jumping between two locations Open

FStarLang/fstar-vscode-assistant#14 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Formatter moves `in` into comments Open

FStarLang/fstar-vscode-assistant#15 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Remove fragmentation code and tests that handle reordering Open

FStarLang/fstar-vscode-assistant#25 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026
Add LSP-level tests Open

FStarLang/fstar-vscode-assistant#26 · 0 comments · 0 reactions · 0 assignees · Indexed Sep 16, 2026

Showing the newest 100

This page lists what was indexed most recently. Advanced filter has the whole inventory, narrowed by language, difficulty and how long a task takes.

Open advanced filter

FStarLang

Showing the newest 100

Get new issues in your inbox