TrustInSoft, the Paris-based software verification company, has expanded its formal verification technology to support the Rust programming language and real-time systems, as part of the latest update to its flagship product, TrustInSoft Analyzer 2025.10.
The update, announced on 4th November, introduces comprehensive Rust analysis tools designed to detect undefined and unwanted behaviour in safety-critical software. It also improves the handling of multithreaded and concurrent code, extending TrustInSoft’s reach beyond traditional C and C++ codebases.
Chief executive Caroline Guillaume said the release represented “a leap into the future of safe, secure, and standards-compliant software development”. “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’,” she said.
The move comes as Rust continues to gain traction in systems programming, particularly for applications where memory safety and reliability are paramount. While Rust eliminates many common sources of bugs, it leaves some areas—such as integer overflows, unsafe code blocks, and C interoperability—beyond its guarantees.
To bolster its Rust capabilities, TrustInSoft partnered earlier this year with Ferrous Systems, a German company specialising in Rust-based tooling and the qualified Ferrocene compiler for safety-critical and embedded environments. The integration allows TrustInSoft Analyzer to apply formal verification and interactive root cause analysis to Rust programs, as well as mixed Rust and C/C++ projects.
“Rust’s memory safety, our qualified compiler toolchain, Ferrocene, and the formal verification in TIS Analyzer provide complementary capabilities,” said Florian Gilcher, managing director of Ferrous Systems. “Together, they help development teams navigate critical paths with confidence and deliver software they can trust.”
The new release also extends TrustInSoft’s verification technology to concurrent and real-time systems. The Analyzer now explores all possible execution paths across threads, interrupts, and timing-sensitive firmware, identifying race conditions and non-deterministic behaviour with mathematical certainty.
Additional updates include full support for the C23 language standard and improved triage tools for managing verification alarms, enabling teams to review, classify, and link them to external bug-tracking systems.
TrustInSoft, which uses formal mathematical methods to guarantee the absence of critical runtime errors, is recognised by the US National Institute of Standards and Technology for its use of abstract interpretation techniques. Its clients include firms in the automotive, aerospace, defence, consumer electronics, and IoT sectors.
