FStar Alternatives

FStar reviews and mentions

• F*: A general-purpose proof-oriented programming language
  4 projects | news.ycombinator.com | 2 Aug 2026

  > Ok, what kinds of problems are they?

  > And ideally - what does a simple solution look like in F-star?

  RTFM

  Or to explicate on this point: find a section in the table of contents that looks interesting to you, go to the respective section, and look at a code example.

  > Set me on the path to installing the thing (ideally above the fold)

  How to install this thing:

  1. Read https://fstar-lang.org/index.html#download

  2. Go to the GitHub page linked there: https://github.com/fstarlang/fstar/releases

  3. Download F* for an operating system of your choice there.

• Are We Stuck with Lean?
  8 projects | news.ycombinator.com | 30 Jul 2026

  Recent posts on formal proofs usually talk about Lean, Rocq, Isabelle and (due to this post) Metamath.

  What do people think of F* [1]? At least, for non-mathematics projects, doesn't it seem to be a more appropriate option [2]? It seems even the CS community is gravitating towards Lean.

  [1] https://fstar-lang.org/

• F* file system – file search that reads SSD directly bypassing OS kernel
  4 projects | news.ycombinator.com | 21 Jun 2026

  Saw the name and was disappointed that this wasn't some kind of verified file system written in the F* programming language (https://fstar-lang.org).

  I don't think I'd ever trust or use this, but still, good job OP :)

• Ask HN: Memory-Safe Low Level Languages
  13 projects | news.ycombinator.com | 27 Apr 2025

  F-star, which was used to build a verified TLS implementation. https://fstar-lang.org/ Though I guess that's actually on the far side of Rust relative to what you're looking for.

• 15,000 lines of verified cryptography now in Python
  9 projects | news.ycombinator.com | 18 Apr 2025

  The 15k lines of C are generated. The implementations are written in (and formally verified using) F, and then the C is generated from the F code using KaRaMeL.

  One should be able to trust the proofs of correctness and never look at (or maintain) the generated C directly.

  - https://fstar-lang.org

  - https://github.com/FStarLang/karamel

  - https://github.com/hacl-star/hacl-star

• F*: A proof oriented general purpose programming language
  5 projects | news.ycombinator.com | 25 Dec 2024
• F* – A Proof-Oriented Programming Language
  4 projects | news.ycombinator.com | 16 May 2024
• Translation of the Rust's core and alloc crates to Coq for formal verification
  3 projects | news.ycombinator.com | 15 May 2024

  wonder how much work it would be to add a rust backend to F* [https://github.com/FStarLang/FStar]

• Lean4 helped Terence Tao discover a small bug in his recent paper
  10 projects | news.ycombinator.com | 27 Oct 2023
• The Deep Link Equating Math Proofs and Computer Programs
  5 projects | news.ycombinator.com | 11 Oct 2023

  I don't think something that specific exists. There are a very large number of formal methods tools, each with different specialties / domains.

  For verification with proof assistants, [Software Foundations](https://softwarefoundations.cis.upenn.edu/) and [Concrete Semantics](http://concrete-semantics.org/) are both solid.

  For verification via model checking, you can check out [Learn TLA+](https://learntla.com/), and the more theoretical [Specifying Systems](https://lamport.azurewebsites.net/tla/book-02-08-08.pdf).

  For more theory, check out [Formal Reasoning About Programs](http://adam.chlipala.net/frap/).

  And for general projects look at [F*](https://www.fstar-lang.org/) and [Dafny](https://dafny.org/).

• A note from our sponsor - SaaSHub
  www.saashub.com | 11 Aug 2026

  SaaSHub helps you find the best software and product alternatives Learn more →