The next anticipated release after Isabelle2025-1 (December 2025) will be Isabelle2026 (October 2026). The hot phase of the release is presently scheduled for 14-Sep-2026..19-Oct-2026. The detailed plan is as follows:
17-Aug-2026: Isabelle2026-RC0 as informal preview
14-Sep-2026: Isabelle2026-RC1 as first formal release candidate
28-Sep-2026: fork of the isabelle-dev vs. isabelle-release repository
19-Oct-2026: final and unchangeable Isabelle2026 release
Important: Contributors need to have things ready for RC1, with a second chance until the repository fork. There need to be several weeks left to consolidate everything, before the release becomes final and unchangable (until the subsequent release).
Isabelle/Pure was originally introduced by Paulson (1986/1989) as a Logical Framework to specify object-logics declaratively, based on Higher-order Natural Deduction. Isabelle/HOL emerged soon as main object-logic and Isabelle application, with many tools for specifications and proofs written in Isabelle/ML.
Isabelle/Isar was added by Wenzel (1999) as a structured language for Human-readable formal proof documents: it works with Isabelle/Pure and regular object-logics. The proof language has been reworked over the decades, with notable extensions in 2015/2016, including the Eisbach language for Isar Proof Methods. Already, from the beginning, Isar had been accompanied by the Isabelle Document language, to write mathematical texts with high-quality typesetting in LaTeX.
So today we may see Isabelle as an agglomeration of many languages for different purposes, all integrated into a single System Framework in Isabelle/Scala. That includes the Isabelle/PIDE Prover IDE with parallel and asynchronous processing of formal documents, and the Isabelle build system (with its distributed cluster manager). Thus we can carry the weight and gravity of large proof documents, as e.g. seen in the Archive of Formal Proofs (AFP).
The official Isabelle2025-1 release is scheduled for mid December 2025. This blog entry is dynamically updated to follow the sequence of public release candidates.
Isabelle2025-1-RC1 (05-Nov-2025): first official release candidate, approx. 6 weeks before final lift-off. Almost everything is ready for testing; some documentation and add-on components still require updates. See also AFP/695d78dfa92a.
Isabelle2025-1-RC2 (19-Nov-2025): consolidated release candidate, ready for further testing and early applications. Some documentation still requires updates, and a few open problems remain. See also AFP/28b3dacf4cf9. Notable changes between RC1 and RC2:
Include Isabelle/Naproche component (with Intro.thy in the Documentation panel of Isabelle/jEdit).
Minor updates of a few Isabelle components: pdfjs, prismjs, sqlite, and jcef (omitted in the distribution).
Minor update of veriT executables: unchanged version, new arm64-darwin executable, rebuilt x64_84-darwin executable (macOS 12), replaced x86_64-windows executable (official download).
Isabelle/jEdit: more reactive mouse handling, notably on macOS.
Isabelle/jEdit: proper update of editor buffer syntax after defining new Isar commands.
Isabelle/jEdit: proper keycode names for LEFT, RIGHT, UP, DOWN.
Isabelle/jEdit: potentially more robust scrolling of initial session build progress.
Isabelle/VSCode: update of underlying vscodium component: version 1.105.17075 (September 2025).
Isabelle/VSCode: more robust session build process on console.
Isabelle/VSCode: more scalable support for theories that are loaded from the session database, e.g. HOL.List within Isabelle/HOL.
Isabelle/VSCode: avoid OCaml icons for Isabelle .ML files.
Isabelle/VSCode: uniform treatment of Isabelle symbols, using the static table provided at build time of the underlying vscodium component.
Isabelle/VSCode: fine-tuning of the underlying protocol wrt. Isabelle/Scala.
Isabelle/HOL: some clarification of command try0 with options try0_schedule and try0_default_timeout.
Isabelle/HOL: recover card_set code equation
Isabelle/HOL: minor library updates.
Isabelle/HOLCF: minor simproc update.
Isabelle/Scala: renamed “isabelle process” to “isabelle ML_process” to emphasize that it has been mostly superseded by “isabelle process_theories”, and avoid confusion with wording (“Isabelle process” refers to the Isabelle/Scala system process, not the Isabelle/ML runtime engine).
Isabelle/ML: Isabelle_Sytem.ML_process invokes “isabelle ML_process” directly from the running Isabelle/Scala process, without starting another Java Virtual Machine of the command-line tool.
Isabelle/Scala: more scalable output of JSON, e.g. for Isabelle/VSCode protocol.
Command-line tool “isabelle process_theories”: proper handling of console interrupts.
Update of Phabricator/Phorge server.
Isabelle2025-1-RC3 (01-Dec-2025): further consolidated release candidate, ready for final testing and regular applications. All known problems have been addressed. See also AFP/3af26ffddf1b. Notable changes between RC2 and RC3:
Proper PIDE markup for “theory … imports X Y Z”, relevant for Isabelle/jEdit, Isabelle/VSCode, HTML browser info.
Isabelle/jEdit: more robust mouse event handling, especially relevant for macOS with Magic Mouse. Avoid spurious text selection after jumping around in the editor (e.g. via hyperlinks).
Isabelle/jEdit: proper target offset when jumping to other buffers, e.g. in Documentation or Theories panel.
Isabelle/jEdit: update of doc jedit, new screenshots from macOS 26 using FlatLaF macOS Light.
Isabelle/VSCode: proper PIDE markup for semantic text color.
HOL: last-minute clarification of options for sledgehammer and try0.
HOL: last-minute changes to sessions HOL-Data_Structures and HOL-Library.
System: default Docker image is now based on ubuntu:24.04, instead of ubuntu:22.04.
Isabelle2025-1-RC4 (08-Dec-2025) with alternative download: pre-final release candidate, for even more testing and regular applications. See also the Archive of Formal Proofs. Notable changes between RC3 and RC4:
Poly/ML: update to version ccd3e3717f72 from branch fixes-5.9.2, which addresses a serious problem in the operation IntInf.~>> (right shift) – relevant for Isabelle/HOL code generation with SML target.
Isabelle/ML: redundant checks for IntInt.~>> to make double sure that it now works properly (to disappear before the final release).
Isabelle/jEdit: more reactive event handling for tree view in Output and Documentation, slightly different behaviour for Debugger (“Threads”).
Isabelle/jEdit: navigator records original position (mouse) before jumping via hyperlink.
Isabelle/VSCode: proper treatment of \<^bold> control symbol (editor view, symbols panel).
The next anticipated release after Isabelle2025 (March 2025) will be Isabelle2025-1 (December 2025). The hot phase of the release is presently scheduled for 03-Nov-2025..15-Dec-2025. The detailed plan is as follows:
06-Oct-2025: Isabelle2025-1-RC0 as informal preview
03-Nov-2025 Isabelle2025-1-RC1 as first formal release candidate
15-Dec-2025: final and unchangeable Isabelle2025-1 release
Important: Contributors need to have things ready for RC1 or RC2. There need to be several weeks left to consolidate everything, before the release becomes final and unchangable (until the subsequent release).
The Isabelle Workshop usually happens every second year: this time on 14-Sep-2024 in Tbilisi, Georgia, colocated with the ITP 2024 conference. The workshop website includes all papers (and some slides).
The Phorge project has succeeded Phabricator as a community fork, starting in June 2021 when the latter was “winding down” (see also https://sketis.net/2021/after-phabricator-we-phorge-it). In Dec-2023 Phorge has become sufficiently stable to consider moving the isabelle-dev service to it, using up-to-date versions of PHP and Ubuntu-Linux. Everything has been cleaned-up and reworked on our side, and we can continue this approach to self-hosting for more years to come.
At the Dagstuhl-Seminar 23401Automated mathematics: integrating proofs, algorithms and data (01..06-Oct-2023), I delivered a talk on Isabelle as System Platform for the Archive of Formal Proofs (AFP).
Abstract:
Isabelle is usually seen as an interactive proof assistant, mostly for Higher-Order Logic (HOL), but that is somehow accidental. In reality, Isabelle is a system platform for functional programming and formal proofs, with sufficient infrastructure to carry its own weight and gravity. The Archive of Formal Proofs (AFP) is the official collection of Isabelle applications that is maintained together with the base system. That poses ever growing demands on the Isabelle platform. This talk gives an overviewof Isabelle software technology, with specific focus on Programming and Scaling, e.g. distributed build clusters for AFP.
See also the slides, which contain further links to relevant materials.
Following our usual 2-years cycle, we have another Isabelle Workshop on Thu 11-Aug-2022. This will be a truly hybrid event: the organizers of the FLoC multiconference will provide local facilities at the Technion Haifa; this will include a digital projector and network connection. We will use that to provide our own virtual facilities on top, to accommodate remote participants via BigBlueButton hosted at TU Munich.
The remote organizers of the workshop, including myself, are very grateful to the few heroic colleagues who will be there in Haifa, despite these confused times of plague and war – and rather expensive conference registration.
Already in June 2021, the main author and maintainer has announced that the platform is “winding down”, i.e. no longer actively maintained – while a few updates have already appeared afterwards. From a technical standpoint, this somewhat undefined state can easily continue one more year without further worries: our self-hosted server is running well without particular problems.
Moreover, a group of Phabricator users has already started to work on the successor project, which is called “Phorge” and developed on the site we.phorge.it. So lets see how this looks like in 6–12 months, when it is time to reconsider that part of the Isabelle infrastructure.
It is good to see that small companies and smart people are able to uphold critical infrastructure, despite the market(ing) decisions by big corporations like Bitbucket.