一句话：首次给出 Solana eBPF 字节码的完整小步语义，并在 Isabelle/HOL 中形式化与验证。
本文针对 Solana 区块链智能合约所使用的 eBPF 字节码语言缺乏形式语义的问题，首次提出其指令集架构的完整形式语义。该语义覆盖所有二进制级指令，并采用小步风格，便于在 Isabelle/HOL 中形式化 Solana eBPF 解释器。作者还设计语义验证框架，从形式化中抽取可执行语义，与原始 Solana eBPF 解释器实现进行对比测试；该方法轻量且非侵入，缓解了 Isabelle/HOL 现有抽取机制的限制。最后展示了该语义在形式化 Solana eBPF 虚拟机主要组件方面的潜在应用。
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}
}