[ros-users] [Discourse.ros.org] [ROS Projects] Formal verification of ROS nodes using Imandra reasoning engine

[Kostya Kanishev]

Hello! We at [Aesthetic Integration](https://www.imandra.ai/) are developing tools and techniques for formal verification of distributed systems. For our ROS-related project, we are working on OCaml client for ROS and we are creating tools and wrappers that allow one to formally reason about ROS node models. With our [Imandra](https://www.imandra.ai/) reasoning engine you can formally verify statements about models written in OCaml, and the same model can be compiled and executed as a ROS node. 

Check our medium post:[https://medium.com/imandra/imandra-interface-to-robot-os-part-i-9f3888c5c3a1](https://medium.com/imandra/imandra-interface-to-robot-os-part-i-9f3888c5c3a1) where we are describing our approach to the creation of a simple model of a ROS node.





---
[Visit Topic](https://discourse.ros.org/t/formal-verification-of-ros-nodes-using-imandra-reasoning-engine/5655/1) or reply to this email to respond.