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

• TRust2: Towards Formally Verified Toolchain of Rust Language in Isabelle/HOLs, by Yongwang Zhao. Keynote/Invited Paper, 26th International Conference on Formal Engineering Methods (ICFEM 2025) , Hangzhou, China, November 10–13, 2025

• Tacco: A Framework for Ensuring the Security of Real-World TEEs via Formal Verification, by Jilin Hu, Yongwang Zhao#, Shuangquan Pan, Zuohua Ding, and Kui Ren. IEEE Transactions on Dependable and Secure Computing (TDSC), VOL. 22, NO. 6, NOVEMBER/DECEMBER 2025, pp. 6983 - 6997.

• 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, ACM Program. Lang. 9, OOPSLA1, Article 80 (April 2025), 27 pages.

• 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.