shorten the abstract and remove a few hanging lines

reports/3sf.tex

@@ -7,7 +7,7 @@ \section{Basic 3SF concepts}\label{sec:3sf}
 
 \paragraph*{Validators.} Participants of the protocol are referred to as \emph{validators} with $n$ being their total number.
 Every validator is identified by a unique cryptographic identity and the public keys are common knowledge. 
-Each validator has a \emph{stake} but for the purpose of this project each validator's stake is set to 1.
+Each validator has a \emph{stake} but for the purpose of this project each validator's stake is set to~1.
 % If a validator $v_i$ misbehaves and a proof of this misbehavior is given, it loses a part of its stake ($v_i$ gets \emph{slashed}). 
 
 \paragraph*{Slots.} Time is divided into \emph{slots}. 

reports/intro.tex

@@ -62,12 +62,13 @@ \subsection{This Project: Model Checking of 3SF}
 specifying consensus algorithms. Among the rich spectrum of
 specifications~\cite{tla-examples}, the most notable for our project are the
 specifications of Paxos~\cite{lamport2001paxos}, Raft~\cite{Ongaro14}, and
-Tendermint~\cite{abs-1807-04938,TendermintSpec2020}. Since consensus algorithms
+Tendermint~\cite{abs-1807-04938,TendermintSpec2020}. AS consensus algorithms
 are quite challenging for classical model checkers like TLC, we choose
-the symbolic model checker Apalache~\cite{Apalache2024,KT19,KonnovKM22}. This model checker utilizes the
+the symbolic model checker Apalache~\cite{Apalache2024,KT19,KonnovKM22}.
+It utilizes the
 SMT solver~Z3~\cite{MouraB08} in the background. Apalache was used for model
 checking of agreement and accountable safety of
-Tendermint~\cite{TendermintSpec2020}. As added benefit, four of the project
+Tendermint~\cite{TendermintSpec2020}. Moreover, four of the project
 participants have developed Apalache in the past and know its strenghts and
 weaknesses.
 

reports/report.tex

@@ -14,7 +14,8 @@
 \newcommand{\rs}[1]{\footnote{\textcolor{purple}{#1}}}
 
 \title{\vspace{-2em}Technical Report: Exploring Automatic Model-Checking of the Ethereum specification\footnote{%
-		The specifications, scripts, and experimental results can be accessed at: \url{https://github.com/freespek/ssf-mc}}}
+		The specifications, scripts, and experimental results can be accessed at:
+        \\\url{https://github.com/freespek/ssf-mc}}}
 \author{%
     Igor Konnov\thanks{This work was supported by Ethereum Foundation
     under grant FY24--1535 in the 2024 Academic Grants Round.}\\
@@ -49,14 +50,13 @@
 Our formalization builds on the executable Python specification of 3SF\@. To
 begin, we manually translate this specification into~\tlap{}, revealing
 significant combinatorial complexity in the definition of Accountable Safety.
-To address these challenges, we introduce several layers of manual abstraction:
-(1) replacing recursion with folds, (2) substituting abstract graphs with
-integers, and (3) decomposing chain configurations.
-To cross-validate our results, we develop alternative encodings in SMT (CVC5)
-and Alloy.
+To address this, we introduce several layers of manual abstraction:
+(1)~replacing recursion with folds, (2)~abstracting graphs with
+integers, and (3)~decomposing chain configurations.
+To cross-validate, we develop encodings in SMT (CVC5) and Alloy.
 
 Despite the inherent complexity, our results demonstrate that exhaustive
-verification of Accountable Safety is feasible for small instances --
+verification of Accountable Safety is feasible for small instances ---
 supporting up to 7 checkpoints and 24 validator votes. Moreover, no violations
 of Accountable Safety are observed, even in slightly larger configurations.
 Beyond these findings, our study highlights the importance of manual