Robotizr and AI-MATTERS: how to enhance safety and reliability of robotic systems

As part of the European AI-MATTERS project, FBK’s Center for Digital Industry (DI Center) worked with Robotizr—an Italian company specializing in industrial automation—to strengthen the reliability and safety of robotic systems through the application of formal software verification methods, offering the service “Application of formal methods for reliable industrial systems.” Robotizr’s platform enables intuitive programming of industrial robotic arms through a graphical interface that allows operators to create operational sequences by composing visual blocks on a tablet, even without programming expertise.  While this flexibility opens robotics to new users and contexts, it also increases the need to ensure that automatically generated programs are safe, consistent, and efficient.

Leveraging AI-MATTERS, the Formal Methods Unit of FBK’s Center for Digital Industry has integrated advanced automatic code verification tools developed in-house (the nuXmv model checker and the Kratos analyzer) to analyze user-generated programs and automatically detect anomalous behaviors, inefficiencies, or potential risks before the robot is deployed.

The outcome was the validation of a platform that combines accessibility with safety, preventing operational errors and ensuring greater reliability in production processes.
This service demonstrated how applied research can underpin the validation of concrete industrial solutions, promoting intelligent, safe, and sustainable automation aligned with the principles of trustworthy Artificial Intelligence.

The design details

The solution

AI-MATTERS provided Robotizr with customized technical expertise and access to state-of-the-art verification technologies developed by FBK’s Formal Methods (FM) Unit.

The project focused on integrating formal verification directly into the Robotizr platform, using advanced tools such as the nuXmv symbolic model checker and the Kratos code analyzer.

Thanks to this collaboration, the Robotizr team—together with FBK researchers Stefano Tonetta and Alberto Griggio —designed a verification backend capable of translating visual robot programs into formal representations and automatically checking for anomalies, unreachable blocks, or unsafe motions.

The Results

The partnership between Robotizr and AI-MATTERS has produced measurable results:

• increased security: early detection of unsafe or inconsistent robotic behavior.
• greater reliability: automated validation of user-defined programs through formal analysis.
• improved usability: users can now receive real-time feedback on potential errors directly within the visual programming interface.

These advances have transformed Robotizr’s platform into a trusted environment for industrial automation, where security and innovation coexist.

Looking forward

Based on the results obtained with AI-MATTERS, Robotizr plans to expand its verification framework to include dynamic runtime analysis and machine learning-based optimization, ensuring that automation remains intelligent and secure.