Gentzen's 1936 proof of the consistency of Peano Arithmetic was a significant result in the foundations of mathematics. We provide here a modified version of the proof, based on Gödel's reformulation, and including additional details and minor corrections which are necessary to definitively prove the well-foundedness of the cut-elimination argument in a constructive environment. All results have been verified using the Coq theorem prover. NOTE TO READERS 26 February 2026: this is a draft which we had intended to submit to the Journal of Automated Reasoning with no particular time-line in our minds as the work was completed as part of Aaron's honours project at ANU in 2023. For that reason, we have used the Springer style files. We are putting it on arxiv as there appears to be some interest in this work as indicated by a post to https://proofassistants.stackexchange.com/questions/6462/how-far-is-gentzens-consistency-proof-of-peano-arithmetic-from-being-formalized in early February 2026. The Coq code is available here: https://github.com/aarondroidbryce/Gentzen/tree/master

We encode Belnap’s basic theory of display calculi in the proof assistant Coq/Rocq version 8.18.0 and formalise the proof that Belnap’s conditions C2–C8 imply the cut-elimination theorem. Our framework allows us to formally prove meta-theoretic results such as Hilbert-completeness and derivability of explicit rules, such as cut, but also others if required. What makes our formalisation powerful is that it works entirely with an abstraction that can be instantiated to many possible logics and display calculi, although we make no attempt to precisely characterise the logics that can be properly displayed in our formalisation. For this reason, our work can be seen as a formalisation of a display calculus framework and a cut-elimination theorem for a wide range of display calculi. As examples, we apply our work to classical propositional logic (CPL), tense logic (Kt), and non-commutative non-associative Lambek calculus to obtain complete display calculi as well as formally proved cut-elimination theorems, but we believe our formalisation to be also applicable to many others. We also encoded a proof of the decidability of CPL that relies only on the structure of proofs within an additive display calculus for CPL. To our knowledge, our work is the first formalisation of a decidability result in display calculus. Moreover, all of our formal proofs are constructive as they never require the addition of the law of excluded middle in Coq’s environment (which is constructive by default), which means we were also able to extract computer programs from our proof of cut-elimination able to convert CPL/Kt/Lambek derivation trees into cut-free ones. As formal proofs are known to be significantly longer to write than usual pen-and-paper proofs, our work led to the development of a multitude of files of Coq code comprising more than 15,000 lines.

We formalise tableau procedures for the modal logics K, KT, and S4, and the modal fixpoint logic LTL, in the proof assistant Coq version 8.17.1. This involves encoding the algorithms, and formally proving their termination and their correctness, the latter boiling down to showing that they are both sound and complete with respect to the semantics of these logics. We give a quick overview of our account of S4 because most of the work had already been achieved by Wu and Goré then focus on LTL: we describe the rules of our tableau calculus and our approach to formally verify it in Coq. Unlike K and KT, these logics require checking for loops and need particular attention to build a satisfying model. Moreover, for LTL, we must also distinguish “good loops” from “bad loops” due to the presence of least and greatest fixpoint modalities. We show how we manage to implement loop-checks to ensure termination and how a model can be constructed from their tableau tree in order to prove soundness. We also demonstrate how the eventuality formulae of LTL are handled in the tableau rules and the various proofs. Such algorithms encoded in Coq can easily be modified to output a satisfying model in the case where the input is satisfiable. We use the program extraction feature of Coq to produce source code for the verified tableau procedures in OCaml and compile them to obtain actual executable programs. We then evaluate these verified programs on the standard benchmarks against other reasoners which are optimised but unverified. As expected, the results show a clear inferiority of our verified reasoners in terms of efficiency, however they still demonstrate that we can be optimistic regarding the usability of verified reasoners in practice. Wu, M., Goré, R.: Verified decision procedures for modal logics.

We investigate two approaches for extending CEGAR-tableaux with SAT-shortcuts using a previously known approach called RECAR but also a totally new approach using the modal resolution theorem prover KSP as an oracle. Our experiments using our C++ implementation CEGARBox++ of CEGAR-tableaux show that: (1) CEGARBox++ with RECAR SAT-shortcuts is not competitive (2) CEGARBox++ using KSP to provide SAT-shortcuts is superior to both CEGARBox++ and KSP, particularly on large satisfiable problems. As far as we know, this is the first effective integration of SAT, tableaux and resolution methods for modal satisfiability which performs better than its parts.

