Isabelle Alternatives

Apps similar to Isabelle include Lean Programming Language, which is free and open source. Other options are F*, Rocq Prover and Agda. In total there are four Programming Languages like Isabelle for Mac, Windows, Linux and the web.

More about Isabelle

Add Alternatives

Isabelle alternatives page was last updated Jul 6, 2026

Lean Programming Language
1 like
Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.
Cost / License
Free
Open Source (Apache-2.0)
Application type
Programming Language
Origin
United States
Platforms
Visual Studio Code
United States
Good alternative?Is this a good alternative to Isabelle?
F*
3 likes
F* is an ML-like functional programming language aimed at program verification. F* can express precise specifications for programs, including functional correctness properties. Programs written in F* can be translated to OCaml or F# for execution.
Cost / License
Free
Open Source
Application type
Programming Language
Platforms
Mac
Windows
Linux
Online
Good alternative?Is F* a good alternative to Isabelle?
Rocq Prover
4 likes
A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming language for mechanised reasoning in mathematics, computer science and more.
Cost / License
Free
Open Source (LGPL-2.1)
Application type
Programming Language
Origin
France
EU
Platforms
Mac
Windows
Linux
France
EU
Good alternative?Is Rocq Prover a good alternative to Isabelle?
Agda
2 likes
Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs...
Cost / License
Free
Open Source
Application type
Programming Language
Platforms
Mac
Windows
Linux
Good alternative?Is Agda a good alternative to Isabelle?