Symposium on Formal Methods for RUST at ICSE 2025
The event
Today, critical infrastructure is vulnerable to both malicious attacks and unintended failures, and these risks are expected to grow in the foreseeable future. Deploying formal methods (FM) across critical cyber physical systems would dramatically improve safety and security, but has historically been too costly to use outside the simplest or most critical subsystems.
In the light of the DARPA TRACTOR program, Atlas Computing is organizing this Symposium to bring together the most relevant projects in formal methods tools for RUST and provide everyone with an update on the cross-functional efforts between academia and industry, and what else needs to be done for the safety and security of cyber systems.
Program (WIP)
9 am - Xavier Denis - Creusot
10 am - Remi Delmas (AWS) - Harness-based verification in Kani
11 am - Aymeric Fromherz (INRIA) - Charon
BREAK
1 pm - Zyad Hassan (AWS) - Contract-based verification in Kani
2 pm - Guillaume Claret (Formal Land) (Coq-of-Rust)
3 pm - Daniel Cumming (Runtime Verification) - Symbolic Execution of Rust code via Stable MIR
4 pm - Son Ho (Microsoft) - Aeneas: Rust Verification by Functional Translation
Main Sponsor
AWS
Co-sponsor
MC
Why RUST?
According to the 2024 Stack Overflow survey RUST was the most-admired programming language with a score of 82.2%. The State of the Developer Nation report marks RUST as one of the fastest growing languages with over 4,000,000 developers in 2024, up from 600,000 in 2020.
Without knowing all the factors driving DARPA’s decision to move from C to RUST, we acknowledge that the latter has a lot to offer:
1. Memory safety without runtime cost (no garbage collector overhead, memory safety guaranteed at compile time, fine-grained control over memory, zero-cost abstractions for memory management)
2. Superior concurrency model (thread safety enforced at compile time, true parallel execution, no data races by design)
3. Performance with safety (C/C++ performance without undefined behaviors, better memory efficiency that Java/Go, predictable runtime behavior, no runtime overhead for abstractions)
4. Good error handling (no silent failures, no unchecked exceptions, better error messages at compile time)
5. Modern developer experience (built-in package management, static typing without bolted-on solutions, integrated testing and documentation)
6. Cross-platform development (native cross-compilation support, strong embedded systems capabilities)
7. System-level control (direct hardware access, more control over memory layout, safe abstractions by default and without overhead)
Even though RUST provides strong safety guarantees through its type system and ownership model, preventing memory safety issues and data races at compile time, its built-in safety features are not sufficient.
There are no substitutes for formal methods (FM) when absolute correctness is required, especially for systems where failure could lead to loss of life, significant financial loss, or critical-systems security breaches.
While a wide range of FM tools have been developed at a fast pace, the overall ecosystem is lacking maturity due to limited capabilities of each tool, incomplete formal semantics of all RUST features, the need for better integration with existing proof assistants, and the lack of standardized specification languages.
The same ownership and borrowing rules that make RUST memory-safe also make formal verification more complex. RUST's rich type system introduces verification challenges around generics and trait bounds, associated types, lifetime parameters and complex enums with variants. Many RUST programs contain unsafe blocks for performance or low-level operations that bypass normal safety checks, may have implicit invariants that are hard to formalize, or simply require additional verification obligations. Verifying concurrent RUST programs is particularly challenging due to Send and Sync trait implications, atomic operations, lock-free data structures, and message passing patterns. Many programs rely heavily on the standard library, which contains significant unsafe code, has complex implementation details, requires the verification of the library abstractions, and may need formal specifications for common types.
What should I bring?
Your research, a friend or colleague, and lots of curiosity and passion for the topic. Due to the venue capacity, the attendance is limited to 100 participants. Save your spot now.
Code of Conduct
When you register for this event you agree with this Code of Conduct.