We extend the mono-modal CEGAR-tableaux of Goré and Kikkert to normal multi-modal logic K_n with global assumptions. We then extend these CEGAR-tableaux to multi-modal tense logic Kt_n without global assumptions by “compiling in” the residuation conditions between “future” and “past” modalities. Our new implementation CEGARBox++ uses C^++ and includes multiple optimisations which speed up proof-search. is the best satisfiability-checker for mono-modal tense logic Kt_1 but is not competitive for global assumptions.

Shuffles are used in electronic voting in much the same way physical ballot boxes are used in paper systems: (encrypted) ballots are input into the shuffle and (encrypted) ballots are output in a random order, thereby breaking the link between voter identities and ballots. To guarantee that no ballots are added, omitted or altered, zero-knowledge proofs, called proofs of shuffle, are used to provide publicly verifiable transcripts that prove that the outputs are a re-encrypted permutation of the inputs. The most prominent proofs of shuffle, in practice, are those due to Terelius and Wikstrom (TW), and Bayer and Groth (BG). TW is simpler whereas BG is more efficient, both in terms of bandwidth and computation. Security for the simpler (TW) proof of shuffle has already been machine-checked but several prominent vendors insist on using the more complicated BG proof of shuffle. Here, we machine-check the security of the Bayer-Groth proof of shuffle via the Coq proof-assistant. We then extract the verifier (software) required to check the transcripts produced by Bayer-Groth implementations and use it to check transcripts from the Swiss Post evoting system under development for national elections in Switzerland.

We provide a new sequent calculus that enjoys syntactic cut-elimination and strongly terminating backward proof search for the intuitionistic Strong L\"ob logic $\sf{iSL}$, an intuitionistic modal logic with a provability interpretation. A novel measure on sequents is used to prove both the termination of the naive backward proof search strategy, and the admissibility of cut in a syntactic and direct way, leading to a straightforward cut-elimination procedure. All proofs have been formalised in the interactive theorem prover Coq.

ElectionGuard is an open source set of software components and specifications from Microsoft designed to allow the modification of a number of different e-voting protocols and products to produce public evidence (transcripts) which anyone can verify. The software uses ElGamal, homomorphic tallying and sigma protocols to enable public scrutiny without adversely affecting privacy. Some components have been formally verified (machine-checked) to be free of certain software bugs but there was no formal verification of their cryptographic security. Here, we present a machine-checked proof of the verifiability guarantees of the transcripts produced according to the ElectionGuard specification. We have also extracted an executable version of the verifier specification, which we proved to be secure, and used it to verify election transcripts produced by ElectionGuard. Our results show that our implementation is of similar efficiency to existing implementations.

We present CEGAR-Tableaux, a tableaux-like method for propositional modal logics utilising SAT-solvers, modal clause-learning and multiple optimisations from modal and description logic tableaux calculi. We use the standard Counter-example Guided Abstract Refinement (CEGAR) strategy for SAT-solvers to mimic a tableau-like search strategy that explores a rooted tree-model with the classical propositional logic part of each Kripke world evaluated using a SAT-solver. Unlike modal SAT-solvers and modal resolution methods, we do not explicitly represent the accessibility relation but track it implicitly via recursion. By using “satisfiability under unit assumptions”, we can iterate rather than “backtrack” over the satisfiable diamonds at the same modal level (context) of the tree model with one SAT-solver. By keeping modal contexts separate from one another, we add further refinements for reflexivity and transitivity which manipulate modal contexts once only. Our solver CEGARBox is, overall, the best for modal logics K, KT and S4 over the standard benchmarks, sometimes by orders of magnitude.

. The BeleniosVS electronic voting scheme offers an attractive mix of verifiability and privacy properties. Moreover, using the ProVerif protocol-verification tool, BeleniosVS has automatic machine-aided analysis of (end-to-end) verifiability in 96 different threat models with the machine-aided analysis finding proofs in 22 cases and finding attacks in the remaining 74 cases. The high number of threat models covered by ProVerif delivers a much richer security analysis than the norm. We revisit the BeleniosVS scheme and propose several refinements to the ProVerif security model and scheme which increase the number of threat models in which the scheme has verifiability from 22 to 28. Our new ProVerif security model also implies end-to-end verifiability but the requirements are easier to satisfy. Interestingly, in all six improvements, both the changes to the security model and one or more changes to the scheme are necessary to prove verifiability.

We port Dawson and Goré’s general framework of deep embeddings of derivability from Isabelle to Coq. By using lists instead of multisets to encode sequents, we enable the encoding of genuinely substructural logics in which some combination of exchange, weakening and contraction are not admissible. We then show how to extend the framework to encode the linear nested sequent calculus \(\mathsf {LNS}_\mathsf {Kt}\) of Goré and Lellmann for the tense logic \(\mathsf {Kt}\) and prove cut-elimination and all required proof-theoretic theorems in Coq, based on their pen-and-paper proofs. Finally, we extract the proof of the cut-elimination theorem to obtain a formally verified Haskell program that produces cut-free derivations from those with cut. We believe it is the first published formally verified computer program for eliminating cuts in any proof calculus.

Verifiable mix nets, and specifically proofs of (correct) shuffle, are a fundamental building block in numerous applications: these zero-knowledge proofs allow the prover to produce a public transcript which can be perused by the verifier to confirm the purported shuffle. They are particularly vital to verifiable electronic voting, where they underpin almost all voting schemes with non-trivial tallying methods. These complicated pieces of cryptography are a prime location for critical errors which might allow undetected modification of the outcome.The best solution to preventing these errors is to machine-check the cryptographic properties of the design and implementation of the mix net. Particularly crucial for the integrity of the outcome is the soundness of the design and implementation of the verifier (software). Unfortunately, several different encryption schemes are used in many different slight variations which makes it infeasible to machine-check every single case individually. However, a particular optimised variant of the Terelius-Wikström mix net is, and has been, widely deployed in elections including national elections in Norway, Estonia and Switzerland, albeit with many slight variations and several different encryption schemes.In this work, we develop the logical theory and formal methods tools to machine-check the design and implementation of all these variants of Terelius-Wikström mix nets, for all the different encryption schemes used; resulting in provably correct mix nets for all these different variations. We do this carefully to ensure that we can extract a formally verified implementation of the verifier (software) which is compatible with existing deployed implementations of the Terelius-Wikström mix net. This gives us provably correct implementations of the verifiers for more than half of the national elections which have used verifiable mix nets.Our implementation of a proof of correct shuffle is the first to be machine-checked to be cryptographically correct and able to verify proof transcripts from national elections. We demonstrate the practicality of our implementation by verifying transcripts produced by the Verificatum mix net system and the CHVote e-voting system from Switzerland.

Recently, Brighton gave another cut-admissibility proof for the standard set-based sequent calculus GLS for modal provability logic GL. One of the two induction measures that Brighton uses is novel: the maximum height of regress trees in an auxiliary calculus called RGL. Tautology elimination is established rather than direct cut-admissibility, and at some points the input derivation appears to be ignored in favour of a derivation obtained by backward proof-search. By formalising the GLS calculus and the proofs in Coq, we show that: (1) the use of the novel measure is problematic under the usual interpretation of the Gentzen comma as set union, and a multiset-based sequent calculus provides a more natural formulation; (2) the detour through tautology elimination is unnecessary; and (3) we can use the same induction argument without regress trees to obtain a direct proof of cut-admissibility that is faithful to the input derivation.

N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study.

Theorem Proving for Modal Logic has traditionally been done with semantic tableaux methods. We are nearing the limit for speed when it comes to these methods. For classical propositional logic, theorem provers using SAT solvers are very efficient. We introduce a method for Modal Logic which incorporates a SAT solver for a speed increase. As a code base we use a state of the art theorem prover for intuitionistic logic, IntSAT, by Claessen and Rosen. We yield good preliminary results and see that there is a lot of room for improvement.

N-PAT is a new model-checking tool that supports the verification of nested-models, i.e. models whose behaviour depends on the results of verification tasks. In this paper, we describe its operation and discuss mechanisms that are tailored to the efficient verification of nested-models. Further, we motivate the advantages of N-PAT over traditional model-checking tools through a network security case study.

As anyone who reads the literature on bi-intuitionistic logic will know, the numerous papers by Cecylia Rauszer are foundational but confusing. For example: these papers claim and retract various versions of the deduction theorem for bi-intuitionistic logic; they erroneously claim that the calculus is complete with respect to rooted canonical models; and they erroneously claim the admissibility of cut in her sequent calculus for this logic. Worse, authors such as Crolard, have based some of their own foundational work on these confused and confusing results and proofs. We trace this confusion to the axiomatic formalism of RBiInt in which Rauszer first characterized bi-intuitionistic logic and show that, as in modal logic, RBiInt can be interpreted as two different consequence relations. We remove this ambiguity by using generalized Hilbert calculi, which are tailored to capture consequence relations. We show that RBiInt leads to two logics, wBIL and sBIL, with different extensional and meta-level properties, and that they are, respectively, sound and strongly complete with respect to the Kripkean local and global semantic consequence relations of bi-intuitionistic logic. Finally, we explain where they were conflated by Rauszer.