Formal Verification of Token Standards on Ethereum and Solana: A Comparative Analysis of Fungible Asset Models

Abstract

Blockchain-based token systems are widely used for the creation and management of economic assets. This makes their correctness a critical concern for blockchain developers, auditors and security engineers. ERC-20 and SPL tokens are amongst the largest and most used standards that define the foundation for token transfer, mint, burning and authorization. However, the architectural and developmental differences in both ecosystems pose distinct challenges in specifying and verifying token correctness. This thesis focuses on invariant-based verification across two heterogeneous blockchain ecosystems. The thesis develops a comparative framework for ERC-20 and SPL token models, focusing mainly on correctness properties like balance consistency, supply preservation, transfer validity, minting, and burning constraints. These properties are validated across six tools: Certora, Foundry, KEVM for ERC-20 and Kani, Prusti, and MIRAI for SPL tokens. It follows a qualitative, artefact-driven case study approach that evaluates tools on five benchmarks: verifiability, expressiveness, specification effort, coverage, and soundness of assumptions. The results depict that the invariant-based verification is a valuable method for checking essential token correctness properties, but its effectiveness depends on the underlying architecture, efforts, and testing tool. Ethereum verification is more contract-centric while Solana verification requires additional reasoning about account ownership, signer authority, mint account relationships and runtime assumptions. The tools provide complementary forms of assurance rather than complete standalone guarantees; deductive verification, fuzzing, bytecode-level reasoning, bounded model checking, contract-based verification and static analysis each capture different aspects of correctness Overall, this thesis shows that formal verification can strengthen confidence in token implementation when the testing procedures are followed strictly with correct specifications and scope. It also highlights the need for layered assurance pipelines that combine formal verification with testing, auditing, and runtime modeling for secure cross-platform token development.