Paris-based TrustInSoft has released TrustInSoft Analyzer 2025.10 in its formal verification toolchain. The update introduces comprehensive Rust analysis capabilities for detecting undefined and unwanted behaviours and delivers an improved multithreading experience. It enables development teams working with Rust or mixed-language codebases in safety-critical environments to gain formal, mathematical confidence in the safety and reliability of their software.
“TIS Analyzer 2025.10 delivers what developers and security teams have been asking for: a tool that doesn’t guess, doesn’t miss and doesn’t stop at ‘probably OK. It brings formal, mathematical confidence to the newest and most complex parts of the modern codebase,’” said Caroline Guillaume, TrustInSoft CEO.
Rust is rapidly becoming very popular in systems programming, especially for its built-in memory safety. However, there are safety guarantees that Rust doesn’t provide, including protection against overflows and safe calling into C functions. Rust also has an unsafe sublanguage where the proof of memory safety needs to be conducted by the user.
In March 2025, TrustInSoft formed a partnership with Ferrous Systems, a provider of Rust-based tooling and solutions for safety-critical and embedded systems, to bring Rust support and the benefits of their qualified compiler toolchain, Ferrocene, to TrustInSoft’s formal analysis engine. TIS Analyzer 2025.10 now provides the same interactive root cause investigation, code coverage, and mathematical proof guarantees for Rust as it does for C and C++. For engineering teams mixing Rust with legacy C/C++ or working in safety-critical environments, this means something concrete: a way to detect undefined and unwanted behaviors, panics, and memory vulnerabilities in mixed-language codebases before they hit production.
“Writing software that is correct and reliable starts with confidence in both the tools and the process,” said Florian Gilcher, managing director of Ferrous Systems. “Rust’s memory safety, our qualified compiler toolchain, Ferrocene, and the formal verification in TIS Analyzer provide complementary capabilities that, when used together, help development teams navigate critical paths with confidence and deliver software they can trust.”
When it comes to concurrency, here bugs can be elusive. TIS Analyzer 2025.10 introduces native support for analyzing concurrent code—including real-time operating systems, interrupt-driven firmware, and multi-instance threading scenarios. The Analyzer doesn’t just simulate a few scenarios. It explores all execution paths, flagging race conditions and non-deterministic behaviors with the same mathematical confidence it brings to single-threaded code.
TIS Analyzer 2025.10 also rounds out support for C23 language features. Developers can now analyse code using _BitInt, constexpr, and nullptr—with improved structure visualization in the Root Cause Investigator.
Alarm triage is also getting smarter. Teams can now collaborate more effectively with features for reviewing, classifying, commenting on, and linking alarms to external bug-tracking systems.
