Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, Emilio Tuosto
The companion paper proposes a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. The model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. A toolchain supports formal model validation, Solidity code generation (extensible to other smart contract languages), and automated test synthesis. Although targeting blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. The expressiveness and practicality of the approach are demonstrated through modelling and realising coordination patterns in smart contracts. This artifact accompanies our paper [Elvis Konjoh Selabi et al., 2026]. It provides a toolchain for generating smart contract code from EDAM (Extended Data-Aware Machines) specifications. The artifact includes the complete source code, a Docker image for easy deployment, pre-generated experiment data (generated code, automated tests, and mutation testing results), and reproduction scripts.
Abstract Program verification provides stronger guarantees of correctness than standard testing. The verification process takes a program as input and derives a mathematical formula. Proving that a program is correct then reduces to establishing that this derived formula is unsatisfiable. Traditionally, automated reasoning tools can be used to determine unsatisfiability automatically. Furthermore, modern solvers can also produce a proof of unsatisfiability. However, these techniques typically rely on the proof and the underlying code being publicly available, which may not be desirable for certain applications. This work shows how to address this problem. Our team initially developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. Building on these initial results, we devised ZKSMT, a virtual machine for validating unsatisfiability results produced by SMT solvers in zero-knowledge settings. In this paper we describe the theoretical foundations of such virtual machines and demonstrate how they can be applied to the theories of uninterpreted functions and linear integer arithmetic, two of the most widely used theories in verification. We conclude by outlining how the full formal verification workflow can be adapted to operate in privacy-preserving settings.
The Hamiltonian cycle problem is a well-known NP-complete problem in graph theory. This problem relates to lots of practical problems such as designing very large scale integration (VLSI) and travel-ling salesman problem (TSP). Since it is NP-complete, there is no efficient algorithm to solve the Hamiltonian cycle problem, and hence, its solution is valuable. In this paper, we propose new physical zero-knowledge proof protocols for the Hamiltonian cycle problem, whereby an entity can prove its knowledge of a solution to another entity without leaking any information about the valuable solution. Our protocols are more efficient than the previous protocols. We also propose a physical zero-knowledge proof protocol for TSP, one of whose building blocks is a new representation of an integer commitment with a secure addition protocol.
Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, Emilio Tuosto
We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contract languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. We demonstrate the expressiveness and practicality of the approach by modelling and realising some coordination patterns in smart contracts.
Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker
Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.
Open access
4 source records
cs.LO
Formal Methods in Verification
Physical Unclonable Functions (PUFs) and Hardware Security
Proof-of-Stake (PoS) consensus protocols commonly employ epochs as temporal abstractions to simplify validator accounting, reward distribution, and slashing enforcement. These designs assume clean and synchronized state transitions across epoch boundaries. In practice, distributed systems exhibit asynchronous execution, delayed finality, and implementation divergence.This paper introduces and analyzes <b><i>Validator Epoch Reset Collisions</i></b>, a class of temporal desynchronization vulnerabilities in which validator state resets, reward counters, slashing windows, or participation flags become inconsistently applied across epoch boundaries. We demonstrate how such collisions create exploitable enforcement gaps that can be leveraged to evade penalties, duplicate rewards, or bypass participation requirements—without violating protocol rules. We argue that epoch-based accounting introduces structural risks to economic security unless continuity-enforcing safeguards are applied.
GLYPH is a transparent verification layer for Ethereum for trustless on-chain verification of heterogeneous proof systems. It unifies upstream SNARK and STARK settlement through a single packed arity-8 sumcheck verifier over p = 2^128 - 159, while preserving upstream assumptions. The design centers on a universal adapter surface, UCIR compilation, and a chain-bound artifact interface for stateless verification. Benchmark evidence in the whitepaper reports 29.45k total transaction gas in recorded testnet receipts. This record includes the whitepaper and the formal proof appendix.
Sungmin Lee, Kichang Lee, Gyeongmin Han, JeongGil Ko
Many location-based services rely on a point-in-polygon test ( PiP ), checking whether a point or a trajectory lies inside a geographic zone. Since geometric operations are expensive in zero-knowledge proofs, privately performing the PiP test is challenging. In this paper, we answer the research questions of how different ways of encoding zones affect accuracy and proof cost by exploiting grid-based lookup tables under a fixed STARK execution model. Beyond a Boolean grid-based baseline that marks cells as in- or outside, we explore a distance-aware encoding approach that stores how far each cell is from a zone boundary and uses interpolation to reason within a cell. % Our experiments on real-world data demonstrate that the proposed distance-aware approach achieves higher accuracy on coarse grids with only a moderate verification overhead, making zone encoding the key lever for efficient zero-knowledge spatial checks. Our experiments on real-world data demonstrate that the proposed distance-aware approach achieves higher accuracy on coarse grids (max. % 60%p 60%p accuracy gain) with only a moderate verification overhead (approximately 1.4×), making zone encoding the key lever for efficient zero-knowledge spatial checks.
Arthur Ramos, Anjolina Grisi de Oliveira, Ruy de Queiroz, Tiago M. L. de Veras
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4.
In this paper, I prove that sublinear regret across the environment Class C requires six functional properties, that these properties are mutually independent, and that they compose into a directed informational chain closing back on itself — a six-link cycle whose final link is grounded in an explicit Doob martingale construction over cycles of play. All six properties are defined functionally — as conditions on the distributions a decision-maker induces over actions and canonical summaries — so the results are invariant under implementation and apply to any decision-making system that can be modelled within the class: a person, an institution, or a machine. Every theorem in this paper, without exception, is checked line by line in the Lean 4 proof assistant against Mathlib: the formalization (~12,700 lines) contains zero `sorry`, zero custom axioms, and zero opaque definitions. Class C is the union of all POMDPs satisfying at least one of six structural properties covering the fundamental qualitative dimensions of adaptive hardness: reward ambiguity (P1), absorbing traps (P2), local optima (P3), deterministic optimality (P4), constrained feasibility (P5), and nonstationarity (P6). * Part I (Necessity). I define six primitives X1–X6 as purely functional properties of decision rules: Objective Tracking, Cross-Context Safety Transfer, Global Attractor Exploration, Policy Simplification, Feasibility Projection, and Feedback Adaptation. For each, I construct an explicit environment in C and prove an unconditional Ω(T) regret lower bound for any decision-maker lacking that primitive.* Part II (Independence). For every ordered pair (i,j) with i≠j, I exhibit an explicit decision rule possessing Xj but lacking Xi that suffers Ω(T) regret on the matching environment. All thirty directed-pair results are shown to follow from one master theorem, verified on a single compound environment with full non-interference analysis.* Part III (Sequential Dependence). Necessity is domain-invariant — a structural failure is a structural failure no matter what "success" means to the decision-maker — which is why Parts I and II hold unconditionally. Sufficiency is not: what counts as success is supplied by the domain, not by the theorem, so a single closed-form sufficiency result covering every domain at once would have to either fix one arbitrary notion of success and stop being general, or say nothing of substance. Part III proves exactly what generalizes. I prove six Information Enhancement Theorems establishing that the six primitives compose into a directed information chain: possessing Xi strictly increases the mutual information available toward any goal variable at Xi+1's task. Each of the six links is established outright — a forward theorem, a reverse theorem, and a non-reversibility result — with the exact point where a domain's own definition of success enters the chain named explicitly, as an Implementation Obligation, rather than assumed away. The closing link, X6→X1, is grounded in an actual Doob martingale construction: given that the cycle-indexed posterior is a martingale, it converges almost surely to the truth across cycles — the precise sense in which the chain accumulates rather than resets. To this paper's knowledge, no prior formalization unifies this many independently-proven-necessary structural properties into a single machine-checked class with proven mutual independence across all of them. All mathematical work is provided in full transparency and independent verification is highly encouraged: the complete Lean formalization, with a passing build and every theorem cross-referenced to its exact identifier, is at github.com/M-Ismail-ZA/IsmailsPrimitives. For any feedback or collaboration, please contact me via the email address listed on the paper. Updated: 3 July 2026 (V6.1).
Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, Ning Luo
Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-knowledge (ZK) protocols for PSPACE-complete statements by enabling ZK proofs of QBF (Quantified Boolean Formula) evaluation. The core idea is to validate quantified resolution proofs (Q-Res) in ZK. We develop an efficient polynomial encoding of Q-Res proofs, enabling proof validation through low-overhead arithmetic checks. We also design a ZK protocol to prove knowledge of a winning strategy related to the QBF, which is often equally important in practice. We implement our protocols and evaluate them on QBFEVAL. The results show that our protocols can verify 72% of QBF evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained.
Antoine Bak, Guilhem Jazeron, Pierre Galissant, Léo Perrin
In recent years, many hash functions have been introduced to satisfy the pressing need of some zero-knowledge protocols for such primitives allowing a low degree verification of their round function when arithmetized over a large field.While this can be achieved by restricting their sub-components to low-degree functions (and their inverse), the newest primitives in this category also leverage the intricacies of some proof systems to use “Split-and-Lookup” non-linear functions that essentially apply a small S-box in parallel over the binary representation of a field element.Such components excel at hindering attacks relying on polynomial system solving, but they offer poor security against statistical attacks. On the other hand, low degree monomials offer the opposite guarantees, being strong against statistical attacks. Several primitives have recently been proposed that combine such components in different ways in order to get the best from both.In this paper, we target such primitives by relying on the low degree components to allow a low-cost polynomial solving step. The weakness of Split-and-Lookups against linear attacks is used to simplify these systems, and their weakness against differential attacks is then used to propagate across many rounds the differential patterns obtained during polynomial solving. We instantiate this general approach by attacking round-reduced Monolith, and providing a distinguisher on full-round Skyscraper. These result then shed some light on how to best combine the different types of components to achieve the highest security.
Andrea Esposito, Francesco Rossi, Marco Bernardo, Francesco Fabris · 5 authors
Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake consensus via cryptographic self-sortition and binary Byzantine agreement. In this paper we present a process algebraic model of the Algorand consensus protocol with the aim of enabling formal verification. Our model captures the behavior of participants in terms of the structured alternation of consensus steps toward a committee-based agreement. We validate the correctness of the protocol in the absence of adversaries and then extend our model to assess the influence of coordinated malicious nodes that can force the commit of an empty block instead of the proposed one. The adversarial scenario is analyzed through an equivalence-checking-based noninterference framework that we have implemented in the CADP verification toolkit. In addition to highlighting both the robustness and the limitations of the Algorand protocol under adversarial assumptions, this work illustrates the added value of using formal methods for the analysis of consensus algorithms within blockchains.
Meihua Xiao, Y. P. Xu, Yongtuo Zhang, Ke Yang · 6 authors
Smart contracts, as a critical application of blockchain technology, significantly enhance its programmability and scalability, offering broad application prospects. However, frequent security incidents have resulted in substantial economic losses and diminished user trust, making security issues a key challenge for further development. Since smart contracts cannot be modified after deployment, flaws in their design or implementation may lead to severe consequences. Therefore, rigorous pre-deployment verification of their correctness is particularly crucial. This paper explores the symmetry in control flows and state transitions of Solidity smart contracts and leverages this inherent structural symmetry to develop a normalized state transition model based on a finite state machine. The FSM model is subsequently formalized into a Promela model with the Spin model checker. By integrating manually defined Linear Temporal Logic formulas with those generated by Smart Pulse, the Promela model is formally verified in Spin to ensure the correctness and security of smart contracts. This approach establishes a systematic verification framework, providing effective support to enhance the reliability and security of smart contracts.
Type systems are routinely employed in many modern programming languages to statically ensure various notions of runtime safety. We explore issues of typability and notions of safety in two different fields: Firstly, we focus on process calculi with composite channel names, where the type of a channel must somehow be derived from the types of its constituents. This collection of results includes a simple type system for the -calculus, along with some results of expressivity w.r.t. the -calculus; a generic type system for the Higher-Order Ψ-calculus, extending a similar type system for the ‘first-order’ Ψ-calculus; and a simple type system for , which aims to highlight a connexion to type structures from class-based/object-oriented languages. Secondly, we focus on the language TinySol, which models core features of the smart-contract language Solidity. Smart contracts are immutable programs with publicly visible code, that run atop a blockchain and are used to manage financial assets of users. Guided by insights from our work in process calculi, we develop type systems for ensuring three different properties: non-interference, call-integrity, and absence of out-of-gas exceptions. Lastly, we seek to tackle some of the shortcomings of the conventional, syntactic approach to type soundness, which had become evident in our previous developments. In particular, we study a peculiar construct in Solidity, known as the fallback function, which is untypable by syntactic type rules. Hence, we turn to a semantic approach to type soundness which allows type safety to be shown, even in cases where well-typedness cannot be proved by ordinary syntactic type rules. We use this approach to propose a method by which type safety may be recovered, even for contracts containing fallback functions, by allowing the programmer to supply a manual proof of type-safety for untypable pieces of code. This method does not depend on specific features of the fallback function, or even of TinySol or Solidity, and it may therefore also be developed for other smart-contract languages.
Abstract This paper introduces semi-competitive differential game logic $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , which enables verification of safety-critical applications that involve interactions between two agents. In $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , these interactions are specified as games on hybrid systems with two players that may collaborate with each other when helpful and may compete when necessary. The players in the hybrid games of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> have individual goals that may overlap, leading to nonzero-sum games. This makes $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> especially well-suited for verifying situations where players, e.g., share safety objectives but otherwise pursue different goals, so that zero-sum assumptions lead to overly conservative results. Additionally, $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> solves the subtlety that even though each player may benefit from knowledge of the other player’s goals, e.g., concerning shared safety objectives, unsafe situations might still occur if every player were to mutually assume the other player would act to avoid unsafety. The syntax and semantics, as well as a sound and relatively complete proof calculus are presented for $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> . The relationship between $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> and zero-sum differential game logic $$\textsf {dG}\mathcal {L}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:mi>L</mml:mi> </mml:mrow> </mml:math> is discussed and the purpose of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> illustrated in a canonical example.
Igor Konnov, Jure Kukovec, Thomas Pani, Roberto Saltini · 5 authors
We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification. Our primary tools are TLA+ for specification and the Apalache model checker for verification. Our formalization builds on the executable Python specification of 3SF. To begin, we manually translate this specification into TLA+, 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. Despite the inherent complexity, our results demonstrate that exhaustive 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 abstraction and domain expertise in enhancing model-checking efficiency and showcases the flexibility of TLA+ for managing intricate specifications.
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa · 7 authors
Abstract This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gr bner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.
Muhammad Rashid, Imran Rasool, Nazir Ahmad Zafar, Hamra Afzaal
Ethereum 2.0 stands out as a progressive decentralized blockchain platform, drawing attention for its security, scalability, and flexibility. Central to Ethereum 2.0 is the Beacon Chain, serving as the cornerstone managing validator rewards, penalties, attestations, and slashing mechanisms. Rewards and Penalties Mechanism (RPM) is of particular importance within the Beacon Chain as it includes validator balances based on their attestation behavior. Despite the critical role of RPM in maintaining the reliability and security of the Beacon Chain, the absence of formal verification work employing model checking is notable. Therefore, this research endeavors to fill this gap by employing formal verification technique to assess the RPM’s behavior concerning Friendly Finality Gadget (FFG) attestations. Utilizing Process Meta Language (PROMELA), a formal model of the RPM is specified, encompassing safety and liveness properties crucial for its robust functioning. The properties, including invalid attestation, integrity, fairness, availability, failure to attest, and inactivity imposition, are formalized through Linear Temporal Logic (LTL). Subsequently, the formal model alongside the specified properties is subjected to verification using the SPIN model checker. The properties are analyzed with respect to verification time, states visited, and memory usage. The outcome of this research contributes to a rigorous analysis of the RPM’s behavior. This work not only enhances an understanding of Beacon Chain’s operational dynamics but also underscores the importance of formal verification in ensuring the reliability and security of blockchain protocols.
Abstract Circuit languages like Circom and Gnark have become essential tools for programmable zero-knowledge cryptography, allowing developers to build privacy-preserving applications. These domain-specific languages (DSLs) encode both the computation to be verified (as a witness generator ) and the corresponding arithmetic circuits , from which the prover and verifier can be automatically generated. However, for these programs to be correct, the witness generator and the arithmetic circuit need to be mutually consistent in a certain technical sense, and inconsistencies can result in security vulnerabilities. This paper formalizes the consistency requirement for circuit DSLs and proposes the first automated technique for verifying it. We evaluate the method on hundreds of real-world circuits, demonstrating its utility for both automated verification and uncovering errors that existing tools are unable to detect.
(English) The advent of the internet, marked by pivotal developments such as the launch of Arpanet and the standardization of HTTP, has irrevocably changed the fabric of modern society. Centralized platforms like Microsoft, Google, Apple, and Amazon have dominated this digital landscape, offering many services ranging from cloud computing to online storage. However, the centralized nature of these services has raised significant concerns regarding user privacy, data integrity, and the potential for censorship. In response to these issues, the open-source community has explored peer-to-peer alternatives, notably in the realm of distributed file systems, ledgers, and blockchain technology. Blockchains, popularized by the emergence of Bitcoin, promote a democratized service model that challenges the centralized status quo. Yet, they are not without their own challenges, including decentralization, security, privacy, and performance. This thesis delves into the nuances of blockchain technology, focusing on Ethereum's transition from Proof of Work (PoW) to Proof of Stake (PoS) and its implications on network hardware requirements, topology, and overall performance. The development of Ethereum serves as a small-scale reflection of the broader ambitions and challenges in transitioning to Decentralized Finance (DeFi) platforms. Despite significant theoretical advancements in consensus mechanisms and scalability solutions, real-world implementations and experimental validations remain sparse. This work aims to bridge this gap by comprehensively analysing Ethereum's PoS transition by examining the interlaced relationships between software logic, hardware configurations, and network dynamics. Through novel measurement models and tools, this thesis contributes to a deeper understanding of how Ethereum's architectural changes impact its ecosystem and its participants' behaviours. Lastly, the research presented in this thesis illustrates the technical and operational challenges facing Ethereum and similar blockchain platforms and proposes a series of contributions that advance the field. This work empirically analyses the future enhancements in blockchain technology by exploring the implications of the network and its topology, to the viability of decentralized validation processes, and the potential for scaling solutions like Data Availability Sampling. The open-source tools and methodologies developed within the thesis scope represent the commitment to transparency and collaboration, which follows the spirit of the decentralized communities it seeks to serve. Through a mix of theoretical exploration and empirical research, this thesis aims to provide a deeper and more detailed understanding of Ethereum PoS' design choices, its capabilities and the limitations this one represents in future steps and upgrades, leading the way for more resilient, scalable, and decentralized digital infrastructures. (Català) L'arribada d'Internet, marcada per avenços fonamentals com el llançament d'Arpanet i l'estandardització de HTTP, ha canviat irrevocablement el teixit de la societat moderna. Les plataformes centralitzades com Microsoft, Google, Apple i Amazon han dominat aquest panorama digital, oferint serveis que van des de la computació al núvol fins a l'emmagatzematge en línia. No obstant això, la naturalesa centralitzada d'aquests serveis ha generat importants preocupacions pel que fa a la privacitat de l'usuari, la integritat de les dades i la possibilitat de censura. En resposta a aquests problemes, la comunitat de codi obert ha explorat alternatives d'igual a igual, especialment en l'àmbit dels sistemes d'arxius distribuïts i la tecnologia blockchain. Les blockchains, popularitzades pel sorgiment de Bitcoin, han proposat fins i tot un model de servei democratitzat que desafia l'statu quo centralitzat. No obstant això, no estan exemptes de desafiaments, incloent la descentralització, la seguretat, la privacitat i el rendiment. Aquesta tesi aprofundeix en les dinàmiques de la tecnologia blockchain, centrant-se en la transició d'Ethereum de Proof of Work (PoW) a Proof of Stake (PoS) i les seves implicacions en els requisits, la topologia de la xarxa i el rendiment general del maquinari. El desenvolupament d'Ethereum serveix com un reflex a petita escala de les ambicions i els desafiaments més amplis en la transició a plataformes de finances descentralitzades (DeFi). Malgrat els importants avenços teòrics en els mecanismes de consens i les solucions d'escalabilitat, les implementacions al món real i les validacions experimentals segueixen sent escasses. Aquesta tesi té com a objectiu tancar aquesta bretxa analitzant exhaustivament la transició PoS d'Ethereum mitjançant l'examen de les relacions entrellaçades entre la lògica del programari, les configuracions de maquinari i la dinàmica de la xarxa. A través de nous models i eines de mesura, aquesta tesi contribueix a una comprensió més profunda de com els canvis arquitectònics d'Ethereum impacten en el seu ecosistema i els comportaments dels seus participants. Per últim, la investigació presentada en aquesta tesi il·lustra els desafiaments tècnics i operatius que enfronten Ethereum i plataformes blockchain similars, i proposa una sèrie de contribucions que esperem serveixin per fer avançar el mon de les blockchains. La tesi analitza empíricament les millores futures en la tecnologia blockchain explorant les implicacions de la xarxa i la seva topologia, la viabilitat dels processos de validació descentralitzats i el potencial per escalar solucions com el mostreig de disponibilitat de dades. Les eines i metodologies de codi obert desenvolupades dins de l'abast de la tesi representen el compromís amb la transparència i la col·laboració, que segueix l'esperit de les comunitats descentralitzades a les que busquem servir. A través d'una combinació d'exploració teòrica i investigació empírica, aquesta tesi té com a objectiu proporcionar una comprensió més profunda i detallada de les opcions de disseny d'Ethereum PoS, les seves capacitats i les limitacions que això representa en futurs passos i actualitzacions, obrint el camí cap a una solució més resilient i escalable per a infraestructures digitals descentralitzades. (Español) La llegada de Internet, marcada por avances fundamentales como el lanzamiento de Arpanet y la estandarización de HTTP, ha cambiado irrevocablemente el tejido de la sociedad moderna. Plataformas centralizadas como Microsoft, Google, Apple y Amazon han dominado este panorama digital, ofreciendo servicios que van desde computación en la nube hasta almacenamiento en línea. Sin embargo, la naturaleza centralizada de estos servicios ha generado importantes preocupaciones con respecto a la privacidad del usuario, la integridad de los datos y la posibilidad de censura. En respuesta a estos problemas, la comunidad de código abierto ha explorado alternativas de igual a igual, especialmente en el ámbito de los sistemas de archivos distribuidos, los libros de contabilidad y la tecnología blockchain. Las blockchains, popularizadas por el surgimiento de Bitcoin, promueven un modelo de servicio democratizado que desafía el status quo centralizado. Sin embargo, no están exentos de desafíos, incluida la descentralización, la seguridad, la privacidad y el rendimiento. Esta tesis profundiza en los matices de la tecnología blockchain, centrándose en la transición de Ethereum de Proof of Work (PoW) a Proof of Stake (PoS) y sus implicaciones en los requisitos, la topología de la red y el rendimiento general del hardware. El desarrollo de Ethereum sirve como un reflejo a pequeña escala de las ambiciones y desafíos más amplios en la transición a plataformas de finanzas descentralizadas (DeFi). A pesar de los importantes avances teóricos en los mecanismos de consenso y las soluciones de escalabilidad, las implementaciones en el mundo real y las validaciones experimentales siguen siendo escasas. Esta tesis tiene como objetivo cerrar esta brecha analizando exhaustivamente la transición PoS de Ethereum mediante el examen de las relaciones entrelazadas entre la lógica del software, las configuraciones de hardware y la dinámica de la red. A través de novedosos modelos y herramientas de medición, esta tesis contribuye a una comprensión más profunda de cómo los cambios arquitectónicos de Ethereum impactan su ecosistema y los comportamientos de sus participantes. Por último, la investigación presentada en esta tesis ilustra los desafíos técnicos y operativos que enfrentan Ethereum y plataformas blockchain similares y propone una serie de contribuciones que hacen avanzar el campo. La tesis analiza empíricamente las mejoras futuras en la tecnología blockchain explorando las implicaciones de la red y su topología, la viabilidad de los procesos de validación descentralizados y el potencial para escalar soluciones como el muestreo de disponibilidad de datos. Las herramientas y metodologías de código abierto desarrolladas dentro del alcance de la tesis representan el compromiso con la transparencia y la colaboración, que sigue el espíritu de las comunidades descentralizadas a las que busca servir. A través de una combinación de exploración teórica e investigación empírica, esta tesis tiene como objetivo proporcionar una comprensión más profunda y detallada de las opciones de diseño de Ethereum PoS, sus capacidades y las limitaciones que esto representa en futuros pasos y actualizaciones, abriendo el camino hacia una solución más resiliente y escalable. e infraestructuras digitales descentralizadas.