摘要：Rust是新興的系統級編程語言,旨在提供內存安全的同時保證極高的性能。Rust形式化語義是用來證明其內存安全和開發Rust程序分析工具的基礎。鑒于目前沒有直接描述Rust的形式化語義,提出了針對Rust語言的形式化可執行語義KRust。為了確保語義的可執行性和應用性,使用了K框架進行語義的開發。KRust目前涵蓋了Rust常見的語法和語義,包括了Rust的3個核心特性:所有權、借用和生命周期。KRust通過了191個測試樣例,其中157個都是來自Rust官方的測試集。語義對比測試實驗發現了Rust編譯器的缺陷。此外,KRust的語義還可以被應用于開發Rust程序分析工具。