// the find
tier4/safe_drive
safe_drive: Formally Specified Rust Bindings for ROS2
Rust bindings for ROS2 with a twist: the executor's scheduling algorithms are formally specified in TLA+ and model-checked for deadlock and starvation freedom. This is for robotics engineers who've been burned by rclcpp's starvation bugs and want memory safety plus verified concurrency guarantees. Not a hobby project — tier4 ships autonomous vehicles with this stack.
The TLA+ specifications are actually included in the repo and verifiable, not just claimed in a README. The starvation fix is a real improvement over rclcpp — the original ROS2 executor has a known scheduler bug this addresses formally. Zero-copy transport and custom allocator support are included, which matter a lot in real-time robotics where heap allocation in hot paths is death. Supports async/await natively, which means you get Rust's async ecosystem instead of callback spaghetti.
117 stars after what appears to be several years of work signals limited adoption — if you hit a bug, you're probably debugging it yourself. Last push was March 2025 and the activity cadence looks sparse, which is a real concern for a safety-critical dependency. The Galactic EOL support is already dropped but still in the tree, suggesting maintenance bandwidth is thin. The generated message bindings live in a separate repo (safe_drive_msg) and cover common_interfaces — custom message types from your own packages require running the code generator yourself, which adds friction to the setup.