# Encoding TLA+'s Set Theory for Automated Theorem Provers

Rosalie Defourné

<figure><img src="image_1.png" /></figure>

## To cite this version:

Rosalie Defourné. Encoding TLA+'s Set Theory for Automated Theorem Provers. Computer Science [cs]. Université de Lorraine, 2023. English. NNT: 2023LORR0263. tel-04408971

HAL Id: tel-04408971

https://theses.hal.science/tel-04408971

Submitted on 9 Jun 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
## Thèse

Présentée et soutenue publiquement pour l'obtention du titre de

DOCTEUR DE L'UNIVERSITE DE LORRAINE

Mention : INFORMATIQUE

par Rosalie DEFOURNE

Sous la direction de Stephan MERZ

## Encoding TLA⁺'s Set Theory for
Automated Theorem Provers

7 novembre 2023

### Membres du jury :

<table><tr><td rowspan="2">Directeur(s) de<br>thèse :</td><td>M. Stephan MERZ</td><td>Directeur de recherche, INRIA, Nancy</td></tr><tr><td>M. Pascal FONTAINE</td><td>Professeur à l'Université de Liège</td></tr><tr><td>Président de jury :</td><td>Mme Catherine DUBOIS</td><td>Professeure à l'ENSIIE, Évry-Courcouronnes</td></tr><tr><td rowspan="2">Rapporteurs :</td><td>M. David DELAHAYE</td><td>Professeur à l'Université de Montpellier</td></tr><tr><td>Mme Aurélie HURAULT</td><td>Maîtresse de conférences à l'ENSEEIHT, Toulouse</td></tr><tr><td rowspan="3">Examinateurs :</td><td>M. Jasmin BLANCHETTE</td><td>Professeur à l'Université de Munich</td></tr><tr><td>M. Guillaume BONFANTE</td><td>Maître de conférences à l'Université de Lorraine</td></tr><tr><td>Mme Chantal KELLER</td><td>Maîtresse de conférences à l'Université Paris-Saclay</td></tr></table>
Remerciements

En préambule de ce long document, je tiens à remercier les personnes qui m'ont aidée à chaque étape de mon parcours. Je remercie pour commencer Aurélie Hurault, David Delahaye, Cathe- rine Dubois, Chantal Keller et Guillaume Bonfante, pour avoir accepté d'évaluer mes travaux et ce manuscrit. Mes encadrants, Stephan Merz, Pascal Fontaine et Jasmin Blanchette, ont également lu et commenté cette thèse de multiples fois. Je veux surtout les remercier pour leurs bons conseils, leur patience à mon égard, et leur soutien dans mes moments de doute parfois terribles.

Je veux ensuite remercier les personnes qui ont partagé mon quotidien au LORIA, pour avoir su créer un environment bienveillant me permettant d'évoluer en toute confiance. Merci à Daniel et Hans-Jörg pour m'avoir accueillie mon premier jour à Nancy. Merci à Margaux et Pierre, pour leur accueil également. Merci à notre assistante d'équipe Sophie, pour son aide enthousiaste avec toutes les corvées administratives. Merci à Benjamin, Thomas et Dylan, pour m'avoir laissé la meilleure place du bureau. Merci à Marie, Sophie, Engel, Horatiu, pour les échanges à l'heure du repas, en séminaire, et aux soirées jeux. Merci à Alessio pour ses questions, qui ont ravivé mon intérêt pour TLA⁺ alors que ma thèse s'achevait. Merci à Claire et Athénaïs, pour leur soutien moral plus que bienvenu dans la dernière ligne droite.

Les dernières personnes que je veux remercier m'ont vue grandir et m'ont soutenue dans le moment le plus décisif de ma vie. Merci à ma famille, et tout particulièrement ma mère, mon père, ma sœur et mon frère, pour votre aide, votre soutien, et votre amour. Enfin, merci à Lucie. Je te remercie en dernier parce que tu es la personne la plus importante dans ma vie désormais. Merci d'avoir bien voulu la partager.
# Résumé

Cette thèse porte sur TLA⁺, un langage de spécification fondé sur la logique temporelle et la théorie des ensembles non typée. TLA⁺ est principalement utilisé dans l'industrie pour vérifier des systèmes concurrents et distribués. On s'intéresse en particulier à la preuve interactive de théorèmes TLA⁺, qui peut être réalisée avec l'outil TLAPS. Cet assistant de preuve emploie une batterie de prouveurs automatiques externes afin de vérifier les obligations de preuve qui correspondent aux étapes de raisonnement de l'utilisateur. Parmi les prouveurs disponibles, on trouve LS4 pour la logique temporelle, Isabelle/TLA⁺, Zenon, et des solveurs SMT dont CVC4, veriT et Z3.

Divers encodages de TLA⁺ sont implémentés pour que TLAPS traduise les obligations vers les logiques d'entrée de chaque prouveur. L'encodage SMT, en particulier, est fondé sur un puissant système de réécriture, complété par un mécanisme d'inférence de types, permettant à TLAPS de simplifier les obligations de façon considérable avant l'envoi vers SMT. Il est naturel de chercher à simplifier les obligations : la théorie des ensembles de TLA⁺ est bien plus expressive que la logique de SMT, qui comprend la logique du premier ordre et certaines théories, par exemple l'arithmétique des entiers. Il est possible d'encoder directement TLA⁺ en fournissant à SMT tous les axiomes qui spécifient les ensembles ; mais cette approche a auparavant été rejetée, car les axiomes sont des formules avec quantificateurs, et SMT ne peut gérer ces quantificateurs efficacement.

Néanmoins, il est important de s'assurer que les encodages de TLAPS n'introduisent pas d'erreur dans la traduction, autrement il serait possible de prouver de faux résultats avec l'outil. L'encodage SMT actuel est trop complexe pour être vérifié, nous avons donc entrepris d'implémenter l'encodage direct et naïf de TLA⁺, dans l'optique de l'optimiser ensuite. Ce travail a abouti à deux contributions. La première est l'implémentation d'un encodage vers la logique d'ordre supérieure et l'ajout d'un nouveau prouveur à TLAPS : Zipperposition. Il est intéressant de disposer d'un tel prouveur, car une petite partie des obligations en TLA⁺ impliquent des étapes d'ordre supérieur. Cela se produit particulièrement souvent autour des preuves par induction. La seconde contribution est une refonte de l'encodage SMT, cette fois basée sur l'encodage direct mais optimisée avec des heuristiques pour instancier les axiomes de la théorie des ensembles. Il s'agit de la technique des *triggers*, populaire parmi les utilisateurs de SMT, et qui nous permet en quelque sorte d'implémenter des procédures d'instanciation selon nos besoins. L'intérêt majeur des *triggers* pour notre approche est qu'ils s'ajoutent à la traduction directe sans en modifier le sens, donc sans compromettre la sûreté de l'encodage. De façon assez surprenante, notre encodage mène à des résultats aussi bons que le précédent.
Abstract

This thesis is about TLA$^{+}$, a specification language based on temporal logic and untyped set
theory. TLA$^{+}$ is mainly used in the industry for the verification of concurrent and distributed
systems. We focus on interactive theorem proving in the context of TLA$^{+}$, which is supported
by the proof assistant TLAPS. This system manages the proof obligations that correspond
to each step of the user’s reasoning, and calls different backend automated provers to check
these obligations. Currently the provers available are LS4 for the temporal fragment of the
logic, Isabelle/TLA$^{+}$, Zenon, and the SMT solvers CVC4, veriT and Z3.

All TLA⁺ obligations are encoded into the respective logics of the backend solvers by TLAPS. The SMT encoding, notably, combines a powerful preprocessing phase with type inference, simplifying obligations in an attempt to remove the TLA⁺ primitive symbols with no counterpart in SMT’s language. It is natural to perform these simplifications, as TLA⁺’s set theory is much more expressive than what SMT is designed for, which is first-order logic with theories such as integer arithmetic. In principle, one could encode TLA⁺ directly by inserting the necessary axioms of set theory into the SMT problem. This approach was discarded in favor of preprocessing because SMT solvers do not cope well with quantified formulas, and the axiomatic theory of TLA⁺ involves many of them.

Regardless, we must ensure that TLAPS does not encode invalid TLA⁺ obligations as
valid problems, otherwise one would be able to prove faulty statements unknowingly. Un-
fortunately, the current version of the SMT encoding is too complex to be verified, which
is why we decided to implement the naive, direct encoding of TLA⁺, as a basis for future
optimizations. This work has lead to two important contributions. The first is an encoding
into higher-order logic, completed by the addition of a new backend for TLAPS: Zipperposi-
tion. A higher-order backend is a worthy addition to the system, because specific situations,
in particular around induction, require higher-order reasoning to be carried out. The second
contribution is a new version of the SMT encoding. This version extends the direct encoding
with heuristics for instantiating the axioms of set theory. More precisely, we annotated our
axioms with *triggers*. Triggers are a popular feature of SMT solvers that allow users to guide
the instantiation module of the solvers for custom axiomatizations. They allow us to extend
the encoding without compromising its soundness, as they do not alter the semantics of for-
mulas. Surprisingly, our encoding achieves performances comparable to the previous version,
despite its simpler design.
# Résumé étendu

## Introduction

Cette thèse porte sur le langage de spécification TLA⁺ et son assistant de preuve TLAPS, qui utilise des prouveurs externes pour automatiser la vérification de théorèmes mathématiques. Notre objectif est d'améliorer l'automatisation apportée par TLAPS en intervenant au niveau des encodages de TLA⁺ pour les prouveurs.

## Preuve interactive et Preuve automatique

Nos travaux s'inscrivent dans le champ des méthodes formelles, dont l'objectif général est la vérification des programmes informatiques. Tout développeur veut pouvoir s'assurer qu'il ou elle écrit du code rigoureux. Dans certains contextes, il est crucial de pouvoir garantir qu'un système ne tombera pas en panne à cause d'un bug informatique [52, 54, 58, 73]. Les méthodes formelles recouvrent plusieurs approches visant à certifier que des programmes satisfont leurs spécifications. Il ne s'agit pas de tester les programmes, mais d'apporter des preuves mathématiques qu'ils ne contiennent pas de bugs.

Le champ qui nous concerne est la preuve interactive, plus particulièrement dans le contexte du langage TLA⁺. Ce langage de spécification permet à l'utilisateur de modéliser des systèmes par des formules mathématiques [48, 51, 85]. TLA⁺ a de nombreux points communs avec d'autres langages de spécification comme la Notation Z ou la Méthode B [1, 2, 74]. Comme ces derniers, TLA⁺ propose la théorie des ensembles comme base théorique, et y ajoute des notions de logique temporelle pour modéliser l'évolution des systèmes au cours du temps.

Une fois un système modélisé en TLA⁺, il est possible d'exprimer ses propriétés de correction par une formule. Supposons par exemple qu'on a défini une formule temporelle *Spec* pour représenter un système. Si *n* est une variable du système, alors la formule

$$Spec \Rightarrow \Box(n \in Nat)$$

exprime le fait que *n* est un entier naturel à tout moment de l'exécution du système. Pour certifier que notre système vérifie la propriété, il suffit de démontrer cette formule comme n'importe quel théorème mathématique. TLA⁺ propose une syntaxe pour écrire des preuves, qui peuvent ensuite être prises en charge par l'outil TLAPS.

TLAPS est un logiciel faisant partie de la famille des prouveurs interactifs, aussi appelés assistants de preuve. Ces outils associent des langages mathématiques expressifs à des procédures de vérification : l'utilisateur développe sa théorie mathématique à partir de ses propres définitions, choisit des théorèmes pour lesquels il écrit des preuves. Le rôle du système est de vérifier que chaque étape du raisonnement de l'utilisateur est logiquement valide. Comme exemples de prouveurs interactifs populaires, on peut citer Coq, qui est basé sur la théorie
des types dépendants, et Isabelle/HOL, qui est basé sur la logique d'ordre supérieur (aussi appelée théorie des types simples) [17, 60].

Le fonctionnement de TLAPS repose essentiellement sur l'emploi de prouveurs automatisque externes pour assurer la vérification [19]. Un prouveur automatique est un outil prenant en entrée des problèmes mathématiques afin de décider de leur validité—quand cela est possible, car le problème général est indécidable pour des logiques suffisamment expressives. Tous les prouveurs ne prennent pas en charge les mêmes logiques, et tous n'implémentent pas les mêmes procédures pour aboutir à une réponse. Cette thèse concerne particulièrement ce qu'on appelle les solveurs SMT (Satisfiability Modulo Theory), qui prennent en charge diverses théories de la logique du premier ordre, avec ou sans quantificateurs. La plupart des solveurs SMT acceptent le langage SMT-LIB en entrée [6, 29, 32].

Étant donnée une spécification TLA⁺ avec des preuves, l'assistant TLAPS identifie les obligations de preuve, qui correspondent à peu près aux étapes du raisonnement de l'utilisateur, et traite ces obligations pour les passer aux prouveurs externes disponibles. Ce traitement consiste essentiellement en un encodage des obligations pour chaque prouveur invoqué. Un encodage est une traduction d'une logique vers une autre. Concevoir et implémenter un encodage peut s'avérer difficile, car certains aspects de la logique d'entrée peuvent ne pas avoir d'équivalent dans la logique de sortie. En outre, pour faire confiance à TLAPS, il faut pouvoir faire confiance aux prouveurs externes d'une part, et aux encodages d'autre part.

## Encodage de TLA⁺ pour SMT

Les prouveurs de TLAPS ont des forces et des faiblesses complémentaires, et tous ne prennent pas nécessairement en charge la totalité du langage. Les différents prouveurs sont LS4—seul prouveur à supporter la logique temporelle du langage—Isabelle/TLA⁺, Zenon [11], et quelques solveurs SMT : CVC4 [5], veriT [12] et Z3 [25]. La logique de SMT est la logique du premier ordre sortée. Différentes théories incluant des symboles interprétés sont également disponibles, par exemple l'arithmétique entière. Les solveurs SMT sont réputés pour leur efficacité sur des problèmes de très grande taille. Le défi pour un encodage de TLA⁺ vers SMT-LIB est de traduire les expressions impliquant des symboles primitifs du langage, car la grande majorité n'ont pas leur équivalent en SMT. Même pour les symboles qui ont un équivalent en SMT, en particulier les opérateurs arithmétiques, la traduction directe n'est pas toujours possible puisque TLA⁺ autorise des combinaisons de symboles non conventionnelles.

Pour donner un bref exemple, on considère la formule suivante :

$$ \forall x : x + 0 = x $$

Cette formule est exprimable en TLA⁺, mais elle n'est pas valide, car il manque l'hypothèse de type $x \in Int$. Sans cette hypothèse, l'expression $x + 0$ est dite sous-spécifiée, et il n'est pas possible de la simplifier en $x$. Considérons maintenant la formule suivante en logique sortée :

$$ \forall x^{\text{int}} : x + 0 = x $$

L'annotation de sorte int indique que la variable $x$ est interprétée dans le domaine des entiers relatifs. Pour cette raison, la dernière formule est valide, car l'argument $x$ de l'addition est toujours un entier dans le contexte de l'expression.

Ce simple exemple illustre la difficulté d'encoder la logique non typée de TLA⁺ dans une logique typée : la traduction requiert d'assigner des types aux symboles et variables
quantifiées (car il faut au moins que les expressions encodées respectent les règles de typage), mais toutes les assignations ne sont pas possibles *a priori*. On dit qu'un encodage est correct si la validité d'une obligation encodée implique la validité de l'obligation source. La correction est essentielle puisqu'un encodage incorrect autoriserait la dérivation de faux théorèmes. La traduction naïve de l'exemple précédent est donc incorrecte.

Une traduction correcte possible consisterait à redéfinir l'addition de TLA⁺ dans le pro-
blème généré pour SMT. Concrètement, on peut créer une sorte $\iota$ afin d'accueillir les expres-
sions de TLA⁺, et déclarer les symboles dont on a besoin comme symboles non interprétés.
En l'occurrence, si on représente l'addition par une fonction plus binaire sur $\iota$, et 0 par une
constante zero de type $\iota$, la formule peut être traduite

$$
\forall x^i : \mathbf{plus}(x, \mathbf{zero}) = x
$$

En parallèle, les interprétations de plus et zero seront fournies par un ensemble d'axiomes
que nous ajoutons au problème encodé. Les solveurs SMT pourront alors raisonner sur ces
nouveaux symboles à partir des axiomes, qui incluent principalement la théorie des ensembles,
les fonctions, et l'arithmétique.

Cet encodage hypothétique, que l'on nomme direct, a le mérite d'être simple à implémen-
ter et prouver correct. Mais on peut a priori penser qu'il ne se montrera pas très efficace en
pratique. En effet, la présence de quantificateurs nuit grandement aux performances des sol-
veurs SMT, qui ont d'abord été conçu pour des problèmes sans quantificateurs. Or, l'encodage
direct implique d'ajouter de nombreux axiomes qui, pour la grande majorité, sont des for-
mules quantifiées. Les solveurs SMT devront déterminer quelles sont les instances nécessaires
des axiomes pour résoudre les problèmes encodés; la difficulté de cette tâche est exacerbée
par le fait que les obligations encodées ne contiennent pas d'information de typage : toutes
les variables quantifiées se voient assigner la sorte générique $\iota$.

Nos travaux poursuivent les efforts de Vanzetto, qui a conçu et implémenté l'encodage
SMT actuel de TLAPS [53]. Partant de cette constatation à propos de l'encodage direct,
Vanzetto a proposé une solution qui consiste à prétraiter les obligations afin de les simplifier.
L'objectif concret de cette simplification est d'éliminer le plus d'occurrences possible de sym-
boles primitifs de TLA⁺ afin de se ramener à la logique de SMT. L'implémentation s'articule
autour d'un module de réécriture permettant de transformer les obligations. Optionnellement,
il est possible de faire une inférence de types pour affiner la réécriture. Par exemple, la règle
suivante pourrait être appliquée pour simplifier des expressions arithmétiques :

$$
x + 0 \rightarrow x \quad \text{si } x \in \text{Int}
$$

La règle ne s'applique pas à l'exemple précédent, mais elle peut permettre de simplifier la
formule

$$
\forall x : x \in \mathbb{Int} \Rightarrow x + 0 = x
$$

Vérifier que la condition $x \in \mathbb{Int}$ est satisfaite dans le contexte de l'expression $x + 0$ relève de l'inférence de types. Une fois la règle appliquée, le but à prouver est simplement $x = x$. En admettant qu'il n'est pas possible de simplifier la formule davantage, l'encodage direct est appliqué, seulement il n'est plus nécessaire de fournir autant d'axiomes à SMT, et le problème est plus simple à résoudre.
## Contributions

L'encodage vers SMT de TLAPS est particulièrement efficace. De nombreuses obligations de preuve importantes en taille ne peuvent être résolues que par l'un des solveurs SMT intégrés à TLAPS. Toutefois, l'encodage tire son efficacité de techniques particulièrement sophistiquées, qui sont difficiles à mettre en place et à vérifier. Cela pose un problème pour la sûreté de TLAPS, car si un encodage prend en charge une partie du raisonnement—comme celui qui sous-tend la simplification des formules—alors il incombe aux développeurs de TLAPS de prouver que leur implémentation est correcte.

Cette thèse améliore l'encodage SMT du point de vue de la sûreté. En effet, notre approche consiste à partir d'une implémentation de l'encodage direct pour ensuite chercher à l'optimiser de manière prudente. Il était initialement prévu de réimplémenter la réécriture et l'inférence de types, mais une autre solution, plus satisfante en termes de correction, a été trouvée. Concrètement, on peut résumer cette thèse en deux contributions, chacune ayant abouti en une publication [27, 28] :

**L'encodage direct**, réduit au strict nécessaire, ne vise pas la logique de SMT mais la logique d'ordre supérieur. On propose un encodage direct réduit à deux étapes élémentaires, faciles à prouver correctes. L'encodage a été implementé afin d'intégrer un nouveau prouveur à TLAPS : Zipperposition [20, 82, 83]. L'intérêt d'un prouveur d'ordre supérieur est aussi d'améliorer l'automatisation de preuves qui étaient mal prises en charge auparavant.

**L'encodage SMT** étend cet encodage direct de manière minimale. Afin d'optimiser la recherche de preuves, on fournit des *heuristiques d'instantiation* pour nos axiomes à SMT. L'intérêt de cette technique est qu'elle ne nécessite pas de modifier les expressions par de la réécriture. La correction de l'encodage n'est donc pas compromise, et on a pu constater par l'évaluation que nos heuristiques permettent d'atteindre le même degré d'efficacité qu'auparavant.

Développons maintenant ces deux contributions dans l'ordre.

## Encodage direct de TLA⁺ vers HOL

Ce premier encodage est qualifié de “direct” car il maintient la structure des expressions aussi fidèlement que possible. Notre objectif global est d'étendre l'encodage direct pour les solveurs SMT. Pour des raisons qui seront clarifiées dans cette section, il est utile de définir dans un premier temps un encodage vers la logique d'ordre supérieur (HOL).

### Formalisation de TLA⁺

Avant de détailler l'encodage de TLA⁺, il faut clarifier la définition formelle du langage, c'est-à-dire donner sa syntaxe et sa sémantique. On propose une définition qui se rapproche autant que possible d'une formalisation standard de la logique du premier ordre. Le mérite de cette approche est qu'elle met en relief ce qui distingue TLA⁺ de cette logique, indiquant ainsi quels aspects du langage sont les plus difficiles à traduire.

La différence entre TLA⁺ et la logique du premier ordre tient en trois points. Le premier est la présence de symboles interprétés, principalement pour la théorie des ensembles, les fonctions
et l'arithmétique. Ces symboles sont en réalité sous-spécifiés, car le langage non typé autorise des combinaisons inhabituelles, comme $x + 0$ dans le cas où $x$ n'est pas un nombre. Il est en fait assez simple de formaliser cet aspect de TLA⁺ : au lieu de définir une interprétation pour chaque symbole, on donne la collection d'axiomes que chaque interprétation est censée satisfaire. Dire que TLA⁺ est sous-spécifié revient à dire que cette collection d'axiomes— cette théorie—n'a pas d'interprétation canonique, qu'aucune interprétation n'est plus légitime qu'une autre.

Le principe de la sous-spécification s'applique en quelque sorte aux connecteurs Booléens, mais nous choisissons de formaliser ceux-ci autrement. La principale raison est qu'il serait difficile en pratique d'encoder les connecteurs Booléens sous la forme de symboles non interprétés et de fournir des axiomes aux prouveurs ; on préférerait directement utiliser les connecteurs équivalents dans la logique de sortie. L'examen de la documentation officielle sur TLA⁺ révèle qu'il est possible de donner une interprétation totale pour chaque connecteur. Considérons par exemple l'implication, notée $\Rightarrow$. En logique traditionnelle, l'implication permet de combiner des formules, mais en TLA⁺ les arguments de $\Rightarrow$ ne sont pas des formules a priori. Par exemple, l'expression $1 + 1 \Rightarrow 2$ est légitime, mais le sens qu'il faut lui donner n'est pas clair. La bonne façon d'interpréter $\Rightarrow$ consiste à comparer la valeur de ses arguments avec la valeur de vérité "vrai" pour les évaluer en tant que formules. Notre exemple est logiquement équivalent à l'expression $(1 + 1 = \text{TRUE}) \Rightarrow (2 = \text{TRUE})$, qui est valide.

Le dernier point à souligner est la présence de symboles d'ordre supérieur, spécifiquement du second ordre. Parmi les symboles primitifs de TLA⁺, on trouve notamment les expressions $\{x \in S : e\}$ pour la compréhension ensembliste et $[x \in S \mapsto e]$ pour les fonctions. Ces deux symboles lient la variable $x$ dans l'expression $e$, on considère donc qu'elles sont paramétrées par la fonction assignant $e$ à tout $x$, représentée par la lambda-expression $\lambda x : e$. Cet aspect ne s'arrête pas aux symboles primitifs, puisque depuis la seconde version du langage l'utilisateur peut définir ses propres symboles du second ordre, qui acceptent comme arguments des symboles du premier ordre ou des lambda-expressions.

Il est facile d'étendre la logique du premier ordre pour inclure les symboles du second ordre dont TLA⁺ a besoin. Cette modification ne fait pas de TLA⁺ une logique d'ordre supérieur, car les quantificateurs universel $\forall$ et existentiel $\exists$ ne permettent pas de quantifier sur des symboles de fonctions. Cependant, comme TLA⁺ autorise le paramétrage de théorèmes par des symboles de fonction, certaines situations relèvent techniquement de l'ordre supérieur. Typiquement, une preuve par récurrence exigera d'invoquer le principe selon lequel, pour tout prédicat $P$, il suffit de prouver $P(0)$ et $\forall n \in Nat : P(n) \Rightarrow P(n + 1)$ pour dériver $\forall n \in Nat : P(n)$. L'une des étapes de la preuve consistera donc à unifier le but courant avec $P(n)$ pour déterminer la valeur de $P$, qui est une variable du second ordre.

Pour cette raison, il est intéressant de proposer un encodage vers la logique d'ordre supérieur. Parmi les prouveurs disponibles dans TLAPS, seul Isabelle/TLA⁺ est capable de traiter les obligations d'ordre supérieur. Ces obligations ne sont pas particulièrement courantes dans la pratique de TLAPS, mais elles sont inévitables dans certains contextes, et l'expérience montre que Isabelle/TLA⁺ est souvent mis en difficulté lorsque le raisonnement à l'ordre supérieur devient trop complexe.

## Définition de l'encodage direct

L'encodage direct vers HOL se résume à deux étapes essentielles : une passe sur les expressions pour corriger les ambiguïtés entre termes et formules, puis l'ajout d'axiomes au problème pour
encoder la sémantique des symboles de TLA⁺.

La première étape vise à retrouver la sémantique habituelle pour les connecteurs Booléens. Dans la logique de TLA⁺, il n'y pas de distinction entre termes et formules, mais dans la logique de sortie, les termes sont identifiés par la sorte $ι$, et les formules sont identifiées par la sorte $o$. Il s'agit d'insérer des conversions appropriées entre termes et formules de façon à obtenir des expressions bien typées. Ces conversions impliquent une injection $cast_o$ de type $o \to ι$. Convertir une formule en terme se fait en la passant en argument à $cast_o$. L'autre direction est moins intuitive, mais nous l'avons déjà illustrée avec l'exemple de $1 + 1 \Rightarrow 2$, dans laquelle deux termes apparaissent là où des formules sont attendues. Notre encodage réécrira cette expression en $(1 + 1 = \mathbf{cast}_o(\mathbf{TRUE})) \Rightarrow (2 = \mathbf{cast}_o(\mathbf{TRUE}))$.

La seconde étape insère des déclarations explicites pour chaque symbole primitif de TLA⁺ dans l'obligation. Chaque symbole se voit assigné un ou plusieurs axiomes (ou schémas d'axiomes) qui spécifient sa sémantique. Ces axiomes sont insérés dans le contexte de l'obligation avec la déclaration ; si un axiome mentionne un nouveau symbole, la procédure est répétée de façon récursive. Typiquement, chaque symbole est spécifié par un à trois axiomes. Nos axiomes sont formulés de sorte à réduire le nombre de dépendances entre symboles. Par exemple, le symbole $∩$, pour l'intersection entre deux ensembles, est spécifié par l'unique axiome

$$ \forall a, b, x : x \in (a \cap b) \Leftrightarrow x \in a \land x \in b $$

Il serait également possible de définir le symbole par la définition $a \cap b \triangleq \{x \in a : x \in b\}$, mais cela ferait dépendre $∩$ de la notation de compréhension.

Les axiomes que nous utilisons ne proviennent pas de la documentation officielle, mais on peut les inférer depuis celle-ci assez facilement. Pour résumer la théorie de TLA⁺, on peut se concentrer sur trois piliers : les ensembles, les fonctions et l'arithmétique. Les axiomes de théorie des ensembles sont standards et correspondent à ceux de la théorie ZFC. Les axiomes des fonctions spécifient le constructeur $[x \in S \mapsto e]$ et les expressions `DOMAIN f` et $f[x]$ pour récupérer le domaine d'une fonction et son image par $x$, respectivement. On trouve également le constructeur $[S \to T]$ pour les ensembles de fonctions. Une présentation complète de TLA⁺ devrait inclure les $n$-uplets, les enregistrements et les séquences, mais ces trois types de structures sont définis à partir des fonctions, et leurs axiomes sont directement conséquences de la théorie des fonctions.

À ce stade de nos travaux, nous choisissons d'ignorer l'arithmétique, pour plusieurs raisons. L'arithmétique entière est une théorie que de nombreux prouveurs prennent en charge de façon native. Plutôt que de fournir aux prouveurs nos propres axiomes pour l'arithmétique, il est naturel de chercher à exploiter les procédures natives de ces prouveurs lorsqu'elles sont disponibles. Pour notre encodage HOL, le prouveur que nous avons choisi d'intégrer à TLAPS est Zipperposition, mais la version que nous utilisons ne prend pas en charge l'arithmétique. Puisque nous envisageons Zipperposition pour une utilisation spécialisée—les obligations d'ordre supérieur—nous traitons le cas de l'arithmétique comme secondaire, et nous l'ignorons. Il y a des axiomes que nous ajoutons néanmoins, car leur omission rendrait non prouvables trop de théorèmes : chaque symbole arithmétique de TLA⁺ a un axiome qui donne son type, par exemple + a l'axiome

$$ \forall x, y \in \mathbf{Int} : (x + y) \in \mathbf{Int} $$

Nous incluons au moins ces axiomes, car ils sont assez simples et nécessaires pour beaucoup de vérifications de routine.
## Intégration de Zipperposition

Zipperposition est un prouveur par superposition pour la logique du premier ordre. Il inclut une extension à l'ordre supérieur, extension qui a permis à l'outil de gagner la compétition CASC dans la section THF. Le dialecte THF appartient au standard TPTP pour exprimer des problèmes mathématiques, et c'est vers ce langage que notre encodage direct traduit les obligations de TLA⁺.

Comme dit précédemment, l'intérêt d'un prouveur comme Zipperposition pour TLAPS est principalement de renforcer l'automatisation pour les obligations d'ordre supérieur, qui autrement sont prises en charge par Isabelle seulement. Nous avons donc comparé les performances de Zipperposition et d'Isabelle sur un ensemble assez grand d'obligations, qui englobe notamment la librairie d'exemples TLA⁺ officielle dans son entièreté. Notre évaluation démontre que les deux prouveurs se complètent assez bien, puisque certaines obligations sont résolues par Zipperposition uniquement, et d'autres par Isabelle uniquement. La principale faiblesse de Zipperposition est qu'il ne peut pas raisonner dans l'arithmétique entière, qui est souvent nécessaire. En outre, notre expérience avec Zipperposition suggère que le prouveur serait capable de résoudre des obligations plus difficiles quand du raisonnement à l'ordre supérieur est requis.

## Encodage de TLA⁺ vers SMT-LIB

L'encodage vers SMT-LIB est conçu comme une extension de l'encodage direct. L'extension se résume à trois modifications, dont seule la première est absolument nécessaire, puisqu'il s'agit d'éliminer l'ordre supérieur des obligations. Par exemple, les expressions $\{x \in S : e\}$ et $[x \in S \mapsto e]$ doivent être exprimées dans la logique du premier ordre. Il existe des procédures standards pour implémenter cette traduction, et notre approche s'inspire des méthodes de défonctionnalisation qu'utilisent les compilateurs de langages fonctionnels. Intuitivement, la méthode consiste à créer un symbole spécialisé pour chaque mention d'un symbole d'ordre supérieur présent dans l'obligation. Si par exemple une obligation mentionne l'ensemble $\{n \in Nat : n < 100\}$, il suffit de créer un symbole spécialisé pour l'argument $\lambda n : n < 100$. Ce symbole, que l'on peut noter setst•, doit être spécifié par l'axiome

$$ \forall a, x : x \in \text{setst}^\bullet(a) \Leftrightarrow x < 100 $$

L'expression d'origine peut être traduite setst•(Nat).

## Intégration de l'arithmétique SMT

La deuxième modification est essentielle pour supporter l'arithmétique entière de manière satisfaisante. Les solveurs SMT sont dotés de techniques spéciales pour raisonner sur l'arithmétique entière, et on souhaite pouvoir mettre ces techniques à profit. Cela implique d'encoder des expressions vers la sorte int de SMT, ce qui n'est pas simple a priori puisque TLA⁺ est non typé. Notre solution, qui était déjà utilisée par l'encodage précédent pour la version sans inférence de types, consiste à fournir quelques axiomes spéciaux permettant aux solveurs SMT de basculer le raisonnement dans le domaine des entiers.

Ces axiomes reposent sur un injecteur castint de type int $\to \iota$. Si $x \in \text{Int}$ est vrai, SMT pourra déduire l'existence d'un $n$ tel que $x = \text{castint}(n)$. Pour encoder ce principe, il suffit
d'ajouter cet axiome au problème final :

$$ \forall x^t : x \in \mathit{Int} \Leftrightarrow [\exists n^{\mathit{int}} : x = \mathit{cast}_{\mathit{int}}(n)] $$

En plus de cette axiome, chaque symbole arithmétique de TLA⁺ avec un symbole SMT équivalent se voit assigner un axiome pour lier les deux versions. Par exemple, nous lions le + de TLA⁺ avec le `+_int` interprété de SMT par l'axiome

$$ \forall m^{\mathit{int}}, n^{\mathit{int}} : \mathit{cast}_{\mathit{int}}(m) + \mathit{cast}_{\mathit{int}}(n) = \mathit{cast}_{\mathit{int}}(m +_{\mathit{int}} n) $$

## Heuristiques d'instantiation pour SMT

La troisième modification concerne la collection d'axiomes entière. L'encodage SMT précédent tirait son efficacité du fait qu'il simplifie grandement les expressions de TLA⁺. Notre encodage innové sur ce point en se contentant de fournir des heuristiques pour guider les procédures d'instantiation de SMT. Cette technique ne nécessite pas de simplifier les expressions, il n'y a donc aucun risque de rendre l'encodage incorrect.

La technique particulière que nous utilisons est celle des *triggers* de SMT [24, 55]. Dans le cas de problèmes avec quantificateurs, les solveurs SMT doivent générer des instances pour les formules universellement quantifiées afin de progresser. Il est difficile en pratique de déterminer quelles sont les instances importantes, et les solveurs peuvent implémenter diverses approches pour répondre à ce problème. Un *trigger* est une annotation sur une séquence de quantificateurs indiquant aux solveurs comment les instancier.

Considérons par exemple l'axiome suivant, qui spécifie l'opérateur d'intersection entre deux ensembles :

$$ \begin{array}{l} \forall a, b, x : \{x \in (a \cap b)\} \\ \phantom{\forall a, b, x : \{x \in (a \cap b)\}} \{a \cap b, x \in a\} \\ \phantom{\forall a, b, x : \{x \in (a \cap b)\}} \{a \cap b, x \in b\} \\ x \in (a \cap b) \Leftrightarrow x \in a \land x \in b \end{array} $$

Nous indiquons les *triggers* entre accolades; dans ce cas, trois *triggers* ont été choisis. Considérons le premier : le motif $x \in (a \cap b)$ indique au solveur SMT qu'il peut chercher les termes de cette forme. Lorsqu'un tel terme est détecté, l'assignation correspondante pour les variables $x$, $a$ et $b$ est utilisée pour générer l'instance de l'axiome. En l'occurrence, il s'agira de la formule qui donne la caractérisation de $x \in (a \cap b)$.

De nombreux solveurs SMT génèrent automatiquement leurs propres *triggers*, mais nous avons trouvé profitable de choisir les nôtres manuellement. Notre stratégie pour sélectionner des *triggers* repose sur l'hypothèse qu'une obligation TLA⁺ typique ne requiert pas de raisonner sur des ensembles ou fonctions qui ne sont pas mentionnées. On peut donc se contenter de récupérer le maximum d'informations sur les termes connus, et en même temps rejeter les *triggers* susceptibles d'introduire de nouveaux ensembles et fonctions, ce qui complexifierait inutilement les problèmes.

Un autre aspect de notre stratégie consiste à anticiper le plus de situations de preuve possible à l'aide de *triggers*. Dans l'exemple précédent, le premier *trigger* permet essentiellement de simplifier une proposition $x \in (a \cap b)$. Or, il est parfois nécessaire d'inférer une proposition
$x \in (a \cap b)$ sans qu'elle soit explicitement mentionnée—typiquement parce qu'elle intervient
à un niveau plus profond du raisonnement. Par exemple, la formule

$$
S \cap \mathit{Int} = \emptyset \wedge 1 \in S \Rightarrow \mathit{FALSE}
$$

est bien prouvable, mais le solveur doit en quelque sorte deviner l'étape $1 \in (S \cap Int)$ qui
permet au raisonnement d'aboutir. Les deuxième et troisième *triggers* de notre exemple sont
adaptés à cette situation, car il suffit de connaître un certain ensemble $a \cap b$ et un certain
élément $x$ de $a$ ou $b$ pour générer une instance pertinente.

Nous nous sommes efforcés d'appliquer des principes comme ceux que nous venons de
décrire de façon aussi systématique que possible pour l'ensemble de l'axiomatisation. Les
axiomes de théorie des ensembles sont traités de façon assez similaire ; certains axiomes doivent
être reformulés pour placer tous les quantificateurs au début de la formule, afin qu'ils puissent
recevoir une annotation. La théorie des fonctions de TLA⁺ inclut le constructeur $[x \in S \mapsto e]$ et, étant donné une fonction $f$, les opérateurs DOMAIN $f$ et $f[x]$ dénotant respectivement le
domaine de $f$ et l'application de $f$ à $x$. Notre stratégie s'adate bien aux axiomes spécifiant
ces symboles : nous évitons d'introduire de nouvelles fonctions, mais nous sélectionnons des
*triggers* qui permettent de récupérer des informations sur les domaines et valeurs d'application
des fonctions connues.

Évaluation de l'encodage SMT

L'évaluation comparée de notre encodage avec l'encodage précédent montre que notre ap-
proche ne mène pas à une perte d'efficacité en termes d'obligations résolues. Compte tenu du
fait que notre implémentation est plus sûre d'utilisation, on peut affirmer que notre encodage
améliore l'état de l'art, puisqu'il est moins risqué de l'utiliser.

Certaines obligations sont résolues par une version de l'encodage mais pas l'autre. Il est
toujours difficile d'expliquer la raison pour laquelle l'un des deux encodages pourrait surpas-
ser l'autre dans une situation donnée. L'approche par simplification semble parfois échouer
parce qu'elle élimine des termes tout en laissant intact des quantificateurs à instancier avec
ces mêmes termes. Notre approche par *triggers* a quelques faiblesses connues, notamment
au niveau des axiomes d'extensionnalité, pour lesquels il est difficile de sélectionner des an-
notations pertinentes. Pour l'axiome d'extensionnalité ensembliste, nous nous contentons de
générer des instances pour les égalités entre ensembles dans l'obligation initiale. Pour l'exten-
sionnalité fonctionnelle, nous générons une instance pour toute paire de fonctions, ce qui mène
à beaucoup d'instances non pertinentes dans certaines situations impliquant de nombreuses
fonctions.

Perspectives

Cette thèse a permis de rendre TLAPS plus sûr d'utilisation, mais il serait possible d'al-
ler encore plus loin dans la certification des preuves. Nous nous sommes efforcés de justifier
la correction de nos deux encodages, mais nos preuves pourraient être erronées, ou notre
implémentation pourrait contenir des erreurs. Une idée serait de chercher à certifier l'implé-
mentation de l'encodage ; un assistant de preuves comme Coq semble adapté à cette tâche. Il
s'agit toutefois d'un projet ambitieux, et une autre solution semble possible. Certains prou-
veurs automatiques permettent de récupérer une preuve lorsqu'une obligation a été prouvée.
Compte tenu du fait que notre encodage modifie assez peu les expressions, il semble possible
de traduire ces preuves dans le langage de TLA⁺ afin de les faire vérifier par un programme
de confiance. C'est ce qui est actuellement fait avec le prouveur Zenon, dont la sortie peut
être vérifiée par Isabelle/TLA⁺. Notre encodage SMT pourrait permettre de reproduire cette
fonctionnalité pour les solveurs SMT capables de produire des preuves.

Pour ce qui est d'améliorer l'encodage du point de vue de l'efficacité, la situation est moins claire. Certaines faiblesses de notre axiomatisation à base de *triggers* pourraient être corrigées, notamment au niveau des axiomes d'extensionnalité. L'axiomatisation pourrait aussi être étendue à d'autres fragments de TLA⁺. Il semble particulièrement facile d'adapter la méthode pour exploiter l'arithmétique entière de SMT à l'arithmétique réelle. Nous avons formulé une stratégie pour sélectionner des *triggers* de manière plus ou moins systématique, la question d'automatiser la génération des *triggers* se pose donc. Il serait notamment intéressant de pouvoir générer des *triggers* pour les instances des schémas d'axiomes que nous générons lors de la réduction au premier ordre.
# Contents

<table><tr><td>1</td><td>Introduction</td><td>21</td></tr><tr><td>1.1</td><td>Context</td><td>21</td></tr><tr><td>1.2</td><td>Motivation</td><td>24</td></tr><tr><td>1.3</td><td>Contributions</td><td>24</td></tr><tr><td>1.4</td><td>Outline</td><td>25</td></tr><tr><td>2</td><td>Background</td><td>27</td></tr><tr><td>2.1</td><td>Automated Theorem Proving</td><td>27</td></tr><tr><td>2.1.1</td><td>The DPLL Procedure</td><td>27</td></tr><tr><td>2.1.2</td><td>Satisfiability Modulo Theories</td><td>33</td></tr><tr><td>2.2</td><td>TLA<sup>+</sup></td><td>39</td></tr><tr><td>2.2.1</td><td>Specifying Systems</td><td>39</td></tr><tr><td>2.2.2</td><td>Model Checking with TLC</td><td>44</td></tr><tr><td>2.2.3</td><td>Interactive Proof with TLAPS</td><td>47</td></tr><tr><td>3</td><td>Formal Semantics of TLA<sup>+</sup>'s Constant Fragment</td><td>57</td></tr><tr><td>3.1</td><td>Overview</td><td>57</td></tr><tr><td>3.2</td><td>The Logic <i>L</i></td><td>58</td></tr><tr><td>3.3</td><td>The Theory of TLA<sup>+</sup></td><td>62</td></tr><tr><td>3.4</td><td>Sequents</td><td>68</td></tr><tr><td>4</td><td>A Direct Encoding of TLA<sup>+</sup> into Higher-order Logic</td><td>71</td></tr><tr><td>4.1</td><td>Overview</td><td>71</td></tr><tr><td>4.2</td><td>The Logic <i>L</i><sup>s</sup></td><td>73</td></tr><tr><td>4.3</td><td>Recovering Formulas</td><td>78</td></tr><tr><td>4.3.1</td><td>Definition</td><td>79</td></tr><tr><td>4.3.2</td><td>Correctness</td><td>81</td></tr><tr><td>4.3.3</td><td>Predicate Types</td><td>84</td></tr><tr><td>4.4</td><td>Rewriting</td><td>86</td></tr><tr><td>4.4.1</td><td>Definition and Correctness</td><td>87</td></tr><tr><td>4.4.2</td><td>Termination and Confluence</td><td>89</td></tr><tr><td>4.5</td><td>Axiomatization</td><td>94</td></tr><tr><td>4.5.1</td><td>Definition and Correctness</td><td>94</td></tr><tr><td>4.5.2</td><td>Second-order Axiomatization of TLA<sup>+</sup></td><td>95</td></tr><tr><td>4.6</td><td>Translation to TPTP</td><td>98</td></tr><tr><td>4.7</td><td>Evaluation</td><td>99</td></tr></table>
<table><tr><td>4.7.1 Methodology</td><td>99</td></tr><tr><td>4.7.2 Results and Discussion</td><td>99</td></tr><tr><td><b>5 An Optimized Encoding into First-order SMT</b></td><td><b>103</b></td></tr><tr><td>5.1 Overview</td><td>103</td></tr><tr><td>5.2 E-matching Patterns</td><td>104</td></tr><tr><td>5.3 Selecting Axioms and Triggers for TLA<sup>+</sup></td><td>107</td></tr><tr><td>5.3.1 Case Study</td><td>107</td></tr><tr><td>5.3.2 General Strategy</td><td>110</td></tr><tr><td>5.4 Other Topics in the SMT Axiomatization</td><td>116</td></tr><tr><td>5.4.1 Axiom Schemas</td><td>116</td></tr><tr><td>5.4.2 Integer Arithmetic</td><td>119</td></tr><tr><td>5.4.3 Set Extensionality</td><td>121</td></tr><tr><td>5.5 Evaluation</td><td>122</td></tr><tr><td>5.5.1 Methodology</td><td>122</td></tr><tr><td>5.5.2 Results and Discussion</td><td>122</td></tr><tr><td><b>6 Conclusion</b></td><td><b>125</b></td></tr><tr><td><b>Bibliography</b></td><td><b>136</b></td></tr><tr><td><b>A The Standard Theory of TLA<sup>+</sup></b></td><td><b>137</b></td></tr><tr><td><b>B Axioms for TPTP</b></td><td><b>145</b></td></tr><tr><td><b>C Axioms for SMT</b></td><td><b>151</b></td></tr></table>
# Chapter 1

# Introduction

This thesis presents translations of TLA⁺ formulas into the input logics of automated theorem provers. TLA⁺ is a formal language combining temporal logic and set theory, used in the industry to specify and verify computer systems [48]. We implemented our translations into TLAPS, an interactive proof system that uses backend provers to automatically verify every step of the user’s reasoning [19]. Special attention is paid to the soundness of each translation, as any mistake may compromise the integrity of TLAPS, letting users derive invalid statements with the system.

## 1.1 Context

Formal methods are a rigorous approach to the verification of software [54]. They are applied in diverse industrial fields such as avionics [73], cloud computing [58] and hardware design [33] to specify, check, and sometimes certify various systems. The methods by which programs can be verified are diverse as well and include model checking and theorem proving.

This thesis is about theorem proving in the context of TLA⁺, a specification language aimed at distributed and concurrent systems [48]. The TLA⁺ Proof System (TLAPS) is an interactive theorem prover whose purpose is to interpret proofs written in a TLA⁺ environment, generate proof obligations corresponding to each step of the user’s reasoning, and have these obligations proved by specialized automated theorem provers [19]. The logics understood by most provers are very different than TLA⁺’s, therefore translations (encodings) of TLA⁺ must be defined for the backends.

### Specification with TLA⁺

As a formal language, TLA⁺ combines the Temporal Logic of Actions (TLA) with axiomatic set theory, more precisely the ZFC theory, named after the mathematicians Zermelo and Frænkel, and the axiom of choice [47, 48, 51]. It is a purely logical language; one is expected to define different predicates describing the states and transitions of a system in an abstract way. This is illustrated in Figure 1.1, where a simple system is defined from an initial state *Init* and a transition predicate *Next*. The variable *out* is temporal: its value changes over time, and its value in the next state is denoted *out'*. The temporal formula *Spec* specifies the system as a whole. It features a temporal connective to state that, for every transition of the system, either *Next* holds or *out* does not change.
<figure><img src="image_3.png" /><figcaption>Figure 1.1: TLA⁺ Specification of the “Hello World!” program</figcaption></figure>

TLA⁺ is close to the Z notation [74], the B method and its extension Event-B [1,2], which are all specification languages based on set theory. In its classical formulation, set theory extends first-order logic (FOL) with a membership relation $\in$ and several axioms. It is a very expressive theory; in fact, it is a suitable framework for any kind of mathematics, and is largely adopted by the mathematical community. In TLA⁺, systems and their properties are expressed in the same mathematical language. For instance, the fact that *out* is a string of characters is expressed $out \in STRING$, and the fact that this property is an invariant of the system is stated

$$Spec \Rightarrow \Box (out \in STRING)$$

It is a valid temporal formula: for every trace satisfying *Spec*, the variable *out* is indeed a string in all states.

Invariants such as this one are commonly referred to as *typing invariants*. It is important to verify them, because TLA⁺ is an untyped language. This is in line with the choice of ZFC as a foundation, but unconventional in the context of computer science. In programming, statically-typed languages benefit from the fact that many type errors can be caught at compile time. In formalized mathematics, most existing systems are based on a variant of type theory. As examples, we mention Isabelle and the object logic Isabelle/HOL which are based on higher-order logic (HOL) [14, 60, 61], the proof assistant Coq which is based on dependent type theory [17, 18], and PVS which is based on predicate subtyping [67]. The Z Notation and B-Method are based on typed variants of set theory. The Mizar proof assistant takes untyped set theory as a foundation, but its syntax includes type annotations, and expressions must pass type-checking [38, 44, 84].

In a polemic article, Lamport argues in favor of untyped formalisms for specification [49]. Type systems restrict one's ability to specify things easily; rich type systems offer more expressiveness, but these languages are too complicated for non-experts to use. In contrast, it is easy to express typing conditions in untyped set theory. For instance, in ordinary mathematics, one is allowed to write

$$\forall x : x \in Real \land x \neq 0 \Rightarrow x/x = 1$$

This is a valid statement, despite the fact that it indirectly refers to nonsensical expressions, like 0/0. The legitimacy of these expressions is not an issue in an untyped framework, because the typing condition does not hold when *x* is 0. Semantically, division is treated as a totally-defined symbol, specified for some input values, unspecified for the rest [39].
### Interactive Proof with TLAPS

Once a TLA⁺ specification is written and its properties expressed, one can attempt to verify it. There are two ways to perform verification in TLA⁺. The first is model checking. The model checker TLC explores all the possible traces given by a temporal formula in an exhaustive way [85]. However, TLC is limited to specifications involving finite data and fixed parameters. For the general case, one has to write a proof and check it with TLAPS.

TLAPS is an *interactive theorem prover* (ITP), also called *proof assistant*. ITPs combine expressive mathematical languages, interactive environments for users to write proofs, and procedures that formally check every step of the user's reasoning. Proofs often involve many tedious verifications, which is why many ITPs rely on automated procedures to solve easy subgoals. Notably, there is a growing interest in integrating *automated theorem provers* (ATPs) with interactive environments. This integration comes with many challenges, as ATPs tend to specialize on particular domains of mathematical logic, and typically do not support logics as expressive as the ITPs [34]. One particularly successful application of ATPs for interactive proving is the Sledgehammer system for Isabelle/HOL, which uses relevance-filtering and an unsound encoding of HOL to quickly derive proofs for the desired goals [10,62]. CoqHammer is a similar tool for Coq, although it is more difficult to translate Coq's dependent type theory into the input logics of ATPs [22]. TLAPS is not as complex a system, but it also relies on automated backends to verify proof obligations [19]. Given a proof script written in a dialect of TLA⁺, TLAPS generates obligations corresponding to the important steps, and translates each obligation into the logics of the available backends.

Let us review the current backend provers of TLAPS. LS4 is a prover for propositional temporal logic [76]. No other backend supports temporal logic, but TLA⁺ proofs are easily structured in such a way that the temporal part of the reasoning is contained in a single obligation. The Isabelle backend uses a direct translation to the object logic Isabelle/TLA⁺ and attempts to prove obligations by using one of the basic automation tactic of Isabelle: **auto**, **force** and **blast**. Zenon is a tableaux-based prover for first-order logic [11]. One distinctive feature of the Zenon backend is that it can optionally produce detailed proofs in Isabelle's format. These proofs may then be checked automatically by Isabelle to increase trust in the proof system. Finally, the SMT backend uses an encoding into the SMT-LIB standard format for SMT solvers [6]. The SMT solvers available are CVC4 [5], veriT [12], and Z3 [25].

SMT is currently TLAPS's most efficient backend. SMT solvers are recognized for their ability to handle very large problems, and used by many ITPs to discharge the most tedious obligations [9, 29, 32]. They excel in contexts involving decidable theories of first-order logic, but do not cope well with quantifiers. The SMT encoding of TLAPS is designed with these strengths and limitations of SMT in mind [53,81]. One can start from the idea of a *direct encoding* of TLA⁺ for SMT solvers. To implement this encoding, it suffices to declare every primitive of TLA⁺ as an *uninterpreted symbol* of SMT (a symbol with no meaning attached to it), then insert axioms into the problem and translate expressions faithfully. This hypothetical encoding suffers from at least three issues. SMT solvers are first-order, but TLA⁺ includes a few second-order constructs, for example {$x \in S : P(x)$}. First-order instantiation is a difficult task for SMT solvers, which may struggle to find the relevant axiom instances. Finally, some symbols of TLA⁺ have interpreted counterparts in SMT (typically, every operator of integer arithmetic), but the direct encoding translates them as uninterpreted symbols.

These problems have been tackled through the implementation of various preprocessing techniques. The core technique is rewriting, which effectively eliminates primitive TLA⁺
symbols from the source obligation. The following rule eliminates an occurrence of $\cup$:

$$x \in (a \cup b) \rightarrow x \in a \lor x \in b$$

However, there are many situations where nonprimitive symbols occur but no rule is applicable. Rewriting is then complemented by auxiliary techniques that modify the logical structure of obligations, enabling further rewritings. Optionally, the preprocessing phase may be optimized by type synthesis. This mechanism attempts to infer types for all subexpressions and annotates expressions accordingly. This enables many optimizations of the base rewriting system:

$$x + y \xrightarrow{x \in \text{Int}, y \in \text{Int}} x +_{\text{int}} y$$

where + is TLA⁺'s untyped addition, and +_int is SMT's interpreted addition. The rule above enables a translation of $x + y$ directly as an integer term in SMT's logic.

## 1.2 Motivation

This thesis continues the work of Vanzetto on the SMT encoding of TLAPS [53,81]. We will refer to Vanzetto's implementation as the "original encoding", to distinguish it from our own work. In order to achieve good results, the original encoding relies on a complex preprocessing phase. This phase is powerful enough to actually solve some obligations before they are sent to the SMT solvers. As evidence for this, we report that, during our evaluation of the original SMT backend (which is detailed in Chapter 5), we found that for about 11% of all obligations, the goal had been reduced to TRUE during preprocessing.

While this kind of efficiency is desirable, we must also ensure that the encoding is sound. An unsound encoding may produce a valid SMT problem from an invalid TLA⁺ obligation, letting users derive faulty statements with TLAPS. If an invalid statement is proved using a particular backend, the error may result from a bug in the ATP, or an error in the translation implemented in TLAPS. Some ATPs can output proofs along with their results, so that these proofs may be checked internally by the ITP. We already mentioned Zenon, whose output can be checked by Isabelle. Let us also mention an ongoing effort to reconstruct TLA⁺ proofs from veriT's output [16, 68, 69].

However, the current SMT encoding carries an important part of the actual solving, and its output can hardly be exploited for debugging purposes, let alone proof reconstruction. Encoded proof obligations have often little in common with the source TLA⁺ obligations, leaving us with the only option to inspect the source code of TLAPS when a bug is found.

Our primary concern is to increase trust in TLAPS, especially the SMT backend. The direct encoding would be a safe alternative to the current one, since it is very easy to prove sound. But it was never implemented fully, as it was assumed too inefficient. Our starting point is the idea of using the direct encoding as a basis for a more modular design, in which preprocessing could be turned off to obtain stronger soundness guarantees. We may not expect the direct encoding to be as efficient, but it would at least let us verify a portion of the current encoding's positive results.

## 1.3 Contributions

Two contributions have been made in the form of new translations of TLA⁺ for ATPs. The first is a direct encoding of TLA⁺ into HOL. The second translation is an optimized encoding
for SMT solvers. Many assets from the first encoding are reused to implement this new SMT encoding, which will effectively replace the original one in a future version of TLAPS. Each contribution has lead to a publication in an international conference [27, 28].

The direct encoding targets HOL, so that the second-order constructs and axiom schemas of TLA⁺ can be easily encoded. To test this encoding, we added support for Zipperposition, a superposition prover that supports higher-order logic [20, 82, 83]. As we were working on this encoding, Zipperposition had just won the CASC competition in the THF division [77, 78]. Besides soundness, a higher-order backend is a worthwhile addition to TLAPS, because specific TLA⁺ obligations do require higher-order unification to be solved. As example, one may take any proof that involves the principle of natural induction:

$$P(0) \wedge (\forall x \in Nat : P(x) \Rightarrow P(x + 1)) \Rightarrow \forall x \in Nat : P(x)$$

The principle is formalized as a lemma of TLAPS’s standard library. When it is invoked, the current goal must be unified with the higher-order variable P. Similar situations arise for general well-founded inductions, or whenever a proof involves user-defined recursive operators. Zipperposition is especially useful for these goals, as the only other backend supporting higher-order logic is Isabelle, whose basic automation tactic are often unable to handle mildly complex obligations.

Our original plans for the SMT encoding included a reimplementation of type synthesis and preprocessing. Instead, we found that most obligations could be solved by SMT with heuristics for the instantiation of TLA⁺’s axioms. These heuristics are implemented by triggers indicating to the solver some terms to look for in order to derive relevant instances. Triggers are a popular solution for users of SMT wishing to stabilize custom theories [30, 50, 55]. They are pivotal in our approach. We use triggers to implement heuristics for reasoning in untyped set theory, and the efficacy of these heuristics for TLA⁺ has been confirmed experimentally. Moreover, triggers extend the direct encoding with little need to change the translation itself, so soundness is not compromised by this technique. Only some adjustments are needed to support second-order constructs, integer arithmetic, and the axiom of set extensionality.

## 1.4 Outline

In Chapter 2, we present the necessary context about automated theorem proving (with a focus on SMT) and the specification language TLA⁺. The first section is an overview of SMT’s theory with its fundamental results and limits. Some generic definitions from the field of mathematical logic are given, in anticipation of the formal treatment of TLA⁺’s logic in future chapters. The second section is an overview of TLA⁺ and its tools. The model checker TLC is briefly introduced, followed by the proof assistant TLAPS. Working TLA⁺ examples are presented to illustrate the usage of these tools.

In Chapter 3, we develop our formal definition of TLA⁺’s constant fragment, including its syntax and semantics. The constant fragment includes TLA⁺’s variant of first-order logic and set theory, but it does not contain the temporal aspects of the logic. In TLA⁺, silly expressions such as $1 \cup \texttt{foo}$ have a denotation. We may not know what this expression denotes, but we know, for example, that it is a set, and that it equals $\texttt{foo} \cup 1$. We propose to formalize the primitive symbols of TLA⁺ as uninterpreted symbols specified only by axioms. TLA⁺ is thus formalized as a logic $\mathcal{L} + T$, where $\mathcal{L}$ is a generic logic providing the interpretations of
Boolean connectives (including quantifiers), and *T* a standard theory containing the axioms of set theory, functions, arithmetic, and more.

In Chapter 4, we define a direct encoding of TLA⁺ into HOL. A higher-order logic is necessary to encode the second-order constructs of TLA⁺ and axiom schemas. For instance, set comprehension {$x \in S : e$} is viewed as a second-order application `setst(S, λx : e)`, and the full schema of comprehension from ZF is encoded as a single axiom. The direct encoding consists in two essential steps: first, an elementary pass over expressions to correct ambiguities regarding Boolean and non-Boolean expressions; second, the insertion of relevant axioms into the final problem. The translation itself preserves the structure of the original TLA⁺ expressions. The direct encoding has been implemented in TLAPS, and the superposition prover Zipperposition added as a new backend. We compare the performances of Zipperposition and Isabelle on a large collection of TLA⁺ proof obligations; our results demonstrate that the two backends have complementary strengths.

In Chapter 5, we extend the direct encoding to an SMT encoding for TLA⁺. Most of the direct encoding's structure and implementation is reused for the SMT encoding; parts of the axiomatizations are revised. Axioms are reformulated and annotated with E-matching patterns (triggers), which have been chosen and refined through an empirical process. We illustrate this process through a simple but realistic TLA⁺ proof obligation, exploring several options for triggers and observing their effects on the SMT procedure. We then derive some general principles underlying our strategy for trigger selection. A few peripheral topics about the axiomatization of TLA⁺ for SMT are addressed: reduction to first-order logic and axiom schemas; axioms for using SMT's integer arithmetic; axioms for set extensionality. Finally, our version of the SMT encoding is compared with the original one of TLAPS. Despite the simpler design of our encoding, we achieve similar performances.
# Chapter 2

## Background

This chapter is divided into two sections. We first review the theory of automated theorem proving through the lens of satisfiability modulo theory (SMT). We then give an overview of TLA$^+$ and its main tools TLC and TLAPS. We conclude this chapter by a brief review of the SMT encoding currently implemented in TLAPS. That encoding will be referred to as the “previous” or “original” SMT encoding to distinguish it from our own version.

### 2.1 Automated Theorem Proving

Automated theorem proving is the design and study of computational procedures (algorithms) for deciding the validity of mathematical formulas. This presupposes two important notions: validity and procedure. The first is formally defined by mathematical logic [45], and the second by the theory of computability [21].

We assume some informal notion of algorithm and will use pseudo-code for our examples. For any formal problem $P(x)$ with parameter $x$, we call *decision procedure* an algorithm that takes $x$ as input and answers either “yes” or “no”, depending on whether $P(x)$ is true or false. A problem is called *decidable* if there is a decision procedure for it, otherwise it is *undecidable*. Some undecidable problems still admit *semi-decision procedures*, which always answer “yes” in the positive case, but in the negative case may answer “no” or never return an answer. These problems are called *semi-decidable*.

SMT solvers extend decision procedures for propositional logic to handle theories of first-order logic, including the general theory of quantifiers. We present the DPLL procedure for propositional logic, then the SMT approach for theories of first-order logic, focussing on the general problem of first-order instantiation.

In the context of interactive theorem proving, SMT solvers are a popular option to automatically handle large proof obligations [9,29,32]. Another important approach to automated theorem proving is *superposition provers*, which are based on extensions of the resolution inference rule [4, 66]. The treatment of first-order quantifiers is central in resolution-based systems, while SMT’s strength is its support for decidable first-order theories.

#### 2.1.1 The DPLL Procedure

For most studies concerning mathematical logic, the starting point is propositional logic (PL). As we present the syntax and semantics of PL, we introduce some general concepts
of mathematical logic. The truth of a propositional formula $\phi$ depends on the truth of the propositional variables it contains, and the problem of deciding, for a given $\phi$, if there exists an assignment of propositional variables making $\phi$ true is called the SAT problem. The DPLL procedure is an algorithm for deciding the SAT problem [23]. Modern SAT solvers are based on an extension of DPLL called CDCL.

## Propositional Logic

We define the generic notion of a *logic* to fix some important terminology. All the logics we will consider (propositional, first-order logic, TLA$^+$) fit into the following definition.

**Definition 2.1.1 (Logic).** A *logic* is a triple $(L, M, \models)$ where $L$ is a collection of formulas (the language), $M$ a collection of interpretations, and $\models$ a relation on $M \times L$ called the satisfaction relation. For all $\phi \in L$ and $I \in M$, we say that $I$ satisfies $\phi$ if $I \models \phi$. A formula is satisfiable if it is satisfied by some interpretation, otherwise it is unsatisfiable.

All the languages we will consider can be defined from BNF grammars, which are sets of formation rules describing how complex terms are formed through the combination of simpler ones. The definition of PL's syntax below is based on a BNF grammar.

**Definition 2.1.2 (Syntax of Propositional Logic).** Propositional logic is parameterized by some collection $\Sigma$ of propositional variables, called a *propositional signature*. The language of PL is given by the grammar

$$ \phi ::= p \mid \text{TRUE} \mid \text{FALSE} \mid \neg \phi \mid \phi \land \phi \mid \phi \lor \phi \mid \phi \Rightarrow \phi \mid \phi \leftrightarrow \phi \quad \text{where } p \in \Sigma $$

The collection of propositional formulas over the signature $\Sigma$ is noted $P(\Sigma)$.

Grammars are ambiguous when certain terms of the language admit several formations. For instance, $\phi \land \psi \lor \rho$ is an ambiguous formula. We use parentheses to remove ambiguities when necessary, for instance we will write $(\phi \land \psi) \lor \rho$ or $\phi \land (\psi \lor \rho)$. To reduce the number of parentheses, we fix some priority rules between the propositional connectives. The connectives $\land$ and $\lor$ have priority over $\Rightarrow$ and $\Leftrightarrow$, so that $\phi \land \psi \Rightarrow \rho \lor \chi$ is read $(\phi \land \psi) \Rightarrow (\rho \lor \chi)$. The connective $\neg$ has priority over all the other connectives, so $\neg \phi \lor \psi$ is read $(\neg \phi) \lor \psi$ for example.

**Definition 2.1.3 (Semantics of Propositional Logic).** Let $\Sigma$ be a propositional signature. A $\Sigma$-valuation is a subset $\theta \subseteq \Sigma$. We define the satisfaction relation for all valuations $\theta$ and formulas $\phi$ by

$$ \theta \models p \qquad \text{iff } p \in \theta $$

$$ \theta \models \text{TRUE} $$

$$ \theta \not\models \text{FALSE} $$

$$ \theta \models \neg \phi \qquad \text{iff } \theta \not\models \phi $$

$$ \theta \models \phi \land \psi \qquad \text{iff } \theta \models \phi \text{ and } \theta \models \psi $$

$$ \theta \models \phi \lor \psi \qquad \text{iff } \theta \models \phi \text{ or } \theta \models \psi $$

$$ \theta \models \phi \Rightarrow \psi \qquad \text{iff } \theta \models \phi \text{ implies } \theta \models \psi $$

$$ \theta \models \phi \leftrightarrow \psi \qquad \text{iff } \theta \models \phi \text{ equals } \theta \models \psi $$

Propositional logic over a signature $\Sigma$ is defined by the language $P(\Sigma)$, the collection of all $\Sigma$-valuations, and the satisfaction relation just defined.
There is some additional terminology to consider regarding satisfiability. For theorem proving, we are especially interested in formulas that are true for all interpretations, or for classes of interpretations fixed by sets of formulas called theories.

**Definition 2.1.4** (Theories). Consider a generic logic with satisfaction relation $|=$. A theory is a collection of formulas $T$. $T$ is satisfied by an interpretation $I$ if all formulas of $T$ are simultaneously satisfied by $I$. In that case, we call $I$ a *model* of $T$, and we note $I \models T$. $T$ is unsatisfiable if it has no model.

Let $T$ be a theory. A formula $\phi$ is a logical consequence of $T$ if $\phi$ is satisfied by all models of $T$. This is noted $T \models \phi$. A *tautology*, or *valid* formula, is a consequence of the empty theory. We note $|=$ when $\phi$ is valid.

**Example 2.1.5.** Here are some tautologies of propositional logic (for all $\phi, \psi$):

<figure><img src="image_4.png" /></figure>

The satisfiability or validity of a given formula can be established by the method of *truth tables*. Consider the formula $\neg(p \Rightarrow q)$. There are only two propositional variables in that formula, $p$ and $q$. Clearly, for all valuations $\theta$, we only need to consider whether $p$ and $q$ are satisfied by $\theta$. There are only four possibilities; for each of them, we can simply evaluate whether the formula is satisfied or not by following the recursive definition of $|=$. All four situations are represented by the table below, where 1 indicates satisfaction and 0 indicates non-satisfaction. We also indicate satisfaction for the subformula $p \Rightarrow q$.

<table><thead><tr><th>p</th><th>q</th><th>p &rarr; q</th><th>&not; (p &rarr; q)</th></tr></thead><tbody><tr><td>0</td><td>0</td><td>1</td><td><b>0</b></td></tr><tr><td>0</td><td>1</td><td>1</td><td><b>0</b></td></tr><tr><td>1</td><td>0</td><td>0</td><td><b>1</b></td></tr><tr><td>1</td><td>1</td><td>1</td><td><b>0</b></td></tr></tbody></table>

As this table shows, $\neg(p \Rightarrow q)$ is satisfiable, and the only valuation that makes it true is the one that contains $p$ but not $q$. For a formula to be valid, it must be satisfied in all situations, so $\neg(p \Rightarrow q)$ is not valid.

The method of truth tables demonstrates a naive decision procedure for propositional logic. Formally, the problems “$\phi$ is satisfiable” and “$\phi$ is valid” for the parameter $\phi \in P(\Sigma)$ are both decidable. Moreover, there is a close correspondence between the two. Consider the equivalence

$$| = \phi \quad \text{iff} \quad \text{for all } \theta, \theta' \neq \neg\phi \quad \text{iff} \quad \neg\phi \text{ is unsatisfiable}$$
More generally,

$$ T \models \phi \quad \text{iff} \quad \text{for all } \theta, \theta' \models T \text{ implies } \theta \not\models \neg \phi \quad \text{iff} \quad T \cup \{\neg \phi\} \text{ is unsatisfiable} $$

For theorem proving, we are more interested in deciding validity than satisfiability. But solvers may be more oriented towards the problem of satisfiability. We may still use such solvers for deciding validity by checking that the *negation* of a goal is unsatisfiable, possibly in the context of a theory *T*.

## SAT Solvers

The procedure of decision for PL based on truth tables requires going through all possible valuations for a given formula. If the input formula contains *n* propositional variables, the number of possibilities is $2^n$. Some industrial applications involve problems with millions of parameters, so this naive procedure cannot be used realistically. Modern SAT solvers like Chaff [56], GRASP [72] or MiniSAT [31] are based on a procedure called DPLL [23]. The first step consists in preprocessing formulas into a more restrictive language [3].

**Definition 2.1.6** (Conjunctive Normal Forms). Let $\Sigma$ be a propositional signature. We define literals, clauses and CNF formulas by the grammar

$$ l ::= p \mid \neg p \qquad \text{(Literals)} $$

$$ C ::= \text{FALSE} \mid l \lor C \qquad \text{(Clauses)} $$

$$ N ::= \text{TRUE} \mid N \land C \qquad \text{(CNF Formulas)} $$

A formula $\phi$ is in conjunctive normal form (CNF) if it can be read as a CNF formula.

Two formulas $\phi$ and $\psi$ are equisatisfiable when $\phi$ is satisfiable iff $\psi$ is. We admit that for all formulas $\phi$, there is a CNF formula $N(\phi)$ such that $\phi$ and $N(\phi)$ are equisatisfiable.

**Example 2.1.7.** Consider the formula

$$ p \lor q \Rightarrow r $$

A possible CNF formula for it is

$$ (\neg p \lor r) \land (\neg q \lor r) $$

One can verify that the equivalence of the two formulas is a tautology. Equivalently, one can compare the truth tables for the two formulas side to side and verify that they are satisfied by the same valuations:

<table><thead><tr><th>p</th><th>q</th><th>r</th><th>p ∨ q</th><th>p ∨ q ⇒ r</th><th>¬p ∨ r</th><th>¬q ∨ r</th><th>(¬p ∨ r) ∧ (¬q ∨ r)</th></tr></thead><tbody><tr><td>0</td><td>0</td><td>0</td><td>0</td><td><b>1</b></td><td>1</td><td>1</td><td><b>1</b></td></tr><tr><td>0</td><td>0</td><td>1</td><td>0</td><td><b>1</b></td><td>1</td><td>1</td><td><b>1</b></td></tr><tr><td>0</td><td>1</td><td>0</td><td>1</td><td><b>0</b></td><td>1</td><td>0</td><td><b>0</b></td></tr><tr><td>0</td><td>1</td><td>1</td><td>1</td><td><b>1</b></td><td>1</td><td>1</td><td><b>1</b></td></tr><tr><td>1</td><td>0</td><td>0</td><td>1</td><td><b>0</b></td><td>0</td><td>1</td><td><b>0</b></td></tr><tr><td>1</td><td>0</td><td>1</td><td>1</td><td><b>1</b></td><td>1</td><td>1</td><td><b>1</b></td></tr><tr><td>1</td><td>1</td><td>0</td><td>1</td><td><b>0</b></td><td>0</td><td>0</td><td><b>0</b></td></tr><tr><td>1</td><td>1</td><td>1</td><td>1</td><td><b>1</b></td><td>1</td><td>1</td><td><b>1</b></td></tr></tbody></table>
CNF formulas admit a simpler representation than general formulas. Consider the following logical equivalences for all $\phi$, $\psi$ and $\rho$:

$$ 
\begin{aligned}
\phi \lor \psi &\Leftrightarrow \psi \lor \phi \\
(\phi \lor \psi) \lor \rho &\Leftrightarrow \phi \lor (\psi \lor \rho) \\
\phi \lor \phi &\Leftrightarrow \phi \\
\mathrm{FALSE} \lor \phi &\Leftrightarrow \phi
\end{aligned}
$$

These laws express that $\lor$ is commutative, associative, and that $\mathrm{FALSE}$ is neutral for $\lor$. They justify the representation of clauses by finite sets of literals: the order of literals does not matter in a clause, nor does the duplication of literals; the clause $\mathrm{FALSE}$ can be represented by the empty set. For similar reasons, CNF formulas can be represented by sets of clauses; in that case, the empty set represents the formula $\mathrm{TRUE}$.

A literal $l$ is of the form $p$ or $\neg p$ where $p$ is a propositional variable. Let us write $\bar{l}$ to refer to whichever case is the opposite for $l$. The DPLL procedure takes a CNF formula as input and incrementally takes decisions for all literals, simplifying the current formula for each decision. That process of simplification is called *propagation*.

**Definition 2.1.8 (Propagation).** Let $N$ be a CNF formula and $l$ a literal. The *propagation* of $l$ into $N$ is the CNF formula $N[l]$ obtained by removing from $N$ all clauses containing $l$, and removing $\bar{l}$ from the remaining clauses. Clearly, neither $l$ nor $\bar{l}$ occurs in $N[l]$.

If $N$ is satisfiable, then for all $l$ either $l \land N[l]$ or $\bar{l} \land N[\bar{l}]$ is satisfiable. A simple procedure is implemented by selecting an $l$, recording the decision and testing for the satisfiability of $N[l]$; if that formula is unsatisfiable, then we test $N[\bar{l}]$ instead. Unsatisfiability is easily detected by searching for the empty clause in derived formulas. This simple procedure still requires testing for all $2^n$ possibilities in the unsatisfiable case. DPLL optimizes the search through *unit propagation* to prune the decision tree.

**Definition 2.1.9 (DPLL).** Figure 2.1 presents the DPLL procedure in pseudo-code. The sub-procedure *select* returns a literal occurring in $N$ but not in *decisions* or *inferred*.

The DPLL algorithm selects literals to set and records them in a sequence *decisions*. Each decision is propagated through the current formula. If the formula is reduced to the empty CNF formula $\mathrm{TRUE}$, then the decision trail is a valuation that satisfies the original formula; if the current formula contains the empty clause $\mathrm{FALSE}$ (this is called a *conflict*), then it is unsatisfiable under the current constraint, so decisions must be undone. In the algorithm above, backtracking to an earlier decision is achieved by using recursion. DPLL optimizes the search by managing another sequence *inferred*. In some situations, the right value for a literal can be deduced from the formula and the current constraint. If deciding $l$ resulted in a conflict, then $\bar{l}$ is necessarily true. If a *unit clause* reduced to the literal $l$ occurs in the formula, then $l$ has to be true. The latter optimization is called *unit propagation*.

**Example 2.1.10.** Consider the following set of clauses:

$$ p \lor q \lor r, \quad \neg p \lor q, \quad \neg p \lor \neg q \lor r, \quad \neg q \lor \neg r $$
DPLL\_main(decisions, inferred, N):

// Unit propagation

for all {l} ∈ N:

inferred := cons(l, inferred)

N := N[l]

if N = ∅ then:

return SAT(decisions + inferred)

if ∅ ∈ N:

return UNSAT

else:

l := select(decisions, inferred, N)

result := DPLL\_main(cons(l, decisions), inferred, N[l])

if result is UNSAT then:

result := DPLL\_main(decisions, cons(¯l, inferred), N[¯l])

return result

DPLL(φ):

N := cnf(φ)

decisions := nil

inferred := nil

DPLL\_main(decisions, inferred, N)

<caption>Figure 2.1: DPLL Procedure</caption>

We present below a possible run of the DPLL algorithm. Inferred literals either result from
unit propagation (UP) or backtracking after a conflict (BT).

<table>
  <tbody>
    <tr>
      <td>p ∨ q ∨ r,</td>
      <td>¬p ∨ q,</td>
      <td>¬p ∨ ¬q ∨ r,</td>
      <td>¬q ∨ ¬r</td>
      <td>(Init)</td>
    </tr>
    <tr>
      <td></td>
      <td>q,</td>
      <td>¬q ∨ r,</td>
      <td>¬q ∨ ¬r</td>
      <td>(Decide p)</td>
    </tr>
    <tr>
      <td></td>
      <td></td>
      <td>r,</td>
      <td>¬r</td>
      <td>(Infer q (UP))</td>
    </tr>
    <tr>
      <td></td>
      <td></td>
      <td></td>
      <td>FALSE</td>
      <td>(Infer r (UP))</td>
    </tr>
    <tr>
      <td>p ∨ q ∨ r,</td>
      <td>¬p ∨ q,</td>
      <td>¬p ∨ ¬q ∨ r,</td>
      <td>¬q ∨ ¬r</td>
      <td>(Backtrack)</td>
    </tr>
    <tr>
      <td>q ∨ r,</td>
      <td></td>
      <td></td>
      <td>¬q ∨ ¬r</td>
      <td>(Infer ¬p (BT))</td>
    </tr>
    <tr>
      <td></td>
      <td></td>
      <td></td>
      <td>¬r</td>
      <td>(Decide q)</td>
    </tr>
    <tr>
      <td></td>
      <td></td>
      <td></td>
      <td></td>
      <td>(Infer ¬r (UP))</td>
    </tr>
  </tbody>
</table>

There are no clauses left in the last state so the formula is satisfiable. The solution is given by the set of literals {¬p, q, ¬r}. Notice that because q is decided by unit propagation the first time, the second backtracking step reverts to the decision of p.

Modern SAT solvers are based on an extension of DPLL called *conflict-driven clause learning* (CDCL) [43,72]. Whenever the algorithm encounters a conflict (the empty clause is derived after propagation), the current trail of decisions is analysed to derive a new clause. Suppose the analysis determines that the decisions $l_1, \dots, l_n$ lead to the conflict. Then the
original formula must entail $\neg(l_1 \wedge \dots \wedge l_n)$, which corresponds to the clause $\overline{l_1} \vee \dots \vee \overline{l_n}$. By adding this *learned clause* to the original problem, the risk of replaying the same conflict is removed. This technique can be combined with *backjumping* to backtrack to earlier decisions in the trail.

### 2.1.2 Satisfiability Modulo Theories

Propositional logic has interesting applications but it is not expressive enough for most mathematical theories. First-order logic (FOL) extends PL in several aspects. The propositional variables are replaced by statements expressing relations between different terms; quantifiers enable the formal expression of universal and existential statements. The satisfaction relation of FOL involves *domains* of objects to interpreted terms, which makes first-order satisfiability inherently more complex than propositional satisfiability. Nevertheless, some theories of FOL are decidable, and validity in pure FOL is semi-decidable. SMT solvers specialize in deciding the satisfiability of formulas for first-order theories of interest.

#### First-order Logic

**Definition 2.1.11 (First-order Terms).** A term signature is a collection $\Sigma$ of symbols with assigned numbers called arities. Let $X$ be some infinite collection of variable symbols. We define the collection of terms $T(\Sigma, X)$ by the grammar

$$t ::= x \mid f(t, \dots, t)$$

where $x \in X$ and $f \in \Sigma$. An application $f(t_1, \dots, t_n)$ is well-formed only if the arity of $f$ is $n$. If $c$ is a symbol with arity 0, the application of $c$ to zero arguments is simply noted $c$.

The collection of variable symbols $X$ is usually fixed and omitted from all notations, so we usually note $T(\Sigma)$ for a collection of terms.

**Definition 2.1.12 (First-order Logic).** A first-order signature is an union $\Sigma = \Sigma_F \uplus \Sigma_P$ where $\Sigma_F$ is a term signature and $\Sigma_P$ a collection of predicate symbols with arities. The language of first-order logic over $\Sigma$ is defined by the grammar

$$\begin{array}{l}
\phi ::= p(t, \dots, t) \mid t = t \\
\qquad | \text{TRUE} \mid \text{FALSE} \mid \neg\phi \mid \phi \wedge \phi \mid \phi \vee \phi \mid \phi \Rightarrow \phi \mid \phi \Leftrightarrow \phi \\
\qquad | \forall x : \phi \mid \exists x : \phi
\end{array}$$

where $x \in X$, $t \in T(\Sigma_F)$, and $p \in \Sigma_P$. The application $p(t_1, \dots, t_n)$ is well-formed only if the arity of $p$ is $n$. An atomic proposition is a formula $p(t_1, \dots, t_n)$ or $t_1 = t_2$. The collection of atomic propositions is noted $A(\Sigma)$. The collection of formulas is noted $F(\Sigma)$.

Let $D$ be some collection called *domain*. A valuation is a function $\theta : X \to D$. An interpretation $I$ consists of two families $(f^I)_{f \in \Sigma_F}$ and $(p^I)_{p \in \Sigma_P}$ such that $f^I \in D^n \to D$ when the arity of $f$ is $n$, and $p^I \subseteq D^n$ when the arity of $p$ is $n$. We define the evaluation of terms as a function $[\cdot]_\theta^I$ by

$$\begin{align*}
[\![x]\!]_\theta^I &\triangleq \theta(x) \\
[\![f(t_1, \dots, t_n)]\!]_\theta^I &\triangleq f^I([\![t_1]\!]_\theta^I, \dots, [\![t_n]\!]_\theta^I)
\end{align*}$$
For all $t \in T(\Sigma_F)$, the value $\llbracket t \rrbracket_\theta^I$ is an element of $D$. For all valuations $\theta$, variables $x$ and values $v \in D$, let $\theta_v^x$ be the valuation that reassigns $x$ to $v$. We now define the satisfaction relation $\models$ as a ternary relation by

$$I, \theta \models p(t_1, \dots, t_n)$$

$$I, \theta \models t_1 = t_2$$

$$I, \theta \models \forall x : \phi$$

$$I, \theta \models \exists x : \phi$$

$$\text{iff } (\llbracket t_1 \rrbracket_\theta^I, \dots, \llbracket t_n \rrbracket_\theta^I) \in p^I$$

$$\text{iff } \llbracket t_1 \rrbracket_\theta^I = \llbracket t_2 \rrbracket_\theta^I$$

$$\text{iff } I, \theta_v^x \models \phi \quad \text{for all } v \in D$$

$$\text{iff } I, \theta_v^x \models \phi \quad \text{for some } v \in D$$

The rules involving propositional connectives are omitted as they are analogous to the ones for propositional logic.

We note $Qx : \phi$ for a formula $\forall x : \phi$ or $\exists x : \phi$. In such formulas, the variable $x$ is said to be bound, and $\phi$ is called the scope of the binder $Qx$. Any variable in a first-order formula is bound by at most one quantifier, otherwise it is called free. A formula with no free variables is called ground. The interpretation of any formula does not depend on the values $\theta(x)$ such that $x$ is not free. In the case of ground formulas, the interpretation does not matter on $\theta$ at all, so we simply note $I \models \phi$ when $\phi$ is ground and $I, \theta \models \phi$ for some arbitrary $\theta$.

Chains of quantifiers are usually shortened by writing $\forall x, y, z : \phi$ and $\exists x, y, z : \phi$. The scope of a quantifier is assumed to be the formula that extends until the next enclosing parenthesis. For instance, $\forall x : p(x) \Rightarrow q(c)$ is read as $\forall x : (p(x) \Rightarrow q(c))$.

**Example 2.1.13.** Here are some tautologies of FOL:

$$\begin{align*}
(\neg\forall x : p(x)) &\Leftrightarrow \exists x : \neg p(x) \\
(\neg\exists x : p(x)) &\Leftrightarrow \forall x : \neg p(x) \\
(p \wedge \forall x : q(x)) &\Leftrightarrow \forall x : p \wedge q(x) \\
((\forall x : p(x)) \Rightarrow q) &\Leftrightarrow \exists x : p(x) \Rightarrow q \\
(\exists y \forall x : p(x, y)) &\Rightarrow \forall x \exists y : p(x, y) \\
(\forall x : p(x, f(x))) &\Rightarrow \forall x \exists y : p(x, y)
\end{align*}$$

Validity for arbitrary formulas of first-order logic is undecidable [80]. This classical result relies on a reduction of the halting problem (the problem of deciding termination for arbitrary procedures) to the problem of validity for FOL. See for example Paragraph 45 in Kleene [45]. However, some particular theories are known to be decidable. The most popular example is *Presburger arithmetic*, also called linear integer arithmetic.

**Example 2.1.14 (Presburger Arithmetic).** The signature of linear arithmetic contains the constant symbol $Z$ (zero), the unary symbol $S$ (successor) and the binary symbol $+$ (used in infix notation). It does not include predicates, but comparisons $\le$ and $<$ can be defined by first-order formulas. The theory is described by the axioms

$$\forall x : S(x) \neq Z$$

$$\forall x, y : S(x) = S(y) \Rightarrow x = y$$

$$\forall x : x + Z = x$$

$$\forall x, y : x + S(y) = S(x + y)$$

$$P(Z) \wedge (\forall x : P(x) \Rightarrow P(S(x))) \Rightarrow \forall x : P(x) \quad \text{for all formulas } P(x)$$
The last line is not a single axiom but an infinite collection of axioms called a schema.

Let $T$ be the collection of axioms for linear arithmetic. Then the problem $T \models \phi$, where the parameter $\phi$ is a formula in the language of linear arithmetic, is decidable. The proof of this results relies on a quantifier-elimination technique [75].

Other examples of decidable theories include the theory of real closed fields or the theory of fixed-size bitvectors [8,15]. Expressive theories tend to be undecidable; if one extends linear integer arithmetic with a symbol and axioms for multiplication, one obtains non-linear integer arithmetic, which is undecidable. It follows that any extension of linear integer arithmetic in which multiplication can be defined is also undecidable [40].

The generic theory of first-order logic, also called the empty theory because no fixed signature or axioms are given, is undecidable. However, under some restrictions, it is decidable [36]. A notable decidable class of FOL is the class of effectively propositional formulas (EPR) [26]. While undecidable in general, the empty theory is semi-decidable. This can be established through a classical result by Herbrand [13,41], which is stated below.

A formula is called quantifier-free when it does not contain quantifiers. Let $\phi$ be quantifier-free and let $x_1, \dots, x_n$ be its free variables. Then the universal closure of $\phi$ is the formula $\forall x_1 \dots x_n : \phi$, noted $\forall^*\phi$. When $\phi$ is quantifier-free, $\forall^*\phi$ is said to be universal and prenex. A substitution is a function $\sigma : X \to T(\Sigma)$; a substitution is ground if all terms $\sigma(x)$ are ground. The result of applying a substitution $\sigma$ to $\phi$ is the formula $\phi\sigma$ (each free variable $x$ is replaced by $\sigma(x)$). Then an instance of $\forall^*\phi$ is a ground formula $\phi\sigma$.

**Theorem (Herbrand).** For all $\phi$ quantifier-free, $\forall^*\phi$ is unsatisfiable iff there exists a finite, unsatisfiable set of instances $\{\phi\sigma_1, \dots, \phi\sigma_n\}$.

Herbrand's Theorem gives the basis for a semi-decision procedure for the empty theory. In order to establish this, we admit two additional results.

**Lemma.** Every first-order formula $\phi$ admits an equisatisfiable prenex formula $\forall^*\psi$.

**Lemma.** A quantifier-free formula $\phi$ is an element of $P(A(\Sigma))$. Suppose $\phi$ is quantifier-free and without equalities. Then $\phi$ is satisfiable as a first-order formula iff it is satisfiable as a propositional formula.

The first lemma is proved by applying a series of logical laws (some of them displayed in Example 2.1.13) to move quantifiers up the structure of $\phi$, then apply a technique called Skolemization to eliminate existential quantifiers [3]. The second lemma involves building a first-order model from a propositional one, called a Herbrand model. Its generalization to formulas with equalities is not trivial, but can be done if satisfiability in PL is constrained by axioms for equality [70].

The naive semi-decision procedure for FOL proceeds as follows. The input is a formula $\phi$. To decide $\models \phi$, we check for the unsatisfiability of $\neg\phi$. There is a formula $\forall^*\psi$ that is satisfiable iff $\neg\phi$ is. We enumerate all finite sets of ground instances $\{\psi\sigma_1, \dots, \psi\sigma_n\}$, testing for the propositional satisfiability of every set (using DPLL for example). If a set is satisfiable, we resume with the next set of instances. If a set is unsatisfiable, then it is also unsatisfiable as a set of first-order formulas, and by Herbrand's Theorem $\forall^*\psi$ is unsatisfiable and thus $\models \phi$. Now, assuming $\models \phi$, then an unsatisfiable set of instances must exist, so the procedure will terminate.
## SMT Solvers

SMT solvers were originally created to solve logical constraints expressed in the quantifier-free (QF) fragment of FOL. These constraints may involve interpreted domains and symbols (arithmetic, arrays, fixed size bitvectors, etc.), or uninterpreted symbols over unspecified domains. Two important extensions of this basic model are the possibility to combine theories whose signatures do not intersect, and support for first-order quantifiers. The adequate language for SMT problems is a *multi-sorted first-order logic* (MS-FOL), which extends the syntax of FOL with type annotations and restricts the combination of symbols to prohibit meaningless expressions.

There exist several approaches to implementing SMT. The one we describe here is the *lazy procedure* based on the popular DPLL(T) architecture [35, 59]. As the name suggests, DPLL(T) combines a DPLL procedure with a solver for the parameter theory T, referred to as a T-solver. Besides checking for satisfiability in T, the T-solver must be able to provide *explanations* for unsatisfiable set of literals, in order to cooperate with the propositional solver. Some problems involve several theories with their corresponding solvers; given a set of Tᵢ-solvers such that the signatures of distinct theories Tᵢ do not overlap, there is a procedure for combining all solvers into a single one for the union of all theories [57, 71]. The theory of *equality and uninterpreted functions* (EUF), which is decidable, plays a central role in this framework, as the equality symbol is common to all theories. Procedures for solving problems of EUF are generally based on congruence closure algorithms [70].

**Example 2.1.15.** This example will illustrate the cooperation between a SAT solver implementing clause learning and a solver for linear integer arithmetic. Consider the formula

$$a - b = 0 \land (f(a) = f(b) \Rightarrow P(a) \land \neg P(b))$$

where a and b are integer constants and f is an uninterpreted function of integers. From the SAT solver's point of view, atoms are abstracted as propositional variables; a possible representation in CNF form is

$$p_1 \land (\neg p_2 \lor p_3) \land (\neg p_2 \lor \neg p_4)$$

with the definitions

$$p_1 \triangleq a - b = 0$$

$$p_3 \triangleq P(a)$$

$$p_2 \triangleq f(a) = f(b)$$

$$p_4 \triangleq P(b)$$

Naive CNF transformations may result in exponential increases of the lengths of the formulas. Modern solvers implement a CNF transformation called the Tseitin transformation, which maintains a linear increase in size [79]. That transformation introduces variables for subformulas; in our example, a variable would be introduced to represent $P(a) \land \neg P(b)$.

The propositional formula is satisfied by the valuation $\{p_1, \neg p_2, p_3, p_4\}$. Suppose the SAT solver returns this candidate model to the T-solver, where T combines linear integer arithmetic with EUF. The T-solver will find the subset $\{p_1, \neg p_2\}$ to be unsatisfiable. Indeed, from $a - b = 0$ it follows (by arithmetic) that $a = b$, and then $f(a) = f(b)$ (by congruence). This contradiction is represented by the clause $\neg p_1 \lor p_2$, which is sent back to the SAT solver. The new problem is

$$p_1 \land (\neg p_2 \lor p_3) \land (\neg p_2 \lor \neg p_4) \land (\neg p_1 \lor p_2)$$
The SAT solver will return the model $p_1, p_2, p_3, \neg p_4$ (this is the only solution as it can be found directly by unit propagation). The T-solver will again find a contradiction as $a = b$ entails $\neg(P(a) \land \neg P(b))$. The unsatisfiable subset is $\{p_1, p_3, \neg p_4\}$, so the clause $\neg p_1 \lor \neg p_3 \lor p_4$ is added to the propositional problem:

$$p_1 \land (\neg p_2 \lor p_3) \land (\neg p_2 \lor \neg p_4) \land (\neg p_1 \lor p_2) \land (\neg p_1 \lor \neg p_3 \lor p_4)$$

The SAT solver will find that problem to be unsatisfiable, which means the original formula is unsatisfiable.

The cooperation of a SAT solver with a T-solver as we just described defines a ground SMT solver. When a problem contains quantifiers $\forall$ or $\exists$, this framework is typically extended with an *instantiation module*. The combination of such a module with a ground SMT solver defines a general SMT solver. Here is a simplified view of this extended architecture: the problem with quantifiers can be represented as a problem $E \uplus Q$ where $E$ is a set of ground formulas, and $Q$ a set of formulas with quantifiers. Usually the elements of $Q$ are assumed to be in universal prenex form $\forall^*\phi$, although solvers may handle quantifiers differently for efficiency reasons [3]. The ground SMT solver may find $E$ to be unsatisfiable (in which case the original problem is unsatisfiable). If $E$ is satisfiable, then the instantiation module is called. Three outcomes are possible: either the satisfiability of $E \uplus Q$ can be verified (then the answer is “sat”); if it cannot be verified, then a number of *instance lemmas* may be produced and added to the ground problem, restarting the whole process; if the satisfiability of $E \uplus Q$ cannot be verified, and no instance lemmas are produced, the SMT solver will return “unknown” [63].

In the context of automated theorem proving, our goal is generally to check for unsatisfiability. Therefore, we will focus on strategies to generate instance lemmas. The general form of an instance lemma is $(\forall^*\phi) \Rightarrow \phi\sigma$ where $\forall^*\phi$ is an element of $Q$.

**Example 2.1.16.** The following example is taken from Reynolds et al [63]. We consider the set of formulas

$$\neg P(a) \land \neg P(b) \land P(c) \land \neg R(b) \land (\forall x : P(x) \lor R(x))$$

where $a, b, c$ are uninterpreted constants and $P, R$ are uninterpreted predicates. As a propositional CNF formula, this problem is represented

$$\neg p_1 \land \neg p_2 \land p_3 \land \neg p_4 \land q$$

with the definitions

$$p_1 \triangleq P(a)$$

$$p_4 \triangleq R(b)$$

$$p_2 \triangleq P(b)$$

$$q \triangleq \forall x : P(x) \lor R(x)$$

$$p_3 \triangleq P(c)$$

The problem is partitioned into the ground problem $E \triangleq \{\neg p_1, \neg p_2, p_3, \neg p_4\}$ and the set $Q \triangleq \{q\}$. $E$ has a trivial (and unique) solution, so the instantiation module is called.

Assuming the only possible terms are $a, b$ and $c$, there are three possible instance lemmas:

$$q \Rightarrow P(a) \lor R(a)$$

$$q \Rightarrow P(b) \lor R(b)$$

$$q \Rightarrow P(c) \lor R(c)$$
The second instance, in particular, reduces to the clause $\neg q \lor p_2 \lor p_4$ by propositional abstraction. Suppose our instantiation strategy selects that lemma. Then the new propositional problem is

$$ \neg p_1 \land \neg p_2 \land p_3 \land \neg p_4 \land q \land (\neg q \lor p_2 \lor p_4) $$

That problem is unsatisfiable, so the solver returns “unsat”.

First-order instantiation is a difficult problem, and several strategies for selecting instances exist. Most SMT solvers that support quantifiers implement a combination of them. Some strategies are *complete*, meaning that they will always enable progress towards unsatisfiability if the formula is indeed unsatisfiable. Let us review the four main approaches to instantiation for SMT.

Of all methods the *enumerative approach* is perhaps the simplest to explain [37,64]. The finite sets of ground terms $\{t_1, \dots, t_n\}$ can be enumerated. Then the enumeration of all the corresponding substitutions results in a complete instantiation procedure, as a straightforward application of Herbrand's Theorem. For the example above, the enumeration might consider the terms $a, b$ and $c$ for the variable $x$, in that order. The instance $P(a) \lor R(a)$ does not make the problem unsatisfiable, but $P(b) \lor R(b)$ does. This method can be made more effective by choosing an appropriate ordering of terms, or basing the search on a refined version of Herbrand's Theorem.

If our goal is to prove that a problem is unsatisfiable, then the *conflict-based approach* is a good option [63,65]. This method looks for instances that contradict the ground problem, such as $P(b) \lor R(b)$ for our example. The other instances are ignored. Successful generation of conflicting instances forces the SAT solver to find a new propositional model, enabling progress. The downside is that finding conflicts is expensive, and may result in too few instances in some cases.

If our goal is to prove that a problem is satisfiable, then *model-based quantifier instantiation* (MBQI) might be a better choice [36,63]. Consider again the example from above; notice that the instance $P(a) \lor R(a)$, while not contradicting the ground problem $E$, is not logically entailed by $E$ either. MBQI targets instances that contradict candidate models for $E$. For instance, a possible model for $E$ might interpret $R$ as the predicate that is always false—that interpretation is possible because all that is known about $R$ is that $\neg R(b)$ is true. But $P(a) \lor R(a)$ contradicts that interpretation (because $\neg P(a)$ holds) so it is generated. MBQI is complete for some fragments of FOL, but it is difficult in general to construct useful models in non trivial satisfiable cases.

The last approach is *E-matching*, which is the most widely used approach for instantiation in SMT [24,63]. Quantified formulas are annotated with patterns, which are usually noted between curly-braces:

$$ \forall x_1, \dots, x_n : \{p_1, \dots, p_k\} \phi $$

The free variables occurring in the patterns $p_i$ must be exactly the variables $x_1, \dots, x_n$. Let $t_1, \dots, t_n$ be terms and $\sigma$ a substitution such that, for all $i$, $E \models p_i\sigma = t_i$ in the theory of EUF. Then $(t_1, \dots, t_n)$ is called a *trigger*, and $\sigma$ can be used to produce an instance lemma. In general, triggers are searched for in the ground problem $E$. For instance, assuming the pattern $\{P(x)\}$ is chosen for our example, then the terms $P(a), P(b)$ and $P(c)$ are all triggers, and three instances are generated. The procedure for detecting triggers is implemented in an effective way by modern SMT solvers [24]. However, the problem of selecting patterns for the quantified formulas is not as easy, and SMT solvers rely on heuristics to generate them [50].
Nevertheless, E-matching is a popular technique among users of SMT, who have the option to select their own triggers for custom axiomatizations [55]. A recurrent problem with the E-matching approach is that it tends to generate too many instances, even sometimes resulting in matching loops (new instances triggering more instances in infinite loops).

This concludes our overview of automated reasoning and SMT. The next part of this chapter concerns TLA⁺, which is a logic based on unsorted set theory. Set theory is a theory of first-order logic, and TLA⁺ also includes symbols from specific theories like integer arithmetic or functions. The high expressiveness of TLA⁺ makes it challenging to encode for SMT solvers, which are better suited for quantifier-free problems. Previous attempts to encode TLA⁺ for SMT relied on preprocessing techniques to eliminate primitive constructs, in particular set-theoretic ones. An important achievement of this thesis is the application of a direct encoding, complemented by axioms with custom E-matching patterns, to handle many proof obligations that were only solved with the help of preprocessing before.

## 2.2 TLA⁺

TLA⁺ is a specification language for modeling computer systems, in particular concurrent and distributed systems [48, 52]. It is based on a variant of Linear Temporal Logic called the Temporal Logic of Actions (TLA), and unsorted set theory. As a formal method, TLA⁺ is similar to the Z notation or Event-B, which are also based on the language of set theory. The core idea underlying TLA⁺ is that first-order logic with temporal modalities is a suitable framework for modeling systems, combining specifications, and refining abstract specifications to lower levels; untyped set theory gives the language more expressiveness [47, 49].

The name “TLA⁺” only refers to the language. Several tools exist to help users with the verification of their TLA⁺ specifications. The main tools are the model checker TLC, which interprets specifications to directly check that they satisfy desired properties [85], and the interactive proof assistant TLAPS, which uses external solvers to mechanically verify proofs written in TLA⁺'s syntax [19]. Some other tools of interest are the symbolic model checker Apalache [46], PlusCal for translating algorithms into TLA⁺ specifications, and the TLA⁺ Toolbox, an Eclipse-based IDE that integrates TLC, TLAPS, and PlusCal.

In this section, we present TLA⁺ and its semantics (Section 2.2.1), demonstrate the basic usage of TLC to verify safety and liveness properties (Section 2.2.2), and introduce the proof syntax and TLAPS (Section 2.2.3). Our work focusses on TLAPS, but it is still worth knowing about TLC, which is useful for verifying finite specifications quickly. Users wanting to check proofs with TLAPS are incited to invoke TLC first, to verify that their specifications are correct at least in the finite case. We will finish this section with a look at the current SMT encoding of TLAPS, which is highly optimized and able to cope with very large proof obligations [53, 81].

For a formal presentation of TLA⁺'s syntax and semantics, we refer the reader to [51]. Our own formalism (Chapter 3) will not include the temporal aspects of TLA⁺'s logic, for reasons that we will make clearer in the present chapter.

### 2.2.1 Specifying Systems

The language of TLA⁺ is based on first-order predicate logic; it includes the usual connectives:

TRUE, FALSE, $\neg A$, $A \Rightarrow B$, $A \land B$, $A \lor B$, $\forall x : P(x)$, $\exists x : P(x)$
MODULE *SimpleClock*

EXTENDS *Naturals*

VARIABLE *hour*

Init $\triangleq$ hour $\in$ 1..12

Increment $\triangleq$ $\land$ hour < 12
             $\land$ hour' = hour + 1

Reset $\triangleq$ $\land$ hour = 12
             $\land$ hour' = 1

Next $\triangleq$ $\lor$ Increment
             $\lor$ Reset

Spec $\triangleq$ Init $\land$ $\Box$[Next]$_{hour}$

<caption>Figure 2.2: Specification of a Simple Clock (Specifying Systems)</caption>

Two extensions of predicate logic are combined to obtain TLA⁺. The first extension is set theory, which includes several primitive operators:

$$ \in, \{e_1, \dots, e_n\}, \text{UNION } S, \text{SUBSET } S, \{x \in S : P(x)\}, \{F(x) : x \in S\}, \dots $$

The operators displayed above are for (in that order) set membership, enumeration set, union of the elements of a set, power set, set comprehension and set replacement. The second extension is TLA. It extends the syntax of FOL with the prime operator $'$, modalities, and quantification over behaviors (flexible variables):

$$ x', \Box A, \Diamond A, \forall x : P(x), \exists x : P(x) $$

We introduce the semantics of TLA⁺ through a practical example: the *SimpleClock* specification, which is inspired by a similar example from TLA⁺'s reference manual [48].

## Specification of a Clock

We specify a clock that tells what *hour* it is. Initially, the hour is some undetermined number between 1 and 12. A clock changes its state by either incrementing the hour value, or resetting it to 1. Which action is taken depends on the current hour (a reset happens iff the current hour is 12). The TLA⁺ specification for this system consists of a single TLA⁺ module, which is shown in Figure 2.2.

Let us describe the different parts of this module. The header simply contains the name of the module. It is immediately followed by the names of the modules to import—here, only *Naturals* is imported, because some arithmetical operators are needed. Then we find declarations, in this case only one for the variable *hour*. The Temporal Logic of Action admits two kinds of variables: *flexible variables* take different values across time, while *rigid variable* have a fixed value. The keyword *VARIABLE* introduces a flexible variable; there are no rigid variables in this specification.

The rest of the specification is just a list of defined expressions, starting with

$$ \mathit{Init} \triangleq \mathit{hour} \in 1..12 $$
The primitive expression `1..12` refers to the set `{i ∈ Int : 1 ≤ i ∧ i ≤ 12}`. Since `hour` is a flexible variable, the truth of `Init` depends on the current state of execution, and we call `Init` a state predicate. A state is simply an assignment of values to the flexible variables of the specification. We represent the state in which `hour` is assigned the value 5 by

$$hour = 5$$

The state predicate `Init` is satisfied by this state. If `hour` is instead assigned the value 0, or 13, or $\sqrt{2}$, then `Init` is not satisfied. TLA⁺ is not a typed language, so the semantics does not assume distinct domains for interpreting variables. Outside of any context, the value of `hour` could be a natural, a real, a set, a Boolean, or something else entirely.

The definition of `Increment` makes use of TLA⁺'s notation for multi-line conjunctions; the expressions prefixed by `∧` on the same level of indentation are part of the same conjunction. The definition is equivalent to

$$Increment \triangleq hour < 12 \land hour' = hour + 1$$

Multi-line disjunctions as in the definition of `Next` are also allowed. The presence of a primed variable makes `Increment` a transition predicate, also called an action. Actions express the relationship between the current state and the next state. For all state expressions `e`, the expression `e'` denotes the value of `e` in the next state of the trace; so `hour'` refers to the next value of `hour`. To evaluate `Increment`, two states are needed. For instance, if `hour = 9` in the current state and `hour = 10` in the next state, we represent this situation by

$$hour = 9 \longrightarrow hour = 10$$

`Increment` is of course satisfied by that pair of consecutive states. In the same spirit, the action `Reset` is satisfied by this transition only:

$$hour = 12 \longrightarrow hour = 1$$

The action `Next` is simply the disjunction of `Increment` and `Reset`, therefore it is satisfied by either of the two situations above.

Lastly, we define the temporal formula `Spec` specifying the whole system:

$$Spec \triangleq Init \land \Box [Next]_{hour}$$

As a temporal formula, `Spec` is interpreted relative to behaviors, which are infinite sequences of states. The predicate `Init` must be true in the first state. The meaning of the second conjunct, $\Box [Next]_{hour}$, is that for all future transitions of the system, either `Next` is true, or `hour' = hour` is true. The latter case is called a *stuttering step*.

Here is the beginning of a behavior satisfying `Spec`:

$$hour = 11 \longrightarrow hour = 12 \longrightarrow hour = 1 \longrightarrow hour = 1 \longrightarrow hour = 2 \longrightarrow \dots$$

`Init` holds in the first state. `Increment` is true for the first transition, then `Reset` for the next, then there is a stuttering step and the last transition satisfies `Increment`.
The possibility of stuttering steps is essential for combining and refining specifications. Given two systems specified by temporal formulas *Spec*<sub>1</sub> and *Spec*<sub>2</sub>, the combination of both systems into a single one is specified by the formula

$$Spec_1 \wedge Spec_2$$

A transition of the whole system is the combination of a transition of *Spec*<sub>1</sub> and a transition of *Spec*<sub>2</sub>. Since transitions include possible stuttering steps, the formula above accounts for transitions in which only one of *Spec*<sub>1</sub> or *Spec*<sub>2</sub> progresses—the other one stutters for this transition. In short, stuttering steps model transitions during which the *environment* of the system may progress. This is essential as components in actual systems may not always progress in a synchronized way. A similar principle applies to refinement, where several transitions of the low-level specification may be necessary to model a single transition of the more abstract specification.

## Specification of a Sorting Algorithm

The *SimpleClock* specification showcases the most basic features of TLA<sup>+</sup>, but there are not many meaningful properties to verify about it. To get a fuller picture of the language, we introduce the *AbstractSorting* module (Figure 2.3), which specifies a sorting algorithm that swaps out-of-order values in an array of integers. We call it abstract because it does not specify an explicit strategy for selecting values to swap.

We import operators from the modules *Naturals* and *Functions*. Besides the variable *a* denoting the array to be sorted, it is parameterized by two constants *N* and *init*. Constants are rigid variables; their values are fixed for all states. *N* is the size of the array and *init* is the initial array.

The specification makes extensive use of TLA<sup>+</sup> functions to represent its data. The primitive construct [*x* ∈ *S* ↦ *e*] that binds *x* in the expression *e* represents a *function* of domain *S*. The domain of a function *f* is a set denoted *DOMAIN* *f*. The value of *f* at *x* is denoted *f*[*x*]. The class of all functions is defined by the predicate

$$f = [x \in \text{DOMAIN } f \mapsto f[x]]$$

The principle of functional extensionality applies: two functions *f* and *g* are equal iff their domains are equal and *f*[*x*] = *g*[*x*] for all *x* in their common domain. The set of functions from set *S* to set *T* is denoted [*S* → *T*].

The functions of TLA<sup>+</sup> are regular objects like sets or integers. In fact, since TLA<sup>+</sup> assumes an unsorted universe of set theory, we may say that all functions are sets. However a TLA<sup>+</sup> function *f* is not equal to its graph {*⟨x, f[x]⟩* : *x* ∈ *DOMAIN* *f*} like it would in Event-B. Furthermore, functions should not be confused with *operators*. A function application is written *f*[*x*] while an operator application is written *F*(*x*), although some operators admit an infix notation, for instance *x* ∪ *y*. All functions have a domain which is a set, while operators may be specified on classes that are not sets. For instance, the operator ∪ is specified for all pairs of sets, but there is no function that corresponds to it, because there can be no set of all sets in ZFC.

*AbstractSorting* involves the particular set

$$\text{ArrayType}(n) \triangleq [1..n \to \text{Int}]$$
### MODULE AbstractSorting

#### EXTENDS Integers, Functions

We specify an abstract sorting algorithm on arrays of integers. The algorithm non-deterministically selects two unordered values to swap at each step of the execution.

CONSTANT $N$, Size of the array
`init` The initial array

VARIABLE $a$ The array

Preliminary Definitions and Assumptions

`ArrayType(n) ⇄ [1 .. n → Int]`

`Swap(f, x, y) ⇄ [f EXCEPT ![x] = f[y], ![y] = f[x]]`

ASSUME NTyping ⇄ $N \in \mathbf{Int} \land N > 0$

ASSUME InitTyping ⇄ $init \in ArrayType(N)$

Main Specification

`Init ⇄ a = init`

`Next ⇄ ∃i, j ∈ DOMAIN a : ∧ i < j 
∧ a[i] > a[j] 
∧ a' = Swap(a, i, j)`

`Spec ⇄ Init ∧ □[Next]ₐ ∧ WFₐ(Next)`

Some relevant properties to verify / prove

`TypingInv ⇄ a ∈ ArrayType(N)`

`g ◦ f ⇄ [x ∈ DOMAIN f ↦→ g[f[x]]]`

`PermutationInv ⇄ ∃p ∈ Bijection(1 .. N, 1 .. N) : a = init ◦ p`

`Sorted(f) ⇄ ∀x, y ∈ DOMAIN f : x < y ⇒ f[x] ≤ f[y]`

THEOREM *Spec* ⇒ □*TypingInv*

THEOREM *Spec* ⇒ □*PermutationInv*

THEOREM *Spec* ⇒ □(*Sorted*(*a*) ⇒ ¬ENABLED *Next*)

THEOREM *Spec* ⇄ *Sorted*(*a*)

<caption>Figure 2.3: Abstract Specification of a Sorting Algorithm</caption>
to represent arrays as functions of the interval 1..n to integers. The keyword ASSUME introduces two (named) assumptions for specifying type constraints on the constant parameters N and init. For swapping two values of a generic function, we introduce the operator Swap with the definition

$$Swap(f, x, y) \triangleq [f \text{ EXCEPT } ![x] = f[y], ![y] = f[x]]$$

That definition involves a primitive operator of TLA⁺ for defining a function differing from another on one or several inputs. If f is a function and z ∈ DOMAIN f, then we have

$$Swap(f, x, y)[z] = \begin{cases} f[y] & \text{if } z = x \\ f[x] & \text{if } z = y \\ f[z] & \text{otherwise} \end{cases}$$

In short, the values at x and y are swapped.

The rest of the specification follows the pattern of defining the state predicate Init, the transition predicate Next, and the temporal formula Spec. Here, Spec contains the additional conjunct WFₐ(Next). The meaning and relevance of this formula will be explained in the next section. The Init predicate specifies that the initial array is init. The Next predicate specifies a transition in which two inputs i and j are selected such that a is unordered at i and j, and a' is obtained by swapping those values. Notice the use of an existential quantifier to specify the non-deterministic selection of i and j.

The middle bar is purely cosmetic; we use it to delimit the actual specification from the relevant properties we want to verify. The keyword THEOREM introduces those properties (these statements have no semantics, they are just here for presentation purposes). Let us explain each of them briefly.

Three properties share the general form *Spec* ⇒ □*P*, which is a way of stating that *P* is an invariant of the specification. Invariants are also called safety properties. The first invariant is a typing invariant stating that *a* is an array of size *N*. TLA⁺ is an untyped language, which means that operators may be combined in unconventional ways; but the semantics of unconventional expressions is not always specified. It is recommended to always express a typing invariant for a specification's variables and verify it. The next safety property, PermutationInv, states that *a* is a permutation of the initial array. The definition involves the operator Bijection, which is defined in the module Functions, and the operator ◦ for composing functions, which we define ourselves.

The third invariant involves the operator ENABLED. For all actions *A*, the expression ENABLED *A* is a state predicate that says a transition specified by *A* is possible from the current state. Thus the property asserts that if *a* is sorted, the system cannot progress.

The fourth property is of the form *Spec* ↛ *P*. This is a notation for □(*Spec* ⇒ ◊*P*), and ◊ is the modal operator for asserting that a property is true in some future state of the behavior. Therefore, the property is understood as the assertion that *a* is eventually sorted (together with the previous property, it follows that the specified sorting algorithm is terminating). Properties asserting that something must eventually happen are called liveness properties.

### 2.2.2 Model Checking with TLC

Model checking is the verification of specifications through the construction and evaluation of their models. TLC is called an explicit-state model checker, because it is based on explicit
<figure><img src="image_5.png" /><figcaption>Figure 2.4: TLC Parameters for the Abstract Sorting Specification</figcaption></figure>

representations of the values of variables of a specification, rather than a symbolic representation. The model checker, which can be invoked from the TLA⁺ Toolbox, exhausts the space of reachable states to verify that all possible behaviors satisfy the desired properties. TLC is useful for detecting bugs in specifications, but it is limited to specifications involving finite data and fixed parameter values.

### Verifying Invariants

A simple configuration for TLC is shown in Figure 2.4. We indicate to TLC that *Init* specifies the initial state and *Next* the transition. We specify the values $N \leftarrow 5$ and *init* $\leftarrow (5, 4, 3, 2, 1)$ (this uses TLA⁺'s notation for tuples, which are the same as functions of a domain $1..n$) for the two parameters of the specification. If we want to specify bounds rather than explicit values for the parameters (for instance, to check for all $N \le 5$), we must write *AbstractSorting* differently—for the sake of simplicity, we will only invoke TLC with two explicit values here.

We indicate to TLC what it should check. The most important parameters are whether we check for *deadlocks* and which *invariants* to verify. If deadlocks are checked, TLC will return an error when a state with no possible transition occurs. If TLC reaches a state violating an invariant, it returns an error. For now, we only verify that *TypingInv* and *PermutationInv* are satisfied in all possible executions; since termination is a desired property in our case, we disable deadlock checking. We wrote one additional invariant and also a temporal formula to verify later. The result of calling TLC is shown in Figure 2.5. The call ended with no errors, so the invariants are indeed satisfied in all reachable states. In total TLC explored 120 distinct states, which corresponds to the number of permutations of a set of five elements.
<figure><img src="image_6.png" /><figcaption>Figure 2.5: Checking Invariants with TLC</figcaption></figure>

<figure><img src="image_7.png" /></figure>

<figure><img src="image_8.png" /><figcaption>Figure 2.6: Checking Violation of Invariants with TLC</figcaption></figure>

## Verifying Liveness Properties

Liveness properties can also be checked by TLC. There is a general method to verify that a state satisfying *P* is reachable which consists in checking that ¬*P* is not an invariant of the specification. For instance, if we run TLC with the instruction to check that ENABLED *Next* is an invariant of *AbstractSorting*, it will return an error upon finding a terminating state, and show the trace of execution. This is equivalent to selecting “deadlocks” in the configuration window.

Suppose we want to check that a terminating state in which *a* is sorted is reachable. The negation of this property is expressed by the formula

$$ \text{Sorted}(a) \Rightarrow \text{ENABLED Next} $$

which is violated exactly when *a* is sorted and no transition is possible. Running TLC, we get an error, and the trace of execution is displayed in Figure 2.6. This trace is actually a minimal sequence of steps to reach the terminating state in which *a* is sorted.

This method is not equivalent to the verification of *Spec* $\rightsquigarrow$ *P*, because by reaching a state violating $\neg P$ we only find *some* path that leads to *P*. To verify the full liveness property, we may ask TLC to check a temporal formula. For instance, to check that the array is eventually sorted, we can simply input $\Diamond \text{Sorted}(a)$ in the last box of TLC's configuration window. This will not work for the present configuration, because the configuration so far uses only the *Init* and *Next* part of the specification and ignores the condition $WF_a(\text{Next})$. With this configuration, an infinite sequence of stuttering steps in which *a* is unchanged is
a legitimate behavior, so the property ◊Sorted(a) is in fact not true. The weak fairness condition WF<sub>a</sub>(Next) prohibits this behavior. Its formal definition is

$$ 
\begin{align*}
WF_a(Next) &\triangleq (◊ \Box ENABLED \langle Next \rangle_a) \Rightarrow \Box ◊ \langle Next \rangle_a \\
\langle Next \rangle_a &\triangleq Next \wedge a' \neq a
\end{align*}
$$

The action $\langle Next \rangle_a$ is a Next step during which the value of a changes. Therefore WF<sub>a</sub>(Next) states that if a non-stuttering step becomes always possible, then it will necessarily happen. After selecting a different option to provide the full formula *Spec* containing the weak fairness condition, and running TLC, we find that the property ◊Sorted(a) is verified as expected.

### 2.2.3 Interactive Proof with TLAPS

Using TLC, we are only able to verify the *AbstractSorting* specification with bounds on *N* and *init*. For the general case, and for specifications that involve infinite sets, we must write proofs and check them using TLAPS.

#### TLA⁺ Proofs

TLA⁺ includes a syntax for proofs based on Lamport's hierarchical style [19]. The syntax is detailed in a note introducing the second version of the language.<fnref n="1" /> We demonstrate it with the module *AbstractSortingSafety* in Figure 2.7. This module contains proofs that the properties *TypingInv* and *PermutationInv* are inductive invariants of the specification.

A theorem is introduced by the keyword *THEOREM*. Those statements may be followed by proofs (the proofs are considered omitted otherwise). The syntax of TLA⁺ proofs is based on a tree structure:

* A leaf is a line of relevant *facts* and *definitions* which are necessary to prove the statement. The facts are introduced by the keyword *BY*. The definitions are introduced by *DEF*. If no facts or definitions are invoked, the proof is written *OBVIOUS*.

* A complex proof is a sequence of *intermediary steps* ending with a *conclusion step* whose statement is *QED*. Each step is a node in the proof structure and must be justified by its own nested proof.

Each step in a proof is introduced by a level indication and an optional label with the notation $\langle level \rangle$ label. The level is a positive number corresponding to the level of nesting in the proof structure. The label is optional and can be any string of ASCII characters, although it is common practice to label steps with natural numbers. The presence of a label has an operational meaning: without a label, the *intermediary step* is implicitly added as a fact for the subsequent steps at the same level and in deeper levels; if a label is present, the step is not implicitly used as a fact, and it must be explicitly invoked when necessary.

This basic syntax suffices to write a proof that *TypingInv* is an invariant of the specification *Spec*. Let us detail the proof of the theorem named *Typing*. Although the full statement is a temporal formula, it is possible to lay out the proof in such a way that most steps can be solved without temporal reasoning. The first step is

$$ Init \Rightarrow TypingInv $$

<footnote n="1">¹http://lamport.azurewebsites.net/tla/tla2-guide.pdf</footnote>
MODULE AbstractSortingSafety

EXTENDS AbstractSorting, TLAPS, Functions, FunctionTheorems

USE NTyping, InitTyping

THEOREM Typing $\triangleq$ Spec $\Rightarrow$ $\Box$TypingInv

⟨1⟩1. Init $\Rightarrow$ TypingInv

BY DEF TypingInv, Init

⟨1⟩2. Next $\wedge$ TypingInv $\Rightarrow$ TypingInv'

BY DEF TypingInv, Next, ArrayType, Swap

⟨1⟩3. UNCHANGED $a \wedge$ TypingInv $\Rightarrow$ TypingInv'

BY DEF TypingInv

⟨1⟩.QED

BY ⟨1⟩1, ⟨1⟩2, ⟨1⟩3, PTL DEF Spec

THEOREM Safety $\triangleq$ Spec $\Rightarrow$ $\Box$PermutationInv

⟨1⟩1. Init $\Rightarrow$ PermutationInv

⟨2⟩.SUFFICES ASSUME $a = init$

PROVE $\exists p \in \text{Bijection}(1..N, 1..N) : a = \text{init} \circ p$

BY DEF Init, PermutationInv, $\circ$

⟨2⟩.[$k \in 1..N \mapsto k$] $\in$ Bijection(1..N, 1..N)

BY Fun_IsBij

⟨2⟩.QED

BY DEF ArrayType, $\circ$

⟨1⟩2. Next $\wedge$ TypingInv $\wedge$ PermutationInv $\Rightarrow$ PermutationInv'

⟨2⟩.SUFFICES ASSUME $a \in [1..N \to Int]$,

NEW $i \in 1..N$, NEW $j \in 1..N$, $a' = \text{Swap}(a, i, j)$,

NEW $p \in \text{Bijection}(1..N, 1..N)$, $a = \text{init} \circ p$

PROVE $\exists q \in \text{Bijection}(1..N, 1..N) : a' = \text{init} \circ q$

BY DEF Next, TypingInv, PermutationInv, ArrayType, $\circ$

⟨2⟩.DEFINE $s \triangleq$ [$k \in 1..N \mapsto \begin{cases} \text{CASE } k = i \to j \\ \quad \Box k = j \to i \\ \quad \Box \text{OTHER} \to k \end{cases}$

⟨2⟩.($p \circ s \in \text{Bijection}(1..N, 1..N)$)

BY Fun_IsBij, $s \in \text{Bijection}(1..N, 1..N)$, Fun_BijTransitive DEF $\circ$

⟨2⟩.QED

BY DEF ArrayType, Swap, $\circ$

⟨1⟩3. UNCHANGED $a \wedge$ PermutationInv $\Rightarrow$ PermutationInv'

BY DEF PermutationInv

⟨1⟩.QED

BY ⟨1⟩1, ⟨1⟩2, ⟨1⟩3, Typing, PTL DEF Spec

<caption>Figure 2.7: Proofs of Two Safety Properties for the Sorting Algorithm</caption>
It is solved simply by expanding the definition of Init and TypingInv. Actually, the proof also requires the assumption init ∈ ArrayType(N), which is named InitTyping in the specification. With the USE command at the beginning of the module, we make sure that the typing assumptions for init and N are always inserted in the proof context.

The second step is the inductive step

$$Next \wedge TypingInv \Rightarrow TypingInv'$$

After expanding the definition of TypingInv', the prime operator is distributed, resulting in the expression a' ∈ ArrayType(N). As a transition predicate, this formula is interpreted for pairs of states; TLAPS reduces this formula to a regular first-order formula by replacing the primed variable a' by a fresh variable. The proof is essentially the verification of

$$Swap(a, i, j) \in ArrayType(N)$$

under the hypothesis a ∈ ArrayType(N) and for i, j ∈ DOMAIN a. This is an elementary verification which only requires expanding the definitions of Swap and ArrayType.

The last intermediary step is for verifying that TypingInv is invariant for stuttering steps:

$$UNCHANGED a \wedge TypingInv \Rightarrow TypingInv'$$

After this, the three steps (1) 1, (1) 2 and (1) 3 are combined to prove the result. The keyword PTL is not a fact, but a pragma to indicate the backend to invoke. “PTL” stands for Propositional Temporal Logic and refers to the LS4 solver [76]. It is typically invoked for a single step involving elementary temporal logic, like in this proof. The other possible backend calls are Isa (for the Isabelle backend), Z3, CVC4, veriT, SMT (for the default SMT solver which may be configured) and Zenon. There are also some variants to specify a different timeout (ZenonT(30)) or a particular Isabelle method (IsaM("auto"), IsaM("force"), IsaM("blast")).

The proof of Safety, which states that PermutationInv is an invariant of the specification, is more involved and features some advanced elements of the proof language. The general structure of the proof is the same: we prove that the invariant is implied by Init, then that it is inductive for Next, for stuttering steps, and we conclude using PTL for the last step. The invariant is proved by constructing a permutation p of 1..N such that a = init ◦ p. In the initial state, p is the identity; for the inductive step, p is updated by composing it with s, which is defined as the permutation that swaps i and j.

The statement of the inductive step features the typing invariant as an hypothesis:

$$Next \wedge TypingInv \wedge PermutationInv \Rightarrow PermutationInv'$$

This is justified by the previously proved result Typing, which is invoked as a lemma for the last step. In general, if Spec ⇒ □P₁ is proved, then it suffices to prove Spec ∧ □P₁ ⇒ □P₂ to deduce Spec ⇒ □P₂.

The first advanced feature of the proof syntax worth noting is the use of the SUFFICES keyword. An intermediary step starting with SUFFICES modifies the current goal of the proof. Formally, assuming the current goal is a formula A, then a step consisting of the statement SUFFICES B corresponds to the obligation B ⇒ A, and replaces the current goal by B for the subsequent steps. Here, we combine SUFFICES with the use of sequents to manage the context of the proof. The general form of a TLA⁺ sequent is

ASSUME $H_1, H_2, \dots$

PROVE A
<figure><img src="image_9.png" /><figcaption>Figure 2.8: Architecture of TLAPS</figcaption></figure>

where A is a formula representing the goal, and each $H_i$ is either a declaration (indicated by the keyword NEW) or a formula representing an hypothesis. A bounded declaration NEW $x \in S$ is just the declaration NEW $x$ followed by the hypothesis $x \in S$. Combining SUFFICES with sequents is the most practical way to reformulate a goal while introducing new symbols and hypotheses.

The keyword DEFINE is used to declare and define a symbol locally. Such steps do not require proofs. Here we use the command to define $s$ as the permutation swapping $i$ and $j$. By default, local definitions are always expanded by TLAPS, so there is no need to include them after a DEF keyword. In complex proofs, it may become necessary to hide definitions; this can be done with the command HIDE DEF in an intermediary step.

The proof of the intermediary step

$$ (p \circ s) \in \textit{Bijection}(1..N, 1..N) $$

involves several facts which are not previous steps of the current proof. The names *Fun_IsBij* and *Fun_BijTransitive* refer to lemmas from the *FunctionTheorems* module. The expression $s \in \textit{Bijection}(1..N, 1..N)$ is an inline, unproved fact for which TLAPS generates an additional proof obligation. The context of that proof obligation is obtained by inserting the previously indicated facts to the current context; here, the lemma *Fun_IsBij*, which states the sufficient conditions for something to be a bijection, is used to prove that $s$ is a permutation of $1..N$. For the main obligation $(p \circ s) \in \textit{Bijection}(1..N, 1..N)$, the two lemmas and the fact about $s$ are used. The lemma *Fun_BijTransitive* states that the composition of two bijections is a bijection.

## TLAPS

The architecture of TLAPS is presented in Figure 2.8. The proof assistant parses a TLA⁺ specification and generates a number of *proof obligations* (PO) from its proofs. Each obligation is *encoded* for one or several of the available backend solvers: Isabelle (using a custom TLA⁺ object logic), Zenon, SMT and PTL. The SMT solvers available are Z3, CVC4 and veriT. By default, TLAPS invokes in a portfolio mode Isabelle, Zenon, and Z3. Users may select a particular backend by using a special keyword in place of an invoked fact. If one of the invoked backends answers positively (if the encoded obligation has been solved), then TLAPS considers the PO to be solved. In other words, the backends are treated as *trusted oracles* by TLAPS, although there is some support for proof verification in the case of Zenon, whose output may be translated and checked by Isabelle.
The preprocessing step that precedes the encoding is common to all backends. Preprocessing includes:

* Insertion of all relevant declarations and facts into the PO's context. Explicitly invoked lemmas, proof steps and inline facts following a `BY` are appended to the current context of the proof for all obligations. Some control is given to the user over which facts are known in the form of the `USE` and `HIDE` command, which can be used at the top level of a specification or inside a proof.

* Expansion of all relevant definitions. By default, top definitions are opaque, but local definitions with `DEFINE` are expanded. Typically, the `DEF` keyword indicates the additional definitions to use for an obligation. The commands `USE DEF` and `HIDE DEF` can be used to override the default behavior of TLAPS for definitions.

* Removal of syntactic sugar. For instance, any expression

$$[f \text{ EXCEPT } ![d_1] = e_1, \dots, ![d_n] = e_n]$$

is rewritten as

$$[\dots [f \text{ EXCEPT } ![d_1] = e_1] \dots \text{ EXCEPT } ![d_n] = e_n]$$

so that `EXCEPT` may be treated as a ternary operator. Another example is multi-argument applications; an application

$$f[x_1, \dots, x_n]$$

is rewritten as

$$f[\langle x_1, \dots, x_n \rangle]$$

* (For backends other than PTL) Elimination of the prime operator. In the simplest case, all primes are found on flexible variables; in this case it suffices to introduce a fresh variable for any $x'$. In general a prime may be found on any expression. TLAPS will distribute the prime operator when possible, for instance $(x+y)'$ is rewritten $x'+y'$. For an expression $F(x)'$ where $F$ is not expanded, TLAPS will replace the whole expression by a fresh identifier.

After preprocessing, the general form of a TLA⁺ proof obligation (in the case of a backend other than PTL) is that of a sequent without temporal connectives or primes. One important omission from our examples is the presence of user-defined second-order operators. Here is an example:

$$F(\mathit{Op}(\_), x) \triangleq \mathit{Op}(x)$$

When the definition of $F$ is not expanded, any expression $F(\mathit{Op}, e)$ is only naturally encoded in second-order logic. Currently, these obligations are only supported by the Isabelle backend, since the logics of Zenon and SMT are first-order. However, a large class of specifications do not require second-order user definitions, so the current support of TLAPS for second-order constructs may suffice for those.
## The SMT Encoding

The SMT backend of TLAPS uses an optimized encoding of TLA⁺ that combines soft type inference and rewriting [53,81]. The usefulness of SMT solvers is recognized in the context of interactive theorem proving supported by automation [9, 29, 32].

The standard input language for SMT solvers is SMT-LIB [6]. As a logic, SMT-LIB is best described as multi-sorted first-order logic (MS-FOL), but the interest of SMT lies in its support for first-order theories. While generic first-order logic is undecidable, some theories have decision procedures, like linear arithmetic or bitvectors. Encoding TLA⁺ in such a way that those procedures can be leveraged is of great interest to the developers of TLAPS, but the fact that TLA⁺ is untyped makes it more challenging. Nevertheless, the current SMT encoding outputs problems expressed in the SMT logic UFNIA (Uninterpreted Functions and Non-linear Integer Arithmetic).

To understand the SMT encoding, it is useful to consider first a direct encoding of TLA⁺. The direct encoding is summed up in the following key ideas:

* A direct, faithful translation of TLA⁺ into MS-FOL is implemented by just declaring every TLA⁺ primitive operator as an uninterpreted symbol in the SMT problem. An uninterpreted sort $\iota$ is declared to receive every term. Some transformations are necessary to recover the Boolean sort (this process is called *Boolification* and achieved in a single pass over the expressions).

* The TLA⁺ primitives, encoded as uninterpreted symbols, are specified by SMT *axioms*. All quantifiers range over the uninterpreted sort $\iota$.

* For arithmetic, we use a different set of *axioms* to specify a correspondence between TLA⁺'s integer arithmetic and SMT's builtin arithmetic.

The support for arithmetic involves a cast operator $\mathit{cast}_{\mathit{int}} : \mathit{int} \to \iota$ and a few *axioms*. One axiom specifies $\mathit{cast}_{\mathit{int}}$ as a bijection between the sort $\mathit{int}$ and the class of sets that are members of $\mathit{Int}$:

$$ \forall x^t : x \in \mathit{Int} \Leftrightarrow \exists n^{\mathit{int}} : x = \mathit{cast}_{\mathit{int}}(n) $$

There are *axioms* to specify a homomorphic relationship between TLA⁺'s arithmetical operators and their SMT counterparts. For instance:

$$ \forall m^{\mathit{int}}, n^{\mathit{int}} : \mathit{cast}_{\mathit{int}}(m) + \iota \mathit{cast}_{\mathit{int}}(n) = \mathit{cast}_{\mathit{int}}(m + \mathit{int} \, n) $$

Despite the integration of SMT's builtin arithmetic, this direct encoding was considered insufficient, essentially because it results in an SMT problem with many uninterpreted symbols and many *axioms* with quantifiers over the uninterpreted sort $\iota$. There were attempts to make the axiomatization efficient with SMT triggers, but they did not lead to satisfactory results. Another problem is the encoding of second-order constructs such as explicit functions $[x \in S \mapsto e]$, which is far from trivial. For these reasons, an extension of the direct encoding was implemented. This optimized encoding is based on a *preprocessing phase* and an optional *type synthesis* mechanism.

The preprocessing phase is centered around a rewriting system. A set of rules are provided for eliminating occurrences of TLA⁺ primitives. For example, an instance of $\cup$ is eliminated by the rule

$$ x \in (a \cup b) \longrightarrow x \in a \lor x \in b $$
The more TLA⁺ primitives we eliminate through rewriting, the better. However, in many situations it is not possible to apply a rewriting rule directly, like in the formula

$$c = (a \cup b) \Rightarrow x \in c$$

Small changes in the structure of expressions can impact the effectiveness of rewriting, which is why rewriting must be complemented by auxiliary techniques. One of these techniques is the elimination of definitions, which eliminates hypotheses of the form $x = e$ by substituting $e$ for $x$ in expressions. Another technique is abstraction, which substitutes parameterized symbols for complex expressions. For instance, the formula

$$(a \cup b) \in d$$

may be rewritten as

$$k(a, b) \in d$$

where $k$ is a fresh symbol defined by $\forall x^t, y^t : k(x, y) = (x \cup y)$. That definition would then be rewritten by an application of set extensionality, which is implemented as the rewriting rule

$$x = y \rightarrow \forall z : z \in x \Leftrightarrow z \in y$$

The second technique is type synthesis, which identifies subexpressions residing in domains of interest (integers, functions, sets, etc.) and assigns them different sorts. Consider the valid TLA⁺ formula

$$\forall x : x \in \mathit{Int} \Rightarrow x + 0 = x$$

According to TLA⁺'s semantics, the variable $x$ ranges over the whole universe of set theory. However, it is clear that only the integer values are relevant (the inner formula is trivially true if $x \notin \mathit{Int}$), so type synthesis will annotate $\forall x$ with the sort int. Since 0 is an integer and the addition of two integers is an integer, it follows that $x + 0$ and $x$ are both integers. The rewriting system will also eliminate the hypothesis $x \in \mathit{Int}$ since it is redundant with the sort of $x$, resulting in the formula

$$\forall x^{\mathit{int}} : x + 0 = x$$

That formula is well-typed in the context of a multi-sorted logic that interprets 0 and + in the domain of integers. However, arbitrary annotations may result in an unsound encoding. Consider the TLA⁺ formula

$$\forall x : x + 0 = x$$

This is a legitimate TLA⁺ formula, but it is not valid, because for instance $FALSE+0 = FALSE$ is unprovable. This time, if we annotate $\forall x$ with int, we obtain a formula that is again well-typed, but also valid. Therefore, the typing of $x$ with int is unsound in this case. In general, type synthesis will look for expressions called *typing hypotheses* to justify the introduction of restrictive sorts. The expression $x \in \mathit{Int}$ is an example of a typing hypothesis.

The previous example suggests that type synthesis may need to integrate some reasoning about TLA⁺'s semantics in order to be practical. The case of TLA⁺ functions proves this is actually necessary: the natural way to type an expression $f[x]$ involves the verification of $x \in \mathit{DOMAIN} f$. Since functions can have any set as domain, any reasonable type system for TLA⁺ must be undecidable.

The SMT backend implements two type systems for TLA⁺, $T_1$ and $T_2$. The encoding that does not use type synthesis is referred to as $T_0$. Both systems are based on the derivation
of typing judgments $\Gamma \vdash e : \tau$ where $e$ is an expression, $\tau$ a type, and $\Gamma$ a typing context (assignment of types to variables). The essential differences between $T_1$ and $T_2$ are seen in their treatment of functional types and applications. The system $T_1$ features elementary sorts and type constructors including the arrow $\tau_1 \to \tau_2$ for functions. The typing rule for applications is expressed

$$ \frac{\Gamma \vdash f : \tau_1 \to \tau_2 \qquad \Gamma \vdash x : \tau_1}{\Gamma \vdash f[x] : \tau_2} $$

The types of $T_1$ do not characterize terms finely enough to capture information such as the domains of functions. For instance, the function $f$ defined as $[i \in \{0, 1, 2\} \mapsto i]$ is assigned the type $\mathbf{int} \to \mathbf{int}$. As a result, a naive application of the typing system might result in the typing of $f[3]$ as an $\mathbf{int}$. But it is not the case that $f[3] \in \mathbf{Int}$. Therefore, to make $T_1$ usable, one has to implement a procedure to verify *type checking conditions* like $x \in \mathbf{DOMAIN} f$.

The system $T_2$ takes a different approach by introducing *dependent* and *refinement types*. These types are expressive enough to characterize the elements of a function's domain. In $T_2$, we have the typing

$$ \vdash [i \in \{0, 1, 2\} \mapsto i] : (i : \{x : \mathbf{int} \mid x = 0 \lor x = 1 \lor x = 2\}) \rightarrow \{y : \mathbf{int} \mid y = i\} $$

The expression $f[3]$ will not be well-typed in $T_2$ because the argument 3 cannot be typed with $\{x : \mathbf{int} \mid x = 0 \lor x = 1 \lor x = 2\}$. The verification of this condition is expressed as part of the typing and verified during the type synthesis mechanism rather than aside from it like in $T_1$.

Despite its efficiency, the SMT encoding has some issues. The first kind of issue concerns the safety, or soundness of the encoding. For instance, testing the encoding with the option `--debug types2` to enable $T_2$ (by default, $T_1$ is enabled), we found that the backend would let us solve the wrong result $[i \in \{0, 1, 2\} \mapsto i][3] \in \mathbf{Int}$. This seems to indicate that the type-checking conditions are not actually verified by the implementation. There are no clear indications in the code's documentation for us to know how to fix this problem.

The soundness of the encoding is also compromised by the substantial complexity of the preprocessing phase. Central to preprocessing is the rewriting system, which is directly implemented in TLAPS. One can easily make a mistake when implementing a rewriting rule, resulting in an unsound encoding. These can be difficult to detect, because one usually writes a proof expecting it to be solved by TLAPS. Nevertheless, we found some examples of unsound rules.<fnref n="2" /> Consider the following rules for simplifying applications:

$$ \begin{array}{l} f[x] \rightarrow \begin{array}{l} \text{IF } x \in \mathbf{DOMAIN} f \text{ THEN } \alpha(f, x) \\ \text{ELSE } \omega(f, x) \end{array} \\ \\ [f \text{ EXCEPT } ![y] = z][x] \rightarrow \begin{array}{l} \text{IF } x \in \mathbf{DOMAIN} f \text{ THEN IF } x = y \text{ THEN } z \\ \text{ELSE } \alpha(f, x) \\ \text{ELSE } \omega([f \text{ EXCEPT } ![y] = z], x) \end{array} \end{array} $$

The symbols $\alpha$ and $\omega$ are two uninterpreted symbols for representing functional application in the final SMT problem. $\alpha$ assumes the application is specified, $\omega$ is for the unspecified

<footnote n="2">²The example we are about to show was found after implementing our own SMT encoding. Comparing the two versions showed a number of proof obligations that were only solved with the original encoding. As it turned out, these obligations were not valid in the first place.</footnote>
case. The two rules are sound, but the second rule was actually implemented with the term $\omega(f, x)$ for the else case. A consequence is that the wrong formula

$$ \forall f, x, y, z : x \neq y \Rightarrow f[x] = [f \text{ EXCEPT } ![y] = z][x] $$

was provable with the SMT backend. The formula is not valid because the assumption $x \in \text{DOMAIN } f$ is missing.

We should point out that the hypothetical direct encoding, which is based on axioms, would suffer from the same problem, because it is easy to make a mistake when coding an axiom in TLAPS's implementation. However, if an axiom is badly implemented, it must be visible in the SMT-LIB problem passed to the solver; one may even narrow the search for the pathological axiom by asking the solver for an unsatisfiable core, if this option is provided. In the case of rewriting, this is not possible, because the point of rewriting is precisely to transform proof obligations to make them simpler.

One aim of the present work is to make the SMT encoding safer. Regarding the state of the original SMT encoding that we just described, we observed that most of the issues stemmed from the complexity of the implementation, in particular the type synthesis algorithm and the preprocessing phase. The direct encoding was considered, but not implemented fully. Our idea then was to revisit the SMT encoding with a more modular design, in which preprocessing (rewriting) could be considered an optimization rather than a necessity. In principle, the direct encoding would not achieve the same performances as the original encoding, but it could be used as a safer version of the SMT encoding.

The next chapter details this direct encoding and presents the arguments for its soundness. In the end, reimplementing type synthesis and preprocessing proved to be unnecessary, as we found a simpler, safer way to optimize the encoding using SMT triggers. The chapter after the next presents that optimization.
# Chapter 3

## Formal Semantics of TLA⁺'s
Constant Fragment

### 3.1 Overview

This chapter develops the formal semantics of TLA⁺'s constant fragment. This fragment excludes all features from temporal logic. The vast majority of TLA⁺ proof obligations are expressed as constant, state or transition formulas; the state and transition formulas are systematically reduced to constant formulas by TLAPS. For the remaining temporal formulas, users are expected to invoke the PTL backend. For the rest of this manuscript, “TLA⁺” will implicitly refer to the constant fragment.

All aspects of the logic are covered in the reference book [48] and the note on TLA⁺ version 2.<fnref n="1" /> However our treatment will be more formal. We define TLA⁺ as a variant of first-order logic (FOL) with the axioms of ZFC set theory. FOL and set theory are both standard frameworks, so it may be helpful to highlight the features that set TLA⁺ apart. We have identified three:

1. There are second-order operators; those can be passed first-order operators or lambda-expressions as arguments;

2. The unsorted logic permits unusual combinations of the operators; an expression like 1/0 is not undefined but underspecified;

3. There is no sort for formulas either; an expression like $42 \Rightarrow 42$ is legitimate.

Underspecification is a central feature of TLA⁺ [39, 49]. To keep the example of 1/0, in the context of underspecification we can write this expression in our specifications, but we may not be able to say anything meaningful about it. We know division on reals is specified by some laws, for instance

$$ \forall x, y \in Real : y \neq 0 \Rightarrow y * (x/y) = x $$

This law will tell us that $0 \neq 0 \Rightarrow 0 * (1/0) = 1$. This is not a very helpful fact, but our only concern for now is to define a precise semantics for untyped operators. As the example of division demonstrates, a natural solution is to avoid interpreting operators and only resort

<footnote n="1">¹http://lamport.azurewebsites.net/tla/tla2-guide.pdf</footnote>
to axioms. All interpretations that satisfy the axioms are legitimate. In some interpretations 1/0 will be a real number, in others it will not.

We formalize TLA⁺ as a logic $\mathcal{L} + T$, where $\mathcal{L}$ is a variant of FOL and $T$ a theory with all the primitive operators and axioms we need. The logic $\mathcal{L}$ extends FOL with second-order operators and a different semantics for Boolean connectives (Section 3.2). The distinction between term and formula is absent in $\mathcal{L}$, so we use the neutral word “expression” instead. The theory $T$ contains the axioms of ZF, the axiom of foundation, and Hilbert’s indefinite choice (also called epsilon-calculus) which trivially implies the axiom of choice (Section 3.3). The theory also includes axioms for functions, arithmetic, and other structures such as tuples and records.

The theorems of TLA⁺ and the proof obligations treated by TLAPS are expressed in the form of sequents (Section 3.4). Sequents technically make the logic second-order, since they offer a way to quantify over first-order operators. However this is a rather obscure feature of the language and it is rarely used in actual proofs. We will discuss sequents in upcoming chapters to address some fine points about the implementation, but for the most part we will only consider the encoding of expressions and take $\mathcal{L} + T$ as source logic.

## 3.2 The Logic $\mathcal{L}$

We introduce some general conventions about notation. If $C$ is a collection, we write $x \in C$ to mean that $x$ is an element of $C$. When we introduce $\in$ as a primitive operator of set theory the symbol will have two different meanings, but it should always be clear in context which meaning is the appropriate one. If $C_1$ and $C_2$ are two collections, we note $C_1 \times C_2$ the collection whose elements are pairs of elements $x \in C_1$ and $y \in C_2$, and $C_1 \to C_2$ the collection of functions $f$ mapping elements $x \in C_1$ to elements $f(x) \in C_2$. If $f$ is any function, the collection Dom($f$) denotes its domain. If $x \in \text{Dom}(f)$ and $v$ is some element, we note $f_v^x$ the function that maps $x$ to $v$ and every $y \in \text{Dom}(f)$ other than $x$ to $f(y)$. We generalize this notation to multiple reassignments by defining $f_v^{x,y}$ as $(f_v^x)^y$.

We fix some infinite collection $\mathcal{V}$. The elements of $\mathcal{V}$ are called variables symbols, or simply variables.

**Definition 3.2.1 (Expressions).** A shape is a finite list of natural numbers $\kappa = (n_1, \dots, n_l)$. If $n_i = 0$ for all $i$ then $\kappa$ is a first-order shape. If $l = 0$ then $\kappa$ is the constant shape. A signature is a function $\Sigma$ from operator symbols to shapes. We note operators with the letter $K$.

The syntax of raw $\Sigma$-expressions and $\Sigma$-arguments is defined by the following grammar:

$$ e ::= x \mid K(f, \dots, f) \mid e = e \mid \text{FALSE} \mid e \Rightarrow e \mid \forall x : e \qquad \text{(Expressions)} $$

$$ f ::= e \mid K \mid \lambda x, \dots, x : e \qquad \text{(Arguments)} $$

where $x \in \mathcal{V}$ and $K \in \text{Dom}(\Sigma)$. An argument $f$ is constant if it is an expression, otherwise it is first-order. An operator $K$ occurring as a first-order argument must have a first-order, non constant shape. The list of variables after a $\lambda$ must be non-empty and without duplicates. An application with zero arguments $K()$ is simply noted $K$.

We assign an *arity* to every raw $\Sigma$-argument $f$. The *arity* of an expression $e$ is 0. The *arity* of a first-order operator $K$ is the length of $\Sigma(K)$. The *arity* of $\lambda x_1, \dots, x_n : e$ is $n$. An application $K(f_1, \dots, f_p)$ is well-formed if $\Sigma(K) = (n_1, \dots, n_p)$ and, for all $1 \le i \le p$, the raw argument $f_i$ has *arity* $n_i$.
We define $\Sigma$-expressions (resp. $\Sigma$-arguments) as raw $\Sigma$-expressions (resp. raw $\Sigma$-arguments) in which all applications are well-formed. We may drop the prefix $\Sigma$- if it is clear in context which signature is considered.

The logical connectives that are not part of the minimalistic grammar of Definition 3.2.1 are introduced as notations:

$$ 
\begin{align*}
\text{TRUE} &\triangleq \text{FALSE} \Rightarrow \text{FALSE} \\
\neg e &\triangleq e \Rightarrow \text{FALSE} \\
e_1 \neq e_2 &\triangleq \neg(e_1 = e_2) \\
e_1 \lor e_2 &\triangleq (\neg e_1) \Rightarrow e_2 \\
e_1 \land e_2 &\triangleq \neg((\neg e_1) \lor (\neg e_2)) \\
e_1 \Leftrightarrow e_2 &\triangleq (e_1 \Rightarrow e_2) \land (e_2 \Rightarrow e_1) \\
\exists x : e &\triangleq \neg(\forall x : \neg e)
\end{align*}
$$

**Example 3.2.2.** Even though the language is unsorted, applications must be well-formed. Let us note $K : \kappa$ to mean that $K$ is assigned the shape $\kappa$ in the relevant signature. Consider a signature $\Sigma$ with a constant symbol $c$, a first-order operator $F : (0)$ and a second-order operator $G : (1, 0)$. Then the following applications are well-formed:

$$ 
\begin{align*}
F(x) \\
F(F(c)) \\
G(F, c) \\
G(\lambda x : F(x), c) \\
G(\lambda y : G(F, y), z)
\end{align*}
$$

The expression $G(F)$ is not well-formed, because $G$ expects two arguments. $F$ and $\lambda x : x$ are not well-formed expressions, but they are well-formed first-order arguments. $G$ is not a first-order argument, it cannot be passed to another operator like $F$ or $\lambda x : x$ can.

Despite the presence of second-order operators and lambda-expressions, most of the features of higher-order logic are absent. For instance $(\lambda x : x)(c)$ is not an expression. Lambda-expressions can appear only as first-order arguments. There are no partial applications either.

**Definition 3.2.3.** In an expression $\forall x : e$, the variable $x$ is said to be bound in $e$. We also say that $e$ is the scope of the quantifier $\forall x$. Similarly, in $\lambda x_1, \dots, x_n : e$, each $x_i$ is bound in the scope $e$. A free variable in an expression or argument is a variable $x$ that occurs outside the scope of a $\forall x$ or $\lambda x_1, \dots, x, \dots, x_n$. The collection $\text{FV}(e)$ (resp. $\text{FV}(f)$) is the collection of the free variables of $e$ (resp. $f$). An expression or argument is called closed if it does not have any free variables.

We now define the semantics of $\mathcal{L}$, which is very similar to the traditional semantics of FOL despite the differences between those two logics. Expressions are assigned values in some indefinite collection $D$, which must at least contain two values for “true” and “false”. The meaning of operator symbols is given by an interpretation $I$. The meaning of free variables is given by a valuation $\theta$.
**Definition 3.2.4 (Evaluation).** A domain is a collection $D$ that includes two distinct elements $\top^D$ and $\bot^D$ called the Boolean values. We assign a domain $D_n$ to every arity $n$ and a domain $D_\kappa$ to every shape $\kappa$ by the following equations:

$$D_0 \triangleq D$$

$$D_n \triangleq D \times \dots \times D \to D \quad (n \text{ occurrences of } D \text{ on the left of } \to)$$

$$D() \triangleq D$$

$$D_{(n_1, \dots, n_p)} \triangleq D_{n_1} \times \dots \times D_{n_p} \to D$$

Let $\Sigma$ be some signature. A $\Sigma$-interpretation $I$ consists of a domain $D$ and a family $(K^I)_{K \in \text{Dom}(\Sigma)}$ such that $K^I \in D_{\Sigma(K)}$ for all $K$. A valuation on $D$ is a function $\theta : \mathcal{V} \to D$. For all $I$ and $\theta$, we define recursively the evaluation $\llbracket \cdot \rrbracket^I_\theta$ of expressions and $n$-ary arguments as follows:

$$\llbracket x \rrbracket^I_\theta \triangleq \theta(x)$$

$$\llbracket K(f_1, \dots, f_n) \rrbracket^I_\theta \triangleq K^I(\llbracket f_1 \rrbracket^I_\theta, \dots, \llbracket f_n \rrbracket^I_\theta)$$

$$\llbracket e_1 = e_2 \rrbracket^I_\theta \triangleq \begin{cases} \top^D & \text{if } \llbracket e_1 \rrbracket^I_\theta = \llbracket e_2 \rrbracket^I_\theta \\ \bot^D & \text{otherwise} \end{cases}$$

$$\llbracket \text{FALSE} \rrbracket^I_\theta \triangleq \bot^D$$

$$\llbracket e_1 \Rightarrow e_2 \rrbracket^I_\theta \triangleq \begin{cases} \top^D & \text{if } \llbracket e_1 \rrbracket^I_\theta \neq \top^D \text{ or } \llbracket e_2 \rrbracket^I_\theta = \top^D \\ \bot^D & \text{otherwise} \end{cases}$$

$$\llbracket \forall x : e \rrbracket^I_\theta \triangleq \begin{cases} \top^D & \text{if } \llbracket e \rrbracket^I_{\theta^x} = \top^D \text{ for all } v \text{ in } D \\ \bot^D & \text{otherwise} \end{cases}$$

For all $v_1, \dots, v_n \in D$:

$$\llbracket K \rrbracket^I_\theta(v_1, \dots, v_n) \triangleq K^I(v_1, \dots, v_n)$$

$$\llbracket \lambda x_1, \dots, x_n : e \rrbracket^I_\theta(v_1, \dots, v_n) \triangleq \llbracket e \rrbracket^I_{\theta^{x_1, \dots, x_n}}$$

The evaluation of $e_1 \Rightarrow e_2$ does not assume that $e_1$ or $e_2$ is evaluated as a Boolean. Similarly for $\forall x : e$. Note that the evaluation of an expression whose top connective is $=$, `FALSE`, $\Rightarrow$ or $\forall$ will always be a Boolean.

**Proposition 3.2.5.** If $e$ is an expression, then $\llbracket e \rrbracket^I_\theta$ is well-defined as an element of $D$. If $f$ is an $n$-ary argument, then $\llbracket f \rrbracket^I_\theta$ is well-defined as an element of $D_n$.

*Proof.* This is proved by induction on the construction of expressions and arguments. The only non-trivial case is the application case. Let $K(f_1, \dots, f_p)$ and $\Sigma(K) = (n_1, \dots, n_q)$. Applications are well-formed by assumption, so $p = q$ and the arity of every $f_i$ is $n_i$. According to the induction hypothesis, $\llbracket f_i \rrbracket^I_\theta \in D_{n_i}$ for all $i$. Since $K^I \in D_{n_1} \times \dots \times D_{n_p} \to D$ by definition, we have $\llbracket K(f_1, \dots, f_p) \rrbracket^I_\theta \in D$. $\square$

**Proposition 3.2.6.** If $x$ is not free in the expression $e$, then $\llbracket e \rrbracket^I_{\theta^x}$ equals $\llbracket e \rrbracket^I_\theta$ for all $\theta$ and $v$. The same holds analogously for arguments.
*Proof.* By induction on the construction of expressions and arguments. In the variable case, the expression must be a variable symbol $y$ such that $y \neq x$; otherwise $x$ would be free in $e$. Thus $\theta_v^x(y) = \theta(y)$. Binder cases are harder; following the definition, we have

$$ \llbracket \forall z : e \rrbracket_{\theta_v^x}^I = \begin{cases} \top^D & \text{if } \llbracket e \rrbracket_{\theta_{v,v'}}^I = \top^D \text{ for all } v' \\ \bot^D & \text{otherwise} \end{cases} $$

It suffices to verify that $\llbracket e \rrbracket_{\theta_{v,v'}}^I = \llbracket e \rrbracket_{\theta_{v'}}^I$. If $x = z$, the two valuations are equal and the result is immediate. If $x \neq z$, we have

$$ \llbracket e \rrbracket_{\theta_{v,v'}}^I = \llbracket e \rrbracket_{\theta_{v',v}}^I = \llbracket e \rrbracket_{(\theta_{v'})^x_v}^I = \llbracket e \rrbracket_{\theta_{v'}}^I $$

where the last equality is justified by the induction hypothesis on $e$ with the valuation $\theta_{v'}^z$. This is possible because $x$ is not free in $e$. Indeed, if $x$ were free in $e$, it would be free in $\forall z : e$ since $z \neq x$. □

**Proposition 3.2.6** justifies the notation $\llbracket e \rrbracket^I$ when $e$ is closed. Since $e$ does not contain any free variables, the values $\theta(x)$ do not matter, and thus $\theta$ itself does not matter in the evaluation.

**Definition 3.2.7 (Satisfiability).** The satisfaction relation $\models$ is defined between interpretations and closed expressions by

$$ I \models e \text{ iff } \llbracket e \rrbracket^I = \top^D $$

Let $T$ be a set of closed expressions. We call $I$ a model of $T$ iff every expression of $T$ is satisfied by $I$. This is written $I \models T$. We note $T \models e$ if $e$ is satisfied by every model of $T$, and $\models e$ in the special case where $T$ is empty. An expression $e$ such that $\models e$ is said to be valid and is called a tautology.

The logic $\mathcal{L}$ is defined by the language of expressions and the satisfaction relation $\models$.

**Example 3.2.8.** Consider again the signature $\Sigma$ of Example 3.2.2. The following expressions are tautologies:

$$ \begin{align*} c &\Rightarrow c \\ G(F, c) &= G(\lambda x : F(x), c) \\ \forall x : x &\Leftrightarrow (x = \text{TRUE}) \end{align*} $$

The lack of a term/formula distinction sets TLA$^+$ apart from most formalisms. It seems unlikely that users would take advantage of that feature. However, experience shows they do so quite naturally. Consider the following expression, which comes from the specification EWD998 from the library of TLA$^+$ Examples:<fnref n="2" />

$$ \mathit{terminationDetected} \in \{\mathit{FALSE}, \mathit{termination}\} $$

where $\in$ and $\cdot, \cdot$ are binary operators. $\mathit{terminationDetected}$ and $\mathit{termination}$ are just constants. With the expected semantics for the pair set, a consequence of the expression above is

$$ \mathit{terminationDetected} \Rightarrow \mathit{termination} $$

<footnote n="2">²https://github.com/tlaplus/Examples</footnote>
This is true even if *termination Detected* and *termination* are not Booleans.

Some consequences of the semantics are stranger, like the tautology 42 ⇒ 42 in a language with numerical constants. Moreover, since the concept of formula does not exist in the logic, any expression can technically play the role of a formula. We have 42 |= 42.

The semantics of Boolean operators is explained in the reference book [48, Section 16.1.3] and also Section 8.1 of the note on TLA⁺ version 2. TLA⁺ actually admits *two* possible interpretations for Boolean connectives, called the *moderate* and the *liberal* interpretation. Our formalism corresponds to the liberal interpretation, which TLAPS officially supports. The advantages of the liberal interpretation is that it is formally very close to FOL, and that it does not impose any constraints on the language of expressions.

## 3.3 The Theory of TLA⁺

The logic $\mathcal{L}$ is a generic framework that fixes the interpretation of the Boolean connectives and also equality. We now turn to the second component of TLA⁺'s logic, which is the theory $T$. First we provide a formal definition for the notation $\mathcal{L} + T$.

**Definition 3.3.1.** Two signature $\Sigma_1$ and $\Sigma_2$ are compatible if their domains do not intersect. We note $\Sigma_1 + \Sigma_2$ the union of two compatible signatures.

**Definition 3.3.2.** A theory (for $\mathcal{L}$) is a set of closed expressions $T$ over some signature $\Sigma_T$. Let $T$ be some theory. We define the logic $\mathcal{L} + T$ as follows:

* A signature of $\mathcal{L} + T$ is a signature of $\mathcal{L}$ compatible with $\Sigma_T$;

* A $\Sigma$-expression of $\mathcal{L} + T$ is a $(\Sigma_T + \Sigma)$-expression of $\mathcal{L}$;

* A $\Sigma$-interpretation is a $(\Sigma_T + \Sigma)$-interpretation that is a model of $T$;

* The evaluation of expression, arguments, and the satisfaction relation are inherited from $\mathcal{L}$.

By definition, an expression $e$ is a tautology in $\mathcal{L} + T$ iff $T \models e$.

Working in $\mathcal{L} + T$ is essentially the same as working in $\mathcal{L}$, only we assume a collection of *primitive operators* in some signature $\Sigma_T$ which are *specified* by the set of axioms $T$.

The rest of this section is an overview of the theory $T$ specifying the primitive operators of TLA⁺. The presentation is organized in several layers: epsilon-calculus, set theory, functions, arithmetic, and others. We will only present the most important fragments of the theory and not always formally. For the complete list of operators and axioms, we refer the reader to Appendix A.

Some axioms are actually axiom schemas. Those schemas are typically parameterized by one or several natural numbers $n$, positive numbers $p$, or operator symbols $K$. The meaning of declaring an axiom schema in $T$ is that the axioms for all values of $n$, $p$ or $K$ are declared in $T$. Thus the collection $T$ must be infinite.
## Epsilon Calculus

The epsilon-calculus has a single operator **choose**: (1). The expression `choose(λx : e)` is usually written `CHOOSE x : e` in TLA⁺'s user syntax. This notation is not general, because the argument to **choose** could be an operator symbol *K*. However, we have the equality `choose(K) = choose(λx : K(x))`, and the second member is represented by `CHOOSE x : K(x)`.

The intuitive semantics of `CHOOSE x : P(x)` is that it selects a value *x* such that *P(x)* is true, if one exists. If no such *x* exists then the expression is unspecified. This is specified by a schema of axioms, where *P* is the parameter.

$$ \forall x : P(x) \Rightarrow P(\mathbf{CHOOSE} x : P(x)) $$

Moreover, a second schema specifies `CHOOSE` as deterministic: if two predicates *P* and *Q* are equivalent then `CHOOSE` selects the same witness for both of them.

$$ (\forall x : P(x) \Leftrightarrow Q(x)) \Rightarrow (\mathbf{CHOOSE} x : P(x)) = (\mathbf{CHOOSE} x : Q(x)) $$

A practical consequence of that last axiom is that we can rewrite expressions below `CHOOSE`. For instance, we have `(CHOOSE x : x \neq x) = (CHOOSE x : FALSE)`.

As a supplement, we define the TLA⁺ constructs for case expressions and if-then-else expressions as notations. The definition below features TLA⁺'s indented notation for multi-line disjunctions, which also exists for conjunctions.

$$ \begin{array}{l} \text{CASE } p_1 \rightarrow e_1, \dots, p_n \rightarrow e_n \\ \triangleq \text{CHOOSE } x : \begin{array}{l} \lor p_1 \land x = e_1 \\ \lor p_2 \land x = e_2 \\ \vdots \\ \lor p_n \land x = e_n \end{array} \\ \text{ELSE} \end{array} $$

$$ \begin{array}{l} \text{CASE } p_1 \rightarrow e_1, \dots, p_n \rightarrow e_n, \text{ OTHER } \rightarrow e \\ \triangleq \text{CASE } p_1 \rightarrow e_1, \dots, p_n \rightarrow e_n, (\neg p_1 \land \dots \land \neg p_n) \rightarrow e \end{array} $$

$$ \begin{array}{l} \text{IF } p \text{ THEN } e_1 \text{ ELSE } e_2 \\ \triangleq \text{CASE } p \rightarrow e_1, \text{ OTHER } \rightarrow e_2 \end{array} $$

Note that if several conditions $p_i$ are true, then a case expression is ambiguous as it may be equal to any $e_i$. Users of TLA⁺ often write case expressions with conditions that obviously exclude each other, so most case expressions are unambiguous in practice.

## Set Theory

We declare the binary operator `in`: `(0,0)`. The expressions `in(x, y)` and `notin(x, y)` are respectively written $x \in y$ and $x \notin y$. TLA⁺'s notations for bounded quantification are defined

$$ \begin{array}{l} \forall x \in e_1 : e_2 \triangleq \forall x : x \in e_1 \Rightarrow e_2 \\ \exists x \in e_1 : e_2 \triangleq \exists x : x \in e_1 \land e_2 \\ \mathbf{CHOOSE} x \in e_1 : e_2 \triangleq \mathbf{CHOOSE} x : x \in e_1 \land e_2 \end{array} $$
The axiom of set extensionality is specified for every object in the domain, in accordance with the view that every mathematical object is a set:

$$ \forall x, y : (\forall z : z \in x \Leftrightarrow z \in y) \Rightarrow x = y $$

The theory admits an operator **subseteq**: (0, 0) for the subset relation. The expression **subseteq**(x, y) is written $x \subseteq y$ and specified by

$$ \forall x, y : x \subseteq y \Leftrightarrow (\forall z : z \in x \Rightarrow z \in y) $$

The rest of the formalization follows the traditional development of ZFC set theory. Here is a summary of the operators of set theory with their shapes and corresponding TLA⁺ notations:

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td>union</td><td>(0)</td><td>UNION e &Delta; union(e)</td></tr><tr><td>subset</td><td>(0)</td><td>SUBSET e &Delta; subset(e)</td></tr><tr><td>enum<sub>n</sub></td><td>(0, ..., 0)</td><td>{e<sub>1</sub>, ..., e<sub>n</sub>} &Delta; enum<sub>n</sub>(e<sub>1</sub>, ..., e<sub>n</sub>)<br/>0 &Delta; enum<sub>0</sub></td></tr><tr><td>setst</td><td>(0, 1)</td><td>{x &isin; e<sub>1</sub> : e<sub>2</sub>} &Delta; setst(e<sub>1</sub>, &lambda;x : e<sub>2</sub>)</td></tr><tr><td>setof<sub>n</sub></td><td>(0, ..., 0, n)</td><td>{e<sub>n+1</sub> : x<sub>1</sub> &isin; e<sub>1</sub>, ..., x<sub>n</sub> &isin; e<sub>n</sub>} &Delta; setof<sub>n</sub>(e<sub>1</sub>, ..., e<sub>n</sub>, &lambda;x<sub>1</sub>, ..., x<sub>n</sub> : e<sub>n+1</sub>)</td></tr><tr><td>cup</td><td>(0, 0)</td><td>e<sub>1</sub> &cup; e<sub>2</sub> &Delta; cup(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>cap</td><td>(0, 0)</td><td>e<sub>1</sub> &cap; e<sub>2</sub> &Delta; cap(e<sub>1</sub>, e<sub>2</sub>)</td></tr><tr><td>diff</td><td>(0, 0)</td><td>e<sub>1</sub> \ e<sub>2</sub> &Delta; diff(e<sub>1</sub>, e<sub>2</sub>)</td></tr></tbody></table>

Note that **enum** and **setof** represent two infinite families of operators, indexed by a natural number *n*. In both cases the shape consists of a list of zeros of length *n*. For **enum** we have $n \ge 0$ while for **setof** we have $n \ge 1$. The ambiguous notation $\{x \in a : x \in b\}$ is interpreted as **setst**(a, $\lambda x : x \in b$).

The operators $\{\cdot\}$ (set enumeration), UNION, SUBSET, $\{x \in \cdot : \cdot\}$ (set comprehension) and $\{\cdot : x \in \cdot\}$ (set replacement) are defined by their axioms and axiom schemas:

$$ \begin{aligned} \forall a, b, x : x \in \{a, b\} &\Leftrightarrow x = a \lor x = b \\ \forall a, x : x \in \text{UNION } a &\Leftrightarrow (\exists y : y \in a \land x \in y) \\ \forall a, x : x \in \text{SUBSET } a &\Leftrightarrow x \subseteq a \\ \forall a, x : x \in \{y \in a : P(y)\} &\Leftrightarrow x \in a \land P(x) \\ \forall a, x : x \in \{F(y) : y \in a\} &\Leftrightarrow (\exists y \in a : x = F(y)) \end{aligned} $$

$P$ and $F$ are operator parameters. We only show the axioms for $enum_2$ and $setof_1$ for the sake of simplicity, but the general schemas for all *n* are easy to infer.

The operators $\cup$, $\cap$ and $\setminus$ can be specified in two ways. The first solution is to give an axiom that characterizes the elements of each set, for instance:

$$ \forall a, b, x : x \in a \cup b \Leftrightarrow x \in a \lor x \in b $$

The second solution is to provide an actual definition for the set:

$$ \forall a, b : a \cup b = \text{UNION} \{a, b\} $$
Both solutions are easily shown equivalent. We prefer the second solution for defining $T$, as it makes clear that the additional operators do not make the theory stronger. The following definitions are admitted:

$$a \cup b \triangleq \text{UNION} \{a, b\}$$

$$a \cap b \triangleq \{x \in a : x \in b\}$$

$$a \setminus b \triangleq \{x \in a : x \notin b\}$$

So far our axioms make $T$ correspond to the theory ZF minus the axiom of infinity. The final theory contains that axiom and also the axiom of foundation:

$$\exists x : \emptyset \in x \land \forall y : y \in x \Rightarrow y \cup \{y\} \in x \quad (\text{Inf})$$

$$\forall x : x \neq \emptyset \Rightarrow \exists y : y \in x \land y \cap x = \emptyset \quad (\text{AF})$$

The resulting theory corresponds to ZFC + AF, where C represents the axiom of choice:

$$\forall x : \emptyset \notin x \land (\forall y, z \in x : y \neq z \Rightarrow y \cap z = \emptyset) \Rightarrow \quad (\text{AC})$$

$$\exists u : \forall v \in x : \exists w : u \cap v = \{w\}$$

The axiom (AC) is independent from ZF + AF, but in the context of the epsilon-calculus it can be proved. Given a set $x$ whose elements are non-empty sets all disjoint to each other, we can define

$$u \triangleq \{(\text{CHOOSE } y : y \in v) : v \in x\}$$

Let $v \in x$ and $w \triangleq \text{CHOOSE } y : y \in v$. Since $\emptyset \notin x$ we have $w \in v$, thus $w \in u \cap v$. Now suppose $w' \in u \cap v$. Then there exists a $v' \in x$ such that $w' = \text{CHOOSE } y : y \in v'$. Since $w' \in v$ and all elements of $x$ are disjoint, we have $v' = v$, thus $w' = w$. Therefore $u \cap v = \{w\}$.

## Functions

Functions are defined axiomatically in TLA⁺. The class of functions is identified by a unary operator `isafcn`, which is not part of the user syntax. Here is a summary of the most important operators:

<table><thead><tr><th>Operator</th><th>Shape</th><th>Notation</th></tr></thead><tbody><tr><td><code>isafcn</code></td><td>(0)</td><td></td></tr><tr><td><code>fn</code></td><td>(0, 1)</td><td>[<i>x</i> &isin; <i>e</i><sub>1</sub> &mapsto; <i>e</i><sub>2</sub>] &triangleq <code>fn</code>(<i>e</i><sub>1</sub>, &lambda;<i>x</i> : <i>e</i><sub>2</sub>)</td></tr><tr><td><code>domain</code></td><td>(0)</td><td><code>domain</code> <i>e</i> &triangleq <code>domain</code>(<i>e</i>)</td></tr><tr><td><code>fnapp</code></td><td>(0, 0)</td><td><i>e</i><sub>1</sub>[<i>e</i><sub>2</sub>] &triangleq <code>fnapp</code>(<i>e</i><sub>1</sub>, <i>e</i><sub>2</sub>)</td></tr><tr><td><code>arrow</code></td><td>(0, 0)</td><td>[<i>e</i><sub>1</sub> &rarr; <i>e</i><sub>2</sub>] &triangleq <code>arrow</code>(<i>e</i><sub>1</sub>, <i>e</i><sub>2</sub>)</td></tr></tbody></table>

Functions are built using the constructor `[<i>x</i> &isin; <i>e</i><sub>1</sub> &mapsto; <i>e</i><sub>2</sub>]`. The domain of a function *f* is accessed through `domain`. The value at *x* is *f*[*x*]. This is specified by the following axioms:

$$\forall a : \text{isafcn}([x \in a \mapsto F(x)])$$

$$\forall a : \text{domain} [x \in a \mapsto F(x)] = a$$

$$\forall a, x : x \in a \Rightarrow [z \in a \mapsto F(z)][x] = F(x)$$

where *F* is an operator parameter.
Two functions with the same domain and the same values on that shared domain are specified as equal. This is the principle of functional extensionality, which is formally written

$$ 
\begin{array}{l}
\forall f, g : \mathit{isafcn}(f) \wedge \mathit{isafcn}(g) \\
\qquad \wedge \mathit{DOMAIN} f = \mathit{DOMAIN} g \\
\qquad \wedge (\forall x : x \in \mathit{DOMAIN} f \Rightarrow f[x] = g[x]) \\
\qquad \Rightarrow f = g
\end{array}
$$

Finally, the set of functions from $a$ to $b$, written $[a \to b]$, is specified by

$$ 
\begin{array}{l}
\forall a, b, f : f \in [a \to b] \Leftrightarrow \mathit{isafcn}(f) \\
\qquad \wedge \mathit{DOMAIN} f = a \\
\qquad \wedge (\forall x : x \in a \Rightarrow f[x] \in b)
\end{array}
$$

In TLA⁺'s reference book, the operator `isafcn` has an actual definition:

$$ \mathit{isafcn}(f) \triangleq f = [x \in \mathit{DOMAIN} f \mapsto f[x]] $$

The proposition below justifies our approach.

**Proposition 3.3.3.** The following TLA⁺ expressions are equivalent:

(i) $\mathit{isafcn}(f)$

(ii) $f = [x \in \mathit{DOMAIN} f \mapsto f[x]]$

(iii) $f \in [\mathit{DOMAIN} f \to \mathit{Im}(f)]$ where $\mathit{Im}(f) \triangleq \{f[x] : x \in \mathit{DOMAIN} f\}$

(iv) $\exists a, b : f \in [a \to b]$

*Proof.* We prove (i) $\Rightarrow$ (ii) using extensionality on $f$ and $[x \in \mathit{DOMAIN} f \mapsto f[x]]$. Both objects are in the class `isafcn`, have `DOMAIN f` for domain, and $f[x]$ for value at $x \in \mathit{DOMAIN} f$. Therefore, they are equal.

For proving (ii) $\Rightarrow$ (iii), it suffices to prove $[x \in \mathit{DOMAIN} f \mapsto f[x]] \in [\mathit{DOMAIN} f \to \mathit{Im}(f)]$. This follows from the axioms of functions and the axiom of set replacement.

The proof of (iii) $\Rightarrow$ (iv) is trivial. (iv) $\Rightarrow$ (i) follows from the axiom specifying $[a \to b]$. $\square$

<figure><img src="image_10.png" /></figure>

The equivalence (i) $\Leftrightarrow$ (ii) demonstrates that our formalization is compatible with the reference book. The proposition above presents two other possible definitions, both of which use the notion of sets of functions. (iii) is only more precise than (iv). Note that if $f \in [a \to b]$, then $a$ is necessarily `DOMAIN f`, whereas $b$ can be any set that contains $\mathit{Im}(f)$.

## Arithmetic

TLA⁺ includes the arithmetics of naturals, integers and reals. The three sets *Nat*, *Int* and *Real* are defined with their intended structure in such a way that *Nat* ⊆ *Int* ⊆ *Real*. The numerical constants and operations of arithmetic are overloaded for the structures in which they are specified. For instance, 1 is specified as an element of *Nat*, but as an element of *Int* or *Real* it still represents the same number. Likewise, the operation 1 + 1 = 2 can be carried out in *Nat*,
but + is also specified as addition on Int and Real, and those three possible interpretations of + coincide.

The construction of the three structures is detailed in the reference book [48, Section 18.4]. We will not reproduce it here as it is both tricky and not important for our purposes. We simply provide the list of operators with some clarifications around their semantics:

* The constants 0, 1, 2, etc. are specified as elements of Nat. Non-negative decimal constants like 3.14 are specified as elements of Real.

* The operator $\leq$ is specified on all sets. The following definitions hold for all $x$ and $y$:

$$x < y \triangleq x \leq y \land x \neq y$$

$$x \geq y \triangleq y \leq x$$

$$x > y \triangleq y \leq x \land x \neq y$$

* The operators $+$, $-$ (unary and binary versions), $*$ and $\hat{}$ are specified on all sets. There are no numerical constants for negative numbers; $-1$ is defined as $-(1)$.

* The operator `/` is division on Real.

* The operators $\div$ and $\%$ are the Euclidean quotient and remainder. They are defined for all $a \in \text{Int}$ and $b \in \text{Nat} \setminus \{0\}$ and satisfy the equations

$$a = b * (a \div b) + (a \% b)$$

$$0 \leq (a \% b) \land (a \% b) < b$$

The last operator we need to introduce is `range`: `(0, 0)`. The expression `range(m, n)` is noted $m..n$ in TLA⁺. It represents the interval of integers between $m$ and $n$ (included). Its definition is

$$m..n \triangleq \{p \in \text{Int} : m \leq p \land p \leq n\}$$

## Other Constructs

The set `BOOLEAN` is defined by

$$\text{BOOLEAN} \triangleq \{\text{TRUE}, \text{FALSE}\}$$

Tuples are defined from functions and Cartesian products are sets of tuples:

$$\langle x, y \rangle \triangleq [i \in 1..2 \mapsto \begin{cases} \text{CASE } i = 1 \text{ THEN } x \\ \text{CASE } i = 2 \text{ THEN } y \end{cases}]$$

$$a \times b \triangleq \{\langle x, y \rangle : x \in a, y \in b\}$$

The general constructs $\langle x_1, \dots, x_n \rangle$ and $a_1 \times \dots \times a_n$ are defined in the same manner. Note that tuples are defined for all $n$, but Cartesian products are only defined for $n \geq 2$, because there are no notations for $n = 0$ or $n = 1$.

For every string of ASCII characters, for example "foo", there is a TLA⁺ constant "foo". All those constants are specified as elements of some set `STRING`. Furthermore, "foo" is
specified to be a tuple of length 3 whose components are unspecified objects representing the characters *f*, *o* and *o*, in that order. Thus “foo”[2] = “foo”[3], and “foo”[1] ≠ “foo”[2].

Records and sets of records are defined in a way analogous to tuples. The domain of a record is a finite set of strings:

$$ 
\begin{align*}
[foo \mapsto x, bar \mapsto y] &\triangleq [s \in \{\text{"foo"}, \text{"bar"}\} \mapsto \begin{array}{l} \text{CASE } s = \text{"foo"} \text{ THEN } x \\ \text{CASE } s = \text{"bar"} \text{ THEN } y \end{array}] \\
[foo : a, bar : b] &\triangleq \{[foo \mapsto x, bar \mapsto y] : x \in a, y \in b\}
\end{align*}
$$

The list of fields can be of any length *n* > 0 but must not contain duplicates.

## 3.4 Sequents

The logic $\mathcal{L} + T$ is adequate to study TLA⁺. However, the proof obligations generated by TLA⁺ are expressed in the form of sequents, which are not part of that logic.

**Definition 3.4.1 (Sequents).** We define contexts and sequents using the following grammar:

$$ \Gamma ::= \cdot \mid \Gamma, \text{NEW } K : \kappa \mid \Gamma, e \mid \Gamma, S \qquad (\text{Contexts}) $$

$$ S ::= \Gamma \vdash e \qquad (\text{Sequents}) $$

The expressions *e* and sequents *S* that occur in a context are called *hypotheses*. The expression *e* after $\vdash$ is called the *goal*. The subexpressions NEW *K*: $\kappa$ are *declarations*, and we impose two constraints on them: there can be at most one declaration of a given *K*, including in nested sequents; the shape $\kappa$ must be first-order.

Every context $\Gamma$ can be naturally treated as a signature by taking Dom($\Gamma$) as the collection of symbols *K* such that NEW *K*: $\kappa$ is in $\Gamma$ and then $\Gamma(K) \triangleq \kappa$. Let $\Sigma$ be a signature. By definition, $\Sigma$ and $\Gamma$ are compatible iff Dom($\Sigma$) and Dom($\Gamma$) are disjoint. In that case $\Sigma + \Gamma$ is defined as a signature.

Given a signature $\Sigma$, we define well-formedness for contexts and sequents:

* The empty context $\cdot$ is always well-formed;

* $\Gamma, \text{NEW } K: \kappa$ is well-formed iff $\Gamma$ is well-formed and $K \notin \text{Dom}(\Gamma)$;

* $\Gamma, e$ is well-formed iff $\Gamma$ is and $e$ is a well-formed ($\Sigma + \Gamma$)-expression;

* $\Gamma, S$ is well-formed iff $\Gamma$ is well-formed and $S$ is a well-formed sequent in the context of the signature $\Sigma + \Gamma$;

* The sequent $\Gamma \vdash e$ is well-formed iff the context $\Gamma, e$ is.

In the syntax of TLA⁺, a declaration NEW *K*: (0, 0) is written NEW $K(\_, \_)$, and similarly for shapes of any length. If the declared *K* is constant we just write NEW *K*. A sequent $\Gamma \vdash e$ is written ASSUME $\Gamma$ PROVE *e*. The notation NEW $x \in e$ is short for the declaration NEW *x* followed by the hypothesis *x* ∈ *e*.
**Example 3.4.2.** Here is an example of a TLA⁺ sequent:

$$
\begin{array}{lcl}
\text{ASSUME} & \text{NEW} & P(\_), \\
             &             & \text{NEW } S, \\
             &             & \text{NEW } x \in S, \\
             &             & P(x) \\
\text{PROVE} & \{y \in S : P(y)\} & \neq \emptyset
\end{array}
$$

Suppose the sequent above corresponds to the statement of a theorem named *MyThm* which has been proved by the user. That result may be invoked in proofs further down the specification. For instance, one may want to prove {$n \in Nat : n > 100$} $\neq \emptyset$ from *MyThm* and the fact $101 > 100$. This will result in an obligation with one nested sequent:

$$
\begin{array}{lcl}
\text{ASSUME} & \text{ASSUME} & \text{NEW } P(\_), \\
             &             & \text{NEW } S, \\
             &             & \text{NEW } x \in S, \\
             &             & P(x) \\
\text{PROVE} & \{y \in S : P(y)\} & \neq \emptyset, \\
             & 101 > 100 & \\
\text{PROVE} & \{n \in Nat : n > 100\} & \neq \emptyset
\end{array}
$$

The idea of the proof is to instantiate *P* with the higher-order argument $\lambda n : n > 100$. This demonstrates how second-order logic becomes necessary for some proof obligations.

**Definition 3.4.3 (Satisfaction for Sequents).** Let $\Sigma$ be a signature, $I$ a $\Sigma$-interpretation, and $\Gamma$ a context well-formed under $\Sigma$. A $\Gamma$-extension of $I$ is a $(\Sigma + \Gamma)$-interpretation $I'$ on the same domain and such that $K^{I'} = K^I$ for all $K \in \text{Dom}(\Sigma)$.

A sequent $\Gamma \vdash e$ is satisfied by $I$ if every $\Gamma$-extension of $I$ that is a model of the hypotheses in $\Gamma$ also satisfies $e$. This is noted $I, \Gamma \models e$. The sequent is called valid if it is satisfied by all interpretations; we note this $\Gamma \models e$.

Contexts are similar to theories as they contain the declarations of a signature and the expressions of a collection of axioms. We view contexts as a way to encode explicit information about a theory: a backend solver taking the encoded obligations as input does not have access to the theory *T*, so we must select relevant declarations and axioms to insert in $\Gamma$. Since *T* is infinite and ZF cannot be characterized by a finite number of axioms, encodings of TLA⁺ into first-order logic are necessarily incomplete.
# Chapter 4

# A Direct Encoding of TLA⁺ into
## Higher-order Logic

### 4.1 Overview

In the previous chapter, we formalized TLA⁺ as a logic $\mathcal{L} + T$, where $\mathcal{L}$ is a variant of FOL without formulas and $T$ is a standard theory on top of $\mathcal{L}$. While TLA⁺ is essentially a first-order logic, it features second-order applications. Moreover, if we consider the language of sequents, we have to account for second-order quantifiers. For these reasons, the most natural encoding of TLA⁺ is an encoding into HOL. This chapter describes that encoding, which has been implemented in TLAPS in the form of the Zipperposition backend [27].

Figure 4.1 shows a diagram of the different steps of the encoding. The logic $\mathcal{L}^t$ is a sorted variant of $\mathcal{L}$ (Section 4.2), and $T'$ is the result of encoding $T$ into $\mathcal{L}^t$. The first step of the encoding is a simple pass over expressions to recover the usual semantics for Boolean connectives (Section 4.3). It is described as a sound and complete encoding of $\mathcal{L}$ into $\mathcal{L}^t$. The optional rewriting step, which is adapted from the original SMT encoding, attempts to eliminate the primitive TLA⁺ constructs of set theory, functions, arithmetic (Section 4.4). We provide its definition as a rewriting system and prove its termination and confluence. The axiomatization step inserts explicit declarations and axioms in the obligation's context (Section 4.5). The last step is a direct translation of sequents in the TPTP language, more precisely the THF dialect (Section 4.6). We conclude this chapter by an evaluation of the encoding on a large set of TLA⁺ specifications (Section 4.7).

**Example 4.1.1.** To illustrate each step of the encoding, we introduce a running example. It is based on the following TLA⁺ definition of sets of partial functions:

$$PFunc(A, B) \triangleq \text{UNION} \{[X \to B] : X \in \text{SUBSET } A\}$$

The elements of a set $PFunc(A, B)$ can be characterized without any reference to set replacement or union:

$$f \in PFunc(A, B) \Leftrightarrow \begin{array}{l} \wedge f \in [\text{DOMAIN } f \to B] \\ \wedge (\text{DOMAIN } f) \subseteq A \end{array}$$

We will focus on the obligation corresponding to the $\Leftarrow$ direction of that equivalence. Figure 4.2 shows a working snippet of code in TLA⁺ with the definition and the proved
TLA$^{+}$ Proof Obligation

<figure><img src="image_11.png" /></figure>

Disambiguate terms and formulas

Eliminate primitive operators

Append explicit declarations and axioms

Translate directly

<figure><img src="image_12.png" /><figcaption>Figure 4.2: Running Example</figcaption></figure>
result. The keyword *Zipper* in the proof line invokes the Zipperposition backend that is based on our encoding.

TLAPS generates a single proof obligation by expanding the definition of *PFunc* in the original sequent. To clarify the structure of expressions, we will use our notations for TLA⁺'s primitive constructs. Without the readable TLA⁺ notations, the proof obligation is written:

ASSUME NEW A, NEW B, NEW f,
  in(f, arrow(domain(f), B)),
 subseteq(domain(f), A)

PROVE in(f, union(setof<1>(subset(A), λX : arrow(X, B))))

## 4.2 The Logic $\mathcal{L}^s$

We view $\mathcal{L}^s$ as a fragment of a more general logic $\mathcal{L}^s$, which is defined in this section. $\mathcal{L}^s$ is a multi-sorted version of $\mathcal{L}$ enjoying the traditional semantics for Boolean connectives. For the TPTP encoding, we use only one sort other than the Boolean sort, which is noted $\iota$ and called the sort of *individuals*. In the next chapter about the SMT encoding, we will add the sort int for integer numbers.

Much of the content of this section is adapted from Section 3.2 on the logic $\mathcal{L}$. The major differences consist in the presence of sort annotations for bound variables, and the restriction of expressions by a type system. Additionally, we introduce *substitutions* and define the substitution of free variables as an operation on terms of $\mathcal{L}^s$.

### Syntax

**Definition 4.2.1 (Types).** Let $S$ be a non-empty collection and $o$ a symbol not in $S$. The elements of $S$ are called *sorts* and $o$ is the *Boolean sort*. Types are defined by the grammar

$$ \tau ::= s \mid \tau \times \dots \times \tau \to s \quad \text{where } s \in S \cup \{o\} $$

The order of a type is defined by

$$ \begin{gathered} \operatorname{ord}(s) \triangleq 0 \\ \operatorname{ord}(\tau_1 \times \dots \times \tau_n \to s) \triangleq \max_{1 \le i \le n} (\operatorname{ord}(\tau_i)) + 1 \quad \text{when } n > 0 \end{gathered} $$

A sort is also a type of order 0. When $\tau = \tau_1 \times \dots \times \tau_n \to s$ and $n = 0$, we write $\tau = s$ and we have $\operatorname{ord}(\tau) = 0$. The types of order 1 and 2 are respectively called first-order and second-order types.

For $\mathcal{L}^s$, we will not consider types of order greater than 2. Our syntax for TLA⁺ was based on two syntactical classes: $e$ for expressions and $f$ for arguments. In $\mathcal{L}^s$, well-formed expressions are assigned a sort; well-formed arguments are assigned a type $\tau$ such that $\operatorname{ord}(\tau) \le 1$. The sorts and first-order types characterize arguments, so we call them *argument types*.

**Definition 4.2.2 (Expressions).** A signature in $\mathcal{L}^s$ is a map $\Sigma$ from operator symbols to types; if $K \in \operatorname{Dom}(\Sigma)$ then $\Sigma(K)$ is a type. The new syntax of expressions and arguments is
$$ \frac{\Gamma(x) = s}{\Gamma \vdash x : s} \quad \frac{\Sigma(K) = \tau_1 \times \dots \times \tau_n \to s}{\Gamma \vdash K(f_1, \dots, f_n) : s} \quad \frac{\Gamma \vdash f_i : \tau_i}{\Gamma \vdash e_1 : s} \quad \frac{\Gamma \vdash e_2 : s}{\Gamma \vdash e_1 = e_2 : o} \quad \frac{\Gamma \vdash e_1 : s}{\Gamma \vdash e_1 \Rightarrow e_2 : o} \quad \frac{\Gamma, x : s \vdash e : o}{\Gamma \vdash (\forall x^s : e) : o} \quad \frac{\Gamma, x_1 : s_1, \dots, x_n : s_n \vdash e : s}{\Gamma \vdash (\lambda x_1^{s_1}, \dots, x_n^{s_n} : e) : s_1 \times \dots \times s_n \to s} $$

<caption>Figure 4.3: Typing Rules for $\mathcal{L}^s$</caption>

defined by the grammar

$$ e ::= x \mid K(f, \dots, f) \mid e = e \mid \text{FALSE} \mid e \Rightarrow e \mid \forall x^s : e \quad \text{(Expressions)} $$

$$ f ::= e \mid K \mid \lambda x^s, \dots, x^s : e \quad \text{(Arguments)} $$

A *typing context* is a map $\Gamma$ from some finite collection of variables to sorts. We note $\Gamma, x : s$ the updated context that maps $x$ to $s$. We define two kinds of *typing judgments*:

* $\Gamma \vdash e : s$ means the expression $e$ has sort $s$;

* $\Gamma \vdash f : \tau$ where $\text{ord}(\tau) \le 1$ means the argument $f$ has type $\tau$.

We note $\vdash e : s$ and $\vdash f : \tau$ when the typing context is empty. The valid typing judgments are defined by the inductive rules of Figure 4.3. An expression or argument is well-formed in some typing context if it has a typing with that context. A *formula* is a well-formed expression whose sort is *o*. A *predicate* is a well-formed argument whose type ends with *o*.

**Example 4.2.3.** We note $K : \tau$ to mean that the operator $K$ has type $\tau$ in some signature. Consider a signature $\Sigma$ with operators $c : s$, $F : s \to s$ and $G : (s \to s) \times s \to s$. Then the term

$$ G(F, c) = G(\lambda x^s : F(x), c) $$

is a well-formed formula. This is shown by the following derivation:

$$ \frac{\frac{\frac{\Sigma(F) : s \to s}{\vdash F : s \to s} \quad \frac{\Sigma(c) : s}{\vdash c : s} \quad \frac{\frac{\Sigma(F) : s \to s}{\vdash c : s} \quad \frac{\Sigma(c) : s}{\vdash (\lambda x^s : F(x)) : s \to s} \quad \frac{\Sigma(c) : s}{\vdash (\lambda x_1^{s_1}, \dots, x_n^{s_n} : e) : s_1 \times \dots \times s_n \to s}}{\frac{\frac{\Sigma(F) : s \to s}{\vdash F : s \to s} \quad \frac{\Sigma(c) : s}{\vdash c : s} \quad \frac{\frac{\Sigma(F) : s \to s}{\vdash c : s} \quad \frac{\Sigma(c) : s}{\vdash (\lambda x^s : F(x), c) : s}}{\frac{\Sigma(F) : s \to s}{\vdash G(F, c) : s}} \quad \frac{\frac{\Sigma(c) : s}{\vdash c : s} \quad \frac{\frac{\Sigma(c) : s}{\vdash (\lambda x^s : F(x), c) : s}}{\frac{\Sigma(F) : s \to s}{\vdash G(F, c) = G(\lambda x^s : F(x), c) : o}}}}{\frac{\Sigma(F) : s \to s}{\vdash G(F, c) = G(\lambda x^s : F(x), c) : o}}}{\frac{\Sigma(F) : s \to s}{\vdash G(F, c) : s}}$$

In the example above, the typing $\vdash c : s$ is derived from the rule APP, because a constant by itself is read as an application with zero arguments. The same judgment cannot be derived with the rule OPARG because the condition $\text{ord}(\tau) = 1$ does not hold for constants.

Let $\Gamma_1$ and $\Gamma_2$ be two typing contexts. We write $\Gamma_1 \subseteq \Gamma_2$ when $\text{Dom}(\Gamma_1) \subseteq \text{Dom}(\Gamma_2)$ and $\Gamma_1(x) = \Gamma_2(x)$ for all $x \in \text{Dom}(\Gamma_1)$. Clearly, any valid typing derivation stays valid when the context $\Gamma$ is extended with fresh variables in every node. This is expressed by the following property, which we admit:

**Proposition 4.2.4.** Suppose $\Gamma_1 \subseteq \Gamma_2$. Then $\Gamma_1 \vdash e : s$ implies $\Gamma_2 \vdash e : s$ for all $e$, and $\Gamma_1 \vdash f : \tau$ implies $\Gamma_2 \vdash f : \tau$ for all $f$.
### Substitutions

If $F(x, y, z)$ (for example) is a term with free variables $x, y, z$, and $t_1, t_2, t_3$ are three other terms, then the term $F(t_1, t_2, t_3)$ is the result of a syntactical operation called substitution.

**Definition 4.2.5 (Substitution).** Let $\Gamma$ be a typing context. A substitution is a function that assigns terms to variables. A substitution $\sigma$ is adequate for $\Gamma$ if $\text{Dom}(\sigma) \subseteq \text{Dom}(\Gamma)$ and $\Gamma \vdash \sigma(x) : \Gamma(x)$ for all $x$. If the domain of $\sigma$ is strictly included in $\Gamma$, $\sigma$ may be naturally extended to the whole context by defining $\sigma(x) = x$.

Let $e$ be a term well-formed in $\Gamma$. A substitution $\sigma$ is compatible with $e$ if no bound variable of $e$ occurs free in a term $\sigma(x)$. In that case, we define the application of $\sigma$ to $e$, which is a term noted $e\sigma$, by recursion on $e$:

$$ 
\begin{align*}
x\sigma &\triangleq \sigma(x) \\
K(f_1, \dots, f_n)\sigma &\triangleq K(f_1\sigma, \dots, f_n\sigma) \\
(e_1 = e_2)\sigma &\triangleq (e_1\sigma) = (e_2\sigma) \\
\text{FALSE}\sigma &\triangleq \text{FALSE} \\
(e_1 \Rightarrow e_2)\sigma &\triangleq (e_1\sigma) \Rightarrow (e_2\sigma) \\
(\forall x^s : e)\sigma &\triangleq \forall x^s : e\sigma^x
\end{align*}
$$

$$ 
\begin{align*}
K\sigma &\triangleq K \\
(\lambda x_1^{s_1}, \dots, x_n^{s_n} : e)\sigma &\triangleq \lambda x_1^{s_1}, \dots, x_n^{s_n} : e\sigma^{x_1, \dots, x_n}
\end{align*}
$$

where $\sigma^x$ is defined as the substitution $\sigma'$ such that $\sigma'(x) = x$ and $\sigma'(y) = \sigma(y)$ for $y \neq x$. For all $n$, $\sigma^{x_1, \dots, x_{n+1}}$ is defined as $(\sigma^{x_1, \dots, x_n})^{x_{n+1}}$.

We write $\{x_1 \mapsto t_1, \dots, x_n \mapsto t_n\}$ the substitution with domain $\{x_1, \dots, x_n\}$ that maps all $x_i$ to their respective $t_i$.

To understand why compatibility with $e$ is important in the definition above, consider a typing context $x : s, y : s$ and the expression $\forall x^s : P(x, y)$ where $P$ is some binary predicate. The substitution $\{y \mapsto x\}$ is adequate for the typing context, but if we forget the compatibility condition and apply the substitution naively, we obtain

$$ (\forall x^s : P(x, y)) \{y \mapsto x\} = \forall x^s : P(x, x) $$

The variable $y$, which is free in the original formula, became bound in the result. We have not defined semantics yet, but we can explain informally why that substitution does not preserve interpretation: if $s$ is interpreted as the domain of natural numbers, and $P$ as the relation $\leq$, then the original formula is false (because $y+1 \leq y$ in particular) while after the substitution it is true (by reflexivity of $\leq$).

This problem, which is called *variable capture*, is avoided by enforcing the compatibility condition between $e$ and $\sigma$. The condition can always be made to hold by renaming the bound variables of $e$ is necessary. That is why we may accept the following definition as a result:

$$ (\forall x^s : P(x, y)) \{y \mapsto x\} = \forall z^s : P(z, x) $$

The variable $z$ may be chosen among all the variable symbols that are not included in the typing context.