HOL4 vs Isabelle

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.

Isabelle is a free proof assistant for expressing mathematical formulas in a formal language and proving them within a logical calculus. Its main applications are formalizing mathematics and verifying properties of hardware, software, programming languages, and protocols. Isabelle/HOL provides a higher-order logic environment for large applications, with tools for reasoning, simplification, linear arithmetic, algebraic decision procedures, and access to external first-order provers through Sledgehammer. Proofs can be written in Isar, a structured language intended to be understandable to people and computers. Isabelle/HOL can generate SML, OCaml, Haskell, and Scala code from executable specifications. Isabelle/jEdit is the default interface, providing ongoing proof checking and real-time feedback; the Isabelle2025-2 release also includes Isabelle/VSCode with panels for documentation, symbols, and Sledgehammer. The distribution includes a library of verified mathematics, supplemented by the Archive of Formal Proofs. Isabelle runs on Linux, macOS, Windows, and self-hosted deployments. Its main code base is subject to BSD-style regulations. Windows lacks developer signatures and certificates and is rejected by Microsoft by default at first launch; macOS requires users to allow the unsigned application to open.