[ros-users] [Discourse.ros.org] [ROS-Industrial] Using Safety Protocols with ROS

[Kostya Kanishev]

Hi! 

Not sure this is relevant to the original discussion -- I've just noticed "safety" and "protocols" in the name of the topic. At [our company](https://www.imandra.ai/), we are working on tools and techniques for ensuring the safety and reliability of communication protocols by means of formal verification. So far we've been focusing on these types of problems in finance -- FinTech is essentially a distributed system of independent nodes communicating via messaging protocols. ROS looks like exactly the same kind of system, so we've also started a ROS-related project. 

We are working on the creation of ROS-OCaml client -- if your code is written in a pure subset of OCaml, then it can be reasoned about using our Imandra proof assistant. Using Imandra, one can mathematically verify statements about your OCaml code, and it helps you to precisely formulate these formal statements by giving you counterexamples to your false claims. This allows you to create extremely reliable, precise and safe code and specification for it.

[1]: [Aesthetic Integration](https://www.imandra.ai/)
[2]: [Try our Imandra reasoning engine in the browser](https://try.imandra.ai/)
[3]: The GitHub of the project: [https://github.com/AestheticIntegration/imandra-ros](https://github.com/AestheticIntegration/imandra-ros)





---
[Visit Topic](https://discourse.ros.org/t/using-safety-protocols-with-ros/5561/9) or reply to this email to respond.