Telit Cinterion Adopts Formal Verification for IoT Software

IoT modules combining embedded AI, edge intelligence and 5G connectivity increase software complexity and expand the risk surface for runtime faults. To address this, Telit Cinterion has integrated TrustInSoft Analyzer into its verification workflow to support the next generation of IoT and cellular modules.

The move establishes a formalized testing framework aimed at mathematically verifying software behavior across all possible execution paths, rather than relying solely on conventional testing or sampling-based validation.

Formal verification embedded in module development
The adoption of TrustInSoft Analyzer introduces exhaustive static analysis into Telit Cinterion’s software verification phases. The tool applies formal methods, including abstract interpretation, to analyze C, C++, and Rust source code and prove the absence of critical runtime errors such as buffer overflows, null pointer dereferences, division-by-zero events, and undefined behavior.

Unlike dynamic testing, which validates selected input scenarios, formal verification evaluates all possible inputs within defined assumptions. This approach is particularly relevant for IoT firmware and communication stacks operating in distributed and safety-relevant environments, where unpredictable field conditions are common.

Telit Cinterion has combined the Analyzer’s generalization capabilities with a proprietary AI-driven engine developed in-house. The integration is intended to accelerate internal validation processes while maintaining mathematical guarantees of soundness. In practical terms, this supports development teams in identifying defects earlier in the lifecycle and reducing iteration cycles during integration of AI workloads at the edge.

Addressing complexity in AI-enabled edge and 5G systems
IoT modules designed for edge intelligence must process sensor data locally, manage connectivity over 4G and 5G networks, and interact with cloud-based services. This creates dense software stacks that include protocol layers, security libraries, device drivers, and AI inference components.

In such architectures, a single undefined behavior in low-level code can propagate through the system, affecting connectivity, data integrity, or device availability. By introducing exhaustive static analysis into its workflow, Telit Cinterion aims to guarantee the absence of specific classes of runtime faults before deployment.

For industrial IoT, automotive telematics, and smart infrastructure applications, this type of assurance contributes to predictable behavior under variable operating conditions. It also supports compliance efforts where demonstrable software reliability is required.

Workflow integration and scalability
TrustInSoft Analyzer has been integrated directly into Telit Cinterion’s existing development workflows, enabling automated analysis during verification phases rather than as a standalone audit step. The tool is designed to scale with increasing code bases and evolving module architectures, supporting continuous integration pipelines common in embedded and connectivity development.

TrustInSoft’s formal methods have been recognized by the US National Institute of Standards and Technology (NIST) in the context of advanced verification techniques. The company provides analysis tools and services for sectors including automotive, aerospace, defence, consumer electronics and IoT.

TrustInSoft will present its Analyzer at Embedded World, taking place March 10–12, 2026, in Nuremberg, Germany (booth 4-340).

www.telit.com