Overview
TRust2 is an open project to develop formally Verified toolchain for the Rust language using theorem provers such as Isabelle/HOL, Lean, and Rocq. The toolchain will include formal languages, program verifier, static analyzer, verified compilers, and code generator for Rust.
Model-Based Development
AADL and SysML are widely used in safety-critical domains such as aerospace and automotive. We are exploring the generation of executable Rust code from these high-level models.
- AADL-to-Rust
- SysMLv2-to-Rust
Theorem Provers
Theorem provers (TPs), including Isabelle/HOL, Lean, and Rocq, are employed to guarantee expected properties of given programs. We are working on bidirectional code generation between these TPs and Rust.
- Isabelle2Rust
- Rust2Isabelle (e.g., based on the Aeneas-Charon project)
Rust Contract Specification
We are developing a formal specification following the design-by-contract principle for Rust. Existing efforts in Rust include Verus, Prusti, and others. Our current toolchain and specification language are still work in progress.
Real-world Rust Applications
Publications
Overveiw of TRust2
- 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
2026
-
Formal Verification of a Memory Allocator for Rust Hypervisors: From Verified to Deployable Code with Functional Equivalence Guarantees, by Liu Jun, Liu Jingxuan, Shenghao Yuan, David Sanan, Chen Kang, Cao Donggang and Yongwang Zhao. Formal Methods in Computer-Aided Design 2026(FMCAD26), to appear.
-
Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications, by Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, Mingshuai Chen. OOPSLA26, to appear.
-
A RISC-V JIT Backend for Solana eBPF: Enabling Multi-Architecture Deployment of Blockchain Virtual Machines, by Jun Liu, Jiayi Lu, Shenghao Yuan, David Sanan, Yongwang Zhao. International Conference on Blockchain Research and Applications (BCRA 2026) (published in the Journal of Blockchain: Research and Applications).
2025
-
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.
-
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.
-
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)
Jian Cheng, Zefeng Cheng, Hao Liu, Jun Liu, Jiayi Lu, Di Luo, David Sanan, Keshen Xiang, Zhibin Yang, Shenghao Yuan, Qiyuan Xu, Yuhan Zou, Jiarui Zhao, Yongwang Zhao
alumni (Alphabetical)
Rui Chang, Shenyi Yang, Zhuoruo Zhang
Source Code
Following the MIT license, the source code of TRust2 is available at https://github.com/OpenSourceVerif
Note: some projects within TRust2 are initially developed in private repositories. They will be made publicly available once the corresponding submissions or declarations have been accepted/completed
Documentation
Links
- Phi-System: an experimental certified programming language and also a generic verification platform.
- CertSBF: A complete formal semantics of eBPF instruction set architecture for Solana.
- Solana-x64-Semantics: Formalizing x64 binary semantics in Isabelle/HOL.
- RustLight AST: A lightweight Rust subset AST crate used by all Rust code generation tasks in TRust2
