Three additions to TrustInSoft's formal verification platform in its April 2026 release bring AI-generated test infrastructure to a category of tooling where correctness proofs have traditionally been an entirely manual process.
TrustInSoft Analyzer (TISA) targets mission-critical and safety-critical software development, where the goal is mathematical proof of correctness rather than probabilistic testing coverage. The April 2026 update introduces AI-generated test drivers and stubs, which reduce the setup overhead involved in running formal analysis — work that previously fell entirely to engineers. Integrated Rust support has been added to the graphical interface, and MC/DC (Modified Condition/Decision Coverage) analysis now runs through formal methods, keeping the same guarantees in place rather than relying on combinatorial testing.
The company describes the release as focused on reducing manual effort while maintaining compliance with industry standards. Combining AI-assisted automation with a formal-methods backend is the design choice: the AI handles scaffolding generation, the mathematical engine handles proof.
Caroline Guillaume, CEO of TrustInSoft, said: "TrustInSoft Analyzer delivers a unique level of guarantees through the use of sound formal methods, and this approach aligns naturally with AI."
TrustInSoft Analyzer delivers a unique level of guarantees through the use of sound formal methods, and this approach aligns naturally with AI.
