This thesis presents a formal verification of an abstract transition-system presentation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure in the Rocq proof assistant. Following Nieuwenhuis et al., SAT solving is modeled as a set of rule-based transitions between states rather than as a concrete algorithm. The thesis formalizes the syntax and semantics of propositional formulas, defines the classical and base DPLL transition systems, and proves their key metatheoretic properties. In particular, we establish correctness and completeness with respect to satisfiability, and we prove termination by showing that the transition relation is well-founded. The formalization extends the original abstract system by also including the pure literal rule. Building on the verified transition system, the thesis introduces an abstract notion of strategy and derives a terminating solver from any strategy satisfying suitable conditions. A concrete strategy is then implemented in Rocq using Equations and shown to satisfy the strategy specification. Together, these results provide a machine-checked and trustworthy core for SAT solving in Rocq and a basis for future extensions toward more advanced systems such as CDCL and DPLL(T).

https://github.com/Vlamonster/RocqSAT
Repository hosting the formalization.

https://vlamonster.github.io/RocqSAT/toc
Documentation of the formalization. ... Read more

Systems are becoming increasingly complex and traditional software testing and manual proofs cannot keep up to ensure correctness. Model checking is a method of performing formal verification of a model by exhaustively checking the state-space. NuSMV is a widely used symbolic verifier and supports three different specification languages: computational tree logic (CTL), linear temporal logic (LTL), and property specification language (PSL). While previous benchmarks on NuSMV exist, they do not detail impacts of the specification language on performance. This paper investigates when each type of logic is most suitable. We evaluate three use cases and develop specifications for them, equivalent in all languages. We analyze runtime, memory and size of the internal representation. Our results show CTL is often faster than LTL and PSL, but memory usage varies by model. CTL performs better on simple global properties or those containing 'next' or 'until' operators. In contrast, LTL and PSL perform better on nested 'global' and 'eventually' operators. LTL and PSL perform nearly identically in all metrics. Bounded Model Checking (BMC) generally outperforms Binary Decision Diagrams-based verification, however, due to the bound, BMC does not guarantee global safety. ... Read more

Model checking is a formal verification method introduced in the 1980s that remains relevant to this day. While each of the many model checking tools created over the past 40 years is well-documented in both scientific literature and technical documents, there is a lack of work comparing different model checkers with one another. In this paper, we compare the SPIN model checker with other popular model checkers, TLC and CBMC.

First, we compare the capabilities and ease of use of these model checkers through a literature review. Then, we investigate the performance of the compared tools through synthetic benchmarks. We conclude that SPIN offers better performance and ease of use than TLC when verifying models of concurrent algorithms, and that it outperforms CBMC when model checking parallel algorithms, while CBMC remains a better choice for model checking sequential programs. ... Read more

Model checking is a formal verification method that uses software to confirm a model of a system fulfills chosen properties. Systems in the TLA+ language are composed of states and transitions. The Apalache model checker for TLA+ is currently unable to reason about whether a system can take a given transition, while TLC can. This is important for verifying properties that assert that a given transition will eventually be taken if it possible. We apply a method from literature for rewriting these properties into a format Apalache accepts on three case studies, with the aim of finding improvements to the method. An equivalent rewrite is found for all cases, though requiring incremental modifications to the literature method. We find that expressions which depend on the updated values of variables after a transition must be distributed across disjunctions. We also note that expressions which depend on the results of prior expressions should be at the same or greater nesting level, and that if the system can pick from a set of new values for a variable, the value chosen must remain constant for the entire rest of the expression, also requiring indenting. From these results, we propose a general method for further research, relying on repeated additional nesting, applied whenever an expression is dependent on a previous expression's variable assignments. We leave its validation for future work. ... Read more

The C Bounded Model Checker (CBMC) is a widely used formal verification tool that operates directly on ANSI-C source code by bit-blasting straight-line programs into Boolean satisfiability (SAT) instances. While CBMC mitigates infinite state spaces by restricting loop iterations and recursion depths via a user-defined unwind bound ($k$) , the exact empirical relationship between this parameter and back-end solver complexity remains largely uncharacterized in existing literature. This paper systematically evaluates the impact of the maximum unwind depth on model checking complexity across three distinct software domains: array bounds, floating-point arithmetic, and heap manipulation. Utilizing metrics of execution runtime, memory footprint, and propositional variable/clause counts, we expose divergent complexity scaling behaviors. Our empirical results demonstrate that while simple non-looping floating-point operations scale under near-constant complexity , nested loops (e.g., Bubble Sort) incur a sharp quadratic complexity expansion ($O(k^2)$). Crucially, heap-intensive algorithms (e.g., In-Place Merge Sort and Singly-to-Doubly Linked List transformations) exhibit severe exponential state-space explosion, triggering solver timeouts at high unwinding thresholds. These findings challenge the intuition that model checking complexity mirrors a program's algorithmic time complexity , highlighting instead that structural loop layouts and memory-aliasing relationships dictate verification feasibility. Based on these insights, we provide concrete recommendations for iterative $k$-value scaling strategies to optimize bounded verification workflows. ... Read more

Model checking is a formal verification technique that can be used to ensure correctness of software systems. mCRL2 is a specification language with an accompanying toolset that can perform various operations including model checking. Modal μ-calculus is the property language used by the mCRL2 toolkit. The fixed-point operators included in modal μ-calculus allow it to express inductive properties. These operators give modal μ-calculus very high expressivity, allowing it to encompass other temporal logics such as LTL, CTL, and CTL*. However, this expressivity comes with some downsides as modal μ-calculus formulae can be hard to understand and take more time to verify compared to less expressive logics. In this study we compare the use of fixed-point operators to the use of helper functions for expressing three properties in a case study based on four distance-vector routing protocols. We find that the properties expressed using fixed-point operators were more performant in terms of verification time. We also found that fixed-point operators lead to larger logic expressions but smaller overall expressions when taking the size of the helper functions into account. Furthermore, we conclude that fixed-point operators can be better suited for people experienced with them, while helper functions can be better suited for the average programmer, at least for this type of task.
... Read more

A display map category, originally just called a class of display maps with a stability condition, can be used to model dependent type theory. There are several other constructions on categories that can serve a similar purpose, such as comprehension categories. In fact, the similarity of such concept has been well-known, and there even have been comparisons made using bicategories of such categorical notions.
In this thesis, I aim to formalise one such comparison, and implement it in a proof assistant. In order to do this, I needed to formalise display map categories, some related concepts, to then construct their bicategory, and show the comparison as a pseudofunctor into the bicategory of comprehension categories. The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library.
... Read more

Formal verification of software can provide a more rigorous guarantee of correctness compared to conventional software testing methods. However, doing this by hand requires substantial effort and is often impractical. To combat this, various verification tools have been developed in recent decades to at least partially automate this process. In this paper we explore Why3, a tool for deductive program verification, by implementing and verifying the A* algorithm. We find that Why3's expressive language allows for easy implementation and verification of A*. However, we also find that it has a significant learning curve and requires some knowledge on formal verification to use. In spite of this, we find it is a useful tool for automated verification. ... Read more

Formal verification promises stronger correctness guarantees than conventional testing, yet it is often perceived as too costly or specialised for everyday software development. This thesis investigates whether SPARK — Ada’s provable subset — can deliver industrial- strength verification for representative algorithms and concurrent systems. Two separate questions guided the work: how well does SPARK work with (RQ1) sequential algorithms; and (RQ2) concurrent systems.
We implemented and formally proved insertion sort, quick-sort, and a generic statically-allocated hash-map to SPARK’s highest assurance level, achieving full functional correctness, as well as two concurrent case studies: a Publisher / Subscriber channel and a novel IO multi-reactor pattern runtime task scheduler, where we combined SPARK with TLA+ model checking to capture liveness and safety properties that SPARK cannot express directly. Across all sequential examples, proof overhead averaged ratios of 6–10 lines of specification, while for the concurrent case-studies, the TLA+ models averaged ratios of 1.7 lines, per every line of executable code.
The study shows that (i) SPARK is practical for non-trivial sequential algorithms, unless they make use of the heap; (ii) concurrency still requires external formalisms, but the combination remains tractable; and (iii) careful specification design, not solver performance, is the dominant cost driver. These findings confirm that correctness-by-construction is attainable within undergraduate project scope and provide quantitative benchmarks for future work. ... Read more

Formal verification is a stricter way of ensuring correctness of a program, but sitting down and writing the proof yourself is often time-consuming. SMT solvers try to automate parts of this process. This paper aims to explore Dafny, a programming language and verifier that uses an SMT solver underneath to do this verification. This paper will go over its logical foundations, and how it can be used to verify an in-place selection sort algorithm as well as a key-value store. It will also explore a feature of Dafny that allows the user to compile to other languages, and will discuss its usefulness in the industry. Verifying the sorting algorithm was very straightforward while the key-value store posed some problems. However, Dafny itself seems to be very straightforward to program in. Its ability to compile to other languages leaves a lot to be desired. While the compiled code is fully functional, the code is barely readable and less than ideal to work with. A further study discussing Dafny’s ease of use compared to other tools could be conducted to see if the lacking compiler could outweigh having a native verifier specifically designed for a high-level programming language. ... Read more

KeY prover has been used to verify parts of the OpenJDK library and Norwegian election software, making it one of the most capable tools for formally verifying Java programs. However, an intuitive explanation of its theoretical foundations, capabilities and limitations is not available and the tool itself has a steep learning curve. This greatly increases the amount of effort to understand the tool sufficiently well to evaluate its suitability for ones needs. Here we implement two case studies to develop an intuition for the working of the tool in practice, exploring what properties can or cannot be expressed as specifications and what verifying correctness with KeY means. We find that the learning curve for KeY is even steeper than expected and conclude that it can be used to verify very complex functional and even some non-functional properties of sequential Java 7 code, conditioned on the capabilities of the user. ... Read more

Formal software verification is an important task for ensuring software correctness, especially in safety-critical systems. One method of formal verification is automated theorem proving, where one defines their program as a set of axioms and its correctness criteria as conjectures. We investigated the suitability of Vampire, an automated theorem prover, for formal verification by analyzing the logical foundations and performing case studies. In these case studies, we implemented Selection Sort and a Key-Value Store to observe what could be represented and proven. We were unable to prove the correctness of Selection Sort, but were able to prove most properties of a Key-Value Store. We discuss the capabilities and limitations of Vampire for formal software verification, namely that it is able to prove many properties of the functions we defined, unless they are heavily reliant on inductive definitions or too general with respect to the axioms. We believe that Vampire's inductive capabilities are currently insufficient for our use case. We reflect on the experience of using Vampire from the perspective of the average computer scientist and give suggestions for further documentation. We then discuss related work, including using Isabelle, another ATP and proof assistant, to reason about sorting algorithms and a Key-Value Store. Finally, we give suggestions for future work, such as rewriting the Key-Value Store in SMT-LIB, a language used as input for SMT solvers. ... Read more

Denotational semantics of type theories provide a framework for understanding and reasoning about type theories and the behaviour of programs and proofs. In particular, it is important to study what can and can not be proved within Martin-Löf Type Theory (MLTT) as it is the basis of proof assistants like Agda, Lean and Coq. Many models, including a certain class of comprehension categories, full and split comprehension categories, have been studied for the semantics of dependent type theories. The motivation for this work comes from the fact that not all comprehension categories are full and split, and one expects that type theories more general than MLTT can be interpreted in a comprehension category which is not full and split.

In this thesis, we first study how MLTT is interpreted in full split comprehension categories through concrete examples. Next, we investigate type theories that can be interpreted in comprehension cat- egories which are not necessarily full and split. For this, we propose a candidate type theory for the internal language of comprehension categories by extracting a type theory from the semantics given by a general comprehension category which is not full and split. We also give an interpretation of this type theory in every comprehension category. ... Read more

The λ-calculus is a versatile tool both in mathematical logic and computer science. This thesis studies and expands upon Martin Hyland’s paper ‘Classical lambda calculus in modern dress’. It gives examples for the definitions and provides more detailed proofs, as well as one new proof for Hyland’s fundamental theorem of the λ-calculus. It complements these definitions and proofs with material of previous authors by which Hyland has been inspired. The thesis translates Hyland’s paper from set theory with classical logic to univalent foundations, and showcases where subtleties arise in such a translation. In particular, it discusses the different implementations of the Karoubi envelope in univalent foundations. Lastly, it discusses the accompanying formalization of parts of Hyland’s paper, with in particular a tactic that was developed for applying β-reduction and substitution to λ-terms. ... Read more

To address the challenge of the time-consuming nature of proofreading proofs, computer proof assistants—such as the Coq proof assistant—have been developed. The Univalent Mathematics project aims to formalise mathematics using the Coq proof assistant from a univalent perspective, which is based on homotopy type theory.

The Symmetry book is a textbook about symmetries in mathematics written from a univalent viewpoint. This paper focuses on formalising the proofs in chapter 3 of the Symmetry book using the UniMath Coq library. Currently, the book is partly formalised in the Agda UniMath library. In this paper, we aim to formalise the chapter using the UniMath Coq library to verify its correctness. We have successfully formalised all the theorems in sections 3.1 to 3.3, along some other minor proofs. ... Read more

This paper will give a formalisation of proofs, given in the paper "isomorphism is equality", in the proof assistant language Coq. The formalisations will be added to UniMath library. A library containing machine readable proofs in the mathematical field of Homotopy Type theory, a relatively new field which combines Homotopy Theory and Martin-Löf Type Theory. The proofs that have been formalised are the equality pair lemma and the proof that isomorphism is equivalent to equality. We have also constructed a concrete universe on which we defined a notion of isomorphism, as per the same paper. ... Read more

This paper focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type Theory. This paper addresses that issue and introduces higher inductive types to UniMath. This is used to develop a computer-checked implementation of the proofs within "Finite Sets in Homotopy Type Theory." This implementation enables future research on finite sets in HoTT by providing accessible and reliable proofs.

This paper defines finite sets as Kuratowski-finite. This is in contrast with the most common notion of finiteness, e.g. Bishop-finite and enumerated types. I argue that Kuratowski-finiteness is the most general finite for which the usual operations of finite types and sub-objects can be operated upon. ... Read more

Existing implementations of category theory for proof assistants aim to be as generic as possible in order to be reusable and extensible, often at the expense of readability and clarity. We present a (partial) formalisation of category theory in the proof assistant Lean limited in purpose to explaining currying, intended to be faithful to the language and definitions used in mathematics literature. We also present some design features of our library and contrast the extent and educational merit with other implementations. ... Read more

Category theory is a branch of abstract mathematics that aims to give a high-level overview of relations between objects. Proof assistants are tools that aid in verifying the correctness of mathematical proofs. To reason about category theory using such assistants, fundamental notions have to be defined. Computer-checked libraries contain all relevant structures and theorems in an accessible way for end users. However, current libraries of category theory are not welcoming to people without in-depth domain knowledge. This paper introduces a library of category theory tailored towards newcomers to the field as well as the learning journey of the authors. We describe the project’s structure, design choices and provide examples of the main features. Moreover, a detailed overview is provided of F-algebras and their relation with inductive data types found in functional programming languages. Construction and evaluation of types like lists and binary trees can be defined in terms of algebras. They provide a general framework for recursion over these types which allow us to reason about them with simple functions. ... Read more

Category theory is a branch of mathematics that is used to abstract and generalize other mathematical concepts. Its core idea is to take the emphasis off the details of the elements of these concepts and put it on the relationships between them instead. The elements can then be characterized in terms of their relationships using various universal properties. The goal of this project was to implement a pedagogical library of category theory in the computer proof assistant Lean, a software tool for formalizing mathematics, and provide a different perspective on various functional programming concepts by finding parallels between them and the universal properties of category theory. ... Read more