AI and Formal Guarantees: What’s New in the April 2026 Release of TrustInSoft Analyzer

As software systems grow more complex and development cycles continue to accelerate, verification tools must evolve to deliver greater efficiency without compromising trust. The April 2026 release of TrustInSoft Analyzer (TISA) introduces new capabilities that simplify adoption, streamline workflows, and deepen formal verification—while keeping mathematical guarantees at the core. 

This release brings together AI‑powered automation, improved usability and deployment, and expanded language and analysis support, all grounded in sound formal methods. 

Smarter Automation, Anchored in Determinism 

AI is increasingly used to accelerate development and verification, but speed alone is not enough. The same AI that helps defenders move faster also helps attackers move faster. 

As AI accelerates both vulnerability discovery and exploitation, automation must be anchored in deterministic, sound analysis. This is where formal methods become the perfect partner for AI. 

AI‑Powered Analysis Driver and Stub Generation  

The April 2026 release introduces AI‑powered analysis driver and stub generation, reducing analysis setup and configuration effort while maintaining the rigor of formal verification. 

AI‑powered analysis driver generation for C, C++, and Rust, enabled one‑click creation of analysis drivers for entry‑point functions. Complex parameters, including function pointers, are handled automatically. AI‑generated analyses are clearly identified in the UI and reports, preserving full traceability for safety and mission critical compliance. 

In addition, AI‑powered stub generation for C code automates the creation of context‑aware stubs by analyzing function bodies and call sites. Fully integrated into the existing UI, this capability significantly reduces manual preparation effort while improving analysis accuracy.  

AI accelerates verification workflows, and formal methods ensure software is reliable and secure. 

Supported LLMs include Claude Sonnet 4.6, Claude Opus 4.5, GPT 5.4, GPT 5.5 and Ollama-hosted LLMs. 

Improved Ease of Use Across the Workflow 

New GUI and usability improvements make it easier to configure analyses, explore results, and investigate root causes. These enhancements support broader adoption across development and verification teams without sacrificing analytical depth. 

Simplified Integration and Deployment 

Deployment has been streamlined across platforms, including macOS and Docker, with reduced external dependencies. These improvements simplify integration into CI pipelines and shared development environments, enabling teams to scale formal verification more easily. 

New Language and Analysis Capabilities 

This release also expands formal verification coverage with: 

• Enhanced Rust support, including programs using Rust core, fully integrated into the TrustInSoft Analyzer GUI 
• Improved MC/DC coverage analysis based on formal methods, supporting standards such as ISO 26262 
• Advanced detection of invalid resource usage, with capabilities to track memory regions for illegal read/write operations and verify that the software adheres to its memory mapping constraints.  

Moving Faster Without Losing Trust  

Across all new features, the objective is clear: help teams move faster without increasing risk. AI improves efficiency; usability reduces friction, and formal methods provide the certainty required when failure is not an option. 

The April 2026 release of TrustInSoft Analyzer is available now. To learn more or schedule a demo, visit www.trust-in-soft.com.