- 1Runs onLinux, Mac, self-hosted, Windows
- 2CostsFree plan
- 3Supported formalismstheorem-proving
- 4CounterexamplesYes
- 5Proof artifactsYes
- 6Input languagesHOL higher-order logic; Standard ML
- 7Deploymentself-hosted
Overview
HOL4 is a free, interactive proof assistant for higher-order logic, with a programming environment for proving theorems and building proof tools. It supports work that combines deduction, execution, and property checking. Built-in decision procedures and theorem provers can establish many simple theorems, and an oracle mechanism can connect to external programs such as SMT and BDD engines. HOL4 supports higher-order logic and Standard ML, and can produce proof artifacts and counterexamples. It is self-hosted and listed for Linux, macOS, and Windows. A Standard ML compiler is required, with Poly/ML recommended; Moscow ML and MLTon are also supported for building tool executables. Windows installation can use Cygwin or the Windows Linux subsystem with Poly/ML. Moscow ML is another option, but the Windows guide notes that it is slower, lacks some Poly/ML libraries, and cannot run concurrent Holmake builds. HOL includes Emacs modes for syntax display and session interaction, and the installation guide links to Vim plugin documentation. Online materials include a tutorial, quick reference, FAQ, manuals, and generated indexes.
Who it is for
HOL4 suits users proving theorems or developing proof tools in higher-order logic, especially those combining deduction, execution, and property checking. New users should be ready to learn Standard ML and allow time to become comfortable with the system.
What is good
- Free software under a Modified 3-clause BSD licence
- Built-in procedures can establish many simple theorems
- Oracle mechanism can connect external SMT and BDD engines
- Documentation includes tutorials, manuals, and a FAQ
What to know first
- Requires a Standard ML compiler
- Windows setup requires an additional environment or compiler choice
- Moscow ML lacks some libraries and concurrent Holmake builds
- The install page estimates about a month to become comfortable
Verdict
HOL4 provides an interactive environment for higher-order logic proofs, with automation and connections to external tools. It is free, but installation depends on a Standard ML compiler, and the documented Windows alternatives have tradeoffs.
HOL4 plans and pricing
All plansCompared on formal verification tools
- Free plan
- Yeshol-theorem-prover.org
- Supported formalisms
- theorem-provinghol-theorem-prover.org
- Counterexamples
- Yeshol-theorem-prover.org
- Proof artifacts
- Yeshol-theorem-prover.org
- Input languages
- HOL higher-order logic; Standard MLhol-theorem-prover.org
- Deployment
- self-hostedhol-theorem-prover.org
Facts
- Purpose
- HOL is an interactive proof assistant for higher-order logic, with a programming environment for proving theorems and implementing proof tools.hol-theorem-prover.org · 7 Oct 2026
- Use cases
- HOL is described as suitable for combining deduction, execution and property checking.hol-theorem-prover.org · 7 Oct 2026
- Automation
- Built-in decision procedures and theorem provers can establish many simple theorems, and an oracle mechanism gives access to external programs such as SMT and BDD engines.hol-theorem-prover.org · 7 Oct 2026
- License
- HOL is free software released under the Modified (3-clause) BSD licence.hol-theorem-prover.org · 7 Oct 2026
- Development
- HOL is a collaborative project hosted on GitHub and welcomes code contributions via pull requests.hol-theorem-prover.org · 7 Oct 2026
- Integrations
- HOL provides Emacs modes for syntax appearance and interacting with HOL sessions, and the install guide links to documentation for a Vim plugin.hol-theorem-prover.org · 7 Oct 2026
- External tools
- HOL requires a Standard ML compiler and recommends Poly/ML; it also supports Moscow ML and MLTon for building tool executables.hol-theorem-prover.org · 7 Oct 2026
- Windows requirement
- The Windows guide requires Cygwin or the Windows Linux subsystem with Poly/ML, or describes Moscow ML as an alternative that is not recommended.hol-theorem-prover.org · 7 Oct 2026
- Windows limitation
- The Windows guide says Moscow ML runs many times slower than Poly/ML and does not support concurrent Holmake builds.hol-theorem-prover.org · 7 Oct 2026
- Documentation
- The online documentation includes a tutorial, quick reference, FAQ, manuals, and generated indexes of libraries, theories and signatures.hol-theorem-prover.org · 7 Oct 2026
- Support
- The community page offers help through the hol-info mailing list and Zulip chat, and directs bug reports and feature suggestions to GitHub issues.hol-theorem-prover.org · 7 Oct 2026
- Learning curve
- The install page says it takes an average of about a month for someone starting from scratch to become comfortable using HOL.hol-theorem-prover.org · 7 Oct 2026
- Users
- The about page names CakeML, HOL4P4, HolBA and Verifereum among projects using HOL.hol-theorem-prover.org · 7 Oct 2026
- Requirements
- HOL requires a Standard ML compiler; the installation guide recommends Poly/ML and also lists Moscow ML, with MLTon supported for building tool executables.hol-theorem-prover.org · 8 Oct 2026
- Windows support
- On Windows, the maker documents installation using Cygwin or the Microsoft Linux subsystem, and also describes a less-featured Moscow ML build for a standard Windows console.hol-theorem-prover.org · 8 Oct 2026
- Notable limitation
- The maker notes that Moscow ML HOL lacks libraries available in the Poly/ML version and does not support concurrent Holmake builds.hol-theorem-prover.org · 8 Oct 2026
Best HOL4 alternatives
See all 20
Where it ranks on Specifiction
Is HOL4 yours?
Claim it for free: prove the domain, then correct facts, plans and screenshots. An editor reviews every change.
Sources
- hol-theorem-prover.org/about· checked 7 Oct 2026
- hol-theorem-prover.org/community· checked 7 Oct 2026
- hol-theorem-prover.org/install· checked 7 Oct 2026
- hol-theorem-prover.org/win-install· checked 7 Oct 2026
- hol-theorem-prover.org/docs/trindemossen-2/· checked 7 Oct 2026