Hello! We at Aesthetic Integration 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 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 where we are describing our approach to the creation of a simple model of a ROS node.