TrustInSoft has released TrustInSoft Analyzer 2025.10, extending its formal verification toolchain to include Rust analysis capabilities alongside its existing C and C++ support. The update enables detection of undefined behaviors, panics, and memory vulnerabilities in mixed-language codebases through exhaustive static analysis.
The Rust integration addresses verification gaps that remain despite the language’s built-in memory safety features. The analyzer can detect integer overflows, verify safe calling conventions when interfacing with C functions, and analyze code within Rust’s unsafe blocks where manual memory safety proofs are required. Teams working with mixed Rust and C/C++ codebases can now apply the same formal verification methods across their entire codebase, including interactive root cause investigation and mathematical proof of code correctness.
The release introduces native support for concurrent code analysis, covering real-time operating systems, interrupt-driven firmware, and multi-threaded applications. Rather than simulating selected execution scenarios, the tool explores all possible execution paths to identify race conditions and non-deterministic behaviors. This exhaustive approach applies the same mathematical verification principles used for single-threaded code to concurrent systems.
Additional updates include support for C23 language features including _BitInt, constexpr, and nullptr, with enhanced structure visualization in the Root Cause Investigator interface. The alarm management system now includes collaborative features for classification, commenting, and integration with external bug-tracking systems. The partnership with Ferrous Systems enables integration with their Ferrocene qualified compiler toolchain for safety-critical Rust development.
Leave a Reply