Overview

TRust² is an open project to develop formally Verified toolchain for the Rust language using theorem provers such as Isabelle/HOL and Coq. The toolchain will include formal languages, program verifier, static analyzer, verified compilers, and code generator for Rust.

Publications

• A complete formal semantics of eBPF instruction set architecture for Solana, by Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanan, Rui Chang, Yongwang Zhao. OOPSLA25, Singapore, to appear.

• Formalizing x86-64 ISA in Isabelle/HOL: A Binary Semantics for eBPF JIT Correctness, by Jiayi Lu, Shenghao Yuan, David Sanan, Yongwang Zhao. 10th Symposium on Dependable Software Engineering: Theories, Tools and Applications (SETTA 2024), Hong Kong, China, November 26–28, 2024, pp. 197-216.

• 面向Rust语言的形式化验证方法研究综述, 张卓若,常瑞,杨申毅,陈芳. 软件学报,2025,36(8):0.

Current Members (Alphabetical)

Rui Chang, Jian Cheng, Jun Liu, Jiayi Lu, Di Luo, David Sanan, Shenyi Yang, Zhibin Yang, Shenghao Yuan, Qiyuan Xu, Zhuoruo Zhang, Yongwang Zhao

Source Code

Documentation

Links

1. Phi-System: an experimental certified programming language and also a generic verification platform.
2. CertSBF: A complete formal semantics of eBPF instruction set architecture for Solana.
3. Solana-x64-Semantics: Formalizing x64 binary semantics in Isabelle/HOL.