We present the first formal semantics for the Solana eBPF bytecode language used in smart contracts on the Solana blockchain platform. Our formalization accurately captures all binary-level instructions of the Solana eBPF instruction set architecture. This semantics is structured in a small-step style, facilitating the formalization of the Solana eBPF interpreter within Isabelle/HOL. We provide a semantics validation framework that extracts an executable semantics from our formalization to test against the original implementation of the Solana eBPF interpreter. This approach introduces a novel lightweight and non-invasive method to relax the limitations of the existing Isabelle/HOL extraction mechanism. Furthermore, we illustrate potential applications of our semantics in the formalization of the main components of the Solana eBPF virtual machine

@article{paperbot3198,
  title = {A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana},
  author = {Shenghao Yuan and Zhuoruo Zhang and Jiayi Lu and David Sanan and Rui Chang and Yongwang Zhao},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA1},
  year = {2025},
  doi = {10.1145/3720414}
}