操作系统安全的形式化验证：从 seL4 到 Verus 的工程实践路径
从seL4微内核的里程碑式验证出发，深入解析现代形式化验证工具链（Kani/Prusti/Verus）在操作系统安全领域的工程实践，包含完整代码示例与实战案例。
Memory Safety
Linux 内核 Rust 子系统深度工程实践：从安全驱动到上游合并之路
深入剖析Linux内核Rust子系统的内部架构，从内存安全动机到实战字符设备驱动编写，涵盖FFI交互、并发原语封装、错误处理与生产级案例分析。
Linux 内核 KASAN 深度实战：内存安全错误的检测利刃
详解Linux内核KASAN内存错误检测工具的架构原理、编译配置、实战案例与高级变体（KFENCE/SW_TAGS/HW_TAGS），覆盖越界写入、UAF、双重释放等常见内存bug的定位实战
深入理解 Rust 所有权系统：从生命周期到并发安全的完整实战指南
深入剖析 Rust 所有权系统的核心原理与实战应用。从所有权三规则、借用与引用、生命周期标注，到智能指针和并发安全，通过完整代码示例展示 Rust 如何在编译期保证零成本内存安全。
Rust Memory Safety and Ownership: A Deep Dive into Zero-Cost Abstractions
Deep dive into Rust's ownership system: ownership rules, borrowing, lifetimes, smart pointers, concurrency safety patterns, Pin, unsafe abstractions, and real-world performance benchmarks.
