Consensus protocols are the core of modern blockchain systems, such as the Bitcoin, Ethereum, and Algorand networks. Thanks to these protocols, participants in a blockchain network can reach consensus on which blocks to add to a blockchain, to have a consistent chain of blocks in the whole network. Blocks are typically collections of transactions, e.g., transferring currency between participants, but can contain other data depending on the use case. Consensus protocols are difficult to design, test, and implement. Problems may only manifest in rare cases but can have disastrous consequences. Formal protocol models allow exhaustive analysis and formal verification. However, formal verification is only as good as the specification of the protocol. For example, specification properties could be vacuously true, or the specification may omit to mention liveness properties that are crucial for progress in a system implementation. This thesis describes the practical validation of a formal specification of Giskard, a consensus protocol used in the PlatON network. We translated key aspects of a formal model of Giskard in the Coq proof assistant to executable Python code, and integrated them into the Sawtooth blockchain framework. Then, we ran simulations of a blockchain network executing Giskard using Sawtooth, checking network node state properties of Giskard as well as its global safety properties. Automated clients from the Sawtooth network provided randomly generated transactions as input for the network. The implementation with the test results are available for reproducibility. Both consensus safety and liveness issues were found in the formal specification of Giskard during the simulations. Based on the previous informal English specification of Giskard, we propose a new formal specification which was validated to reach consensus on blocks in the simulated blockchain network and uphold the protocol’s crash and Byzantine failure tolerance to a certain degree. The improved formal model can serve as a new basis for verifying and implementing Giskard in the future. / Konsensusprotokoll utgör kärnan i moderna blockkedjesystem som Bitcoin-, Ethereum- och Algorandnätverken. Tack vare dessa protokoll kan deltagare i blockkedjenätverk nå konsensus om vilka block som ska läggas till, för att få en konsekvent blockkedja i hela nätverket. Block är vanligen samlingar av transaktioner, till exempel överföringar av valuta mellan deltagare, men kan också innehålla annan data beroende på användningsområdet. Konsensusprotokoll är svåra att designa, testa och implementera. Problem kanske bara visar sig i sällsynta fall, men kan ha katastrofala konsekvenser. Formella protokollmodeller tillåter uttömmande analys och formell verifiering. Men formell verifiering ger bara så goda resultat som protokollspecifikationen tillåter. Till exempel kan specfikationsegenskaper vara sanna innehållslöst eller så kan specifikationen underlåta att nämna framstegsegenskaper som är viktiga för att en systemimplementation inte ska låsa sig. Denna avhandling beskriver den praktiska valideringen av en formell specifikation av Giskard, ett konsensusprotokoll som används i PlatONnätverket. Vi översatte nyckelaspekter av en formell modell i bevisassistenten Coq till körbar Python-kod och integrerade koden i blockkedjeramverket Sawtooth. Sedan körde vi simuleringar av ett blockkedjenätverk som använder Giskard med hjälp av Sawtooth och undersökte Giskards tillståndsegenskaper för nätverksnoder och även dess globala säkerhetsegenskaper. Automatiserade klienter från Sawtooth-nätverket tillhandhöll slumpgenererade transaktioner som indata för nätverket. Implementeringen med testresultaten är tillgängliga för reproducerbarhet. Både säkerhets- och framstegsproblem hittades i den formella specifikationen av Giskard under simuleringarna. Baserat på en tidigare informell specifikation av Giskard på engelska föreslår vi en ny formell specifikation som validerades att nå konsensus på block i det simulerade blockkedjenätverket och att till en viss grad tolerera krascher och byzantinska fel. Den förbättrade formella modellen kan användas som en ny bas för att verifiera och implementera Giskard i framtiden.

The Swedish public sector is under constant pressure to improve processes and services through further digitalization. Blockchain is a novelty technology which shows promise of enabling functionalities which are desired within the sector. However, as the technology is still in its infancy, the practical value it could offer the sector remains unproven. In this master thesis, the socio-technical transition of the public sector for adopting blockchain is analyzed using the multi-level perspective framework. The sector is operationalized as an incumbent socio-technical regime and blockchain as a collection of niche innovations. Affordance theory and the multi-level perspective are combined to analyze how the perception of blockchain affects the potential transition pathways. The primary empirical data is gathered through a series of interviews with key individuals from both the Swedish public sector and blockchain community, as well as from attending blockchain events. Secondary data is gathered through the review of various types of literature regarding the topic. The findings of the thesis show that the practical value and functionalities that blockchain offers and that match the needs of the sector are verification, authentication, traceability, automating simple logical functions, and digitizing unique value. The identified conceptual solutions deemed suitable today are: blockchain for identity management, blockchain for data verification, blockchains for property registers of, e.g., vehicles and real estate, and external industry blockchains for improved traceability of, e.g., supply chains and sales records. The thesis also derives recommendations for the public sector indicating that, e.g., active education, revision of regulation, and international cooperation would further a potential transition towards blockchain. It also finds that perceived affordances of a technology in its early stages affect the transition pathways; barriers of entry, number of potential adopting application sectors, the level of coordination, and the available resources for development are influenced by the perceptions. / Svensk offentlig sektor utsätts konstant för påtryckningar gällande fortsatt digitalisering av processer och tjänster. Blockkedjan är en ny teknologi som påvisar potential att kunna tillgodose funktioner önskvärda inom den offentliga sektorn. Dock är teknologin fortfarande i ett begynnande stadie och dess praktiska värde är ännu obevisat. I detta examensarbete analyseras offentliga sektorns potentiella socio-tekniska övergång till att ta blockkedjor i bruk med hjälp av multinivåperspektiv-ramverket. Sektorn operationaliseras som en befintlig socio-teknisk regim och blockkedjor som en samling av nischinnovationer. Görlighetsteori och multinivåperspektivet kombineras för att analysera hur uppfattningen av blockkedjor påverkar de potentiella övergångsvägarna. Primära empiriska data samlas in genom en serie av intervjuer med nyckelindivider från både svensk offentlig sektor och blockkedjegemenskapen, samt även från deltagande i blockkedjearrangemang. Sekundära data samlas in genom en studie av diverse typer av litteratur gällande ämnet. Examensarbetets resultat påvisar att det praktiska värdet och funktionaliteterna som blockkedjor tillgodoser och som passar med offentliga sektorns behov är verifikation, autentisering, spårbarhet, automatisering av simpla logiska funktioner, samt digitalisering av unika värden. De identifierade konceptuella lösningarna som bedöms lämpliga i dagsläget är: blockkedja för identitetshantering, blockkedja för dataverifikation, blockkedjor för egendomsregister, t.ex. för fordon och bostäder, samt externa industriblockkedjor för förbättrad spårning, t.ex. av försörjningskedjor och försäljning. Examensarbetet härleder även rekommendationer till offentliga sektorn, innefattande exempelvis aktiv utbildning, revision av reglementen, samt internationellt samarbete. Resultaten påvisar även att den uppfattade görligheten av en teknologi i ett tidigt stadie av innovation påverkar övergångsvägarna in i en regim. Detta genom att uppfattningarna influerar inträdesbarriärer, antalet potentiella applikationssektorer, koordinationsnivån, samt mängden tillgängliga resurser.