Validating Rust for industry: Certification meets formal analysis
summary
Claims a workflow that pairs TrustInSoft Analyzer (abstract interpretation, no full build required—uses build trace) with a Ferosin SDK (qualified compiler, signed releases) to exhaustively detect and prove absence of whole classes of runtime errors: unwrap/expect panics, slice OOB, div-by-zero, integer overflow, MMIO rule violations, and undefined behavior across Rust↔C/C++ FFI. Tool outputs combined Rust+C reports, produces MCDC coverage, needs almost no annotations, and is already used toward automotive, medical and IEC 61508 qualification.
AI-written summary · about
chapters (10)
- 0:00Safety critical Rust intro
- 1:06Validating Rust for certification
- 4:20Rust runtime errors and unsafe
- 8:16TrustInSoft Analyzer for Rust
- 15:06Ferrocene’s role in Rust
- 19:51Ferrocene’s certified compiler
- 22:00Rust compiler issues and fixes
- 23:50Compliance and confidence in Rust
- 24:52Certification chain with Ferrocene
- 25:35Q&A on verification
related talks
56mRust for Foundation Software
26mFerrocene - qualifying the Rust compiler using a fully open source tool stack
58mRust for The Curious C++ Developers
25mContinuous compliance with Rust in automotive software
28mSafety compliance of Rust libraries
21mA Tour of Empirical Verification in Rust
22mRust as a Foundation for a Safe and Sustainable Future
25m"Compiler-Driven Development: Making Rust Work for You"