Overview

TRust² is an open project to develop formally Verified toolchain for the Rust language using theorem provers such as Isabelle/HOL 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 Rocq, Isabelle/HOL, and Lean, 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

• Solana blockchain
• Hvisor

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

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