《日経Robo》ファナックが買収したロボベンチャー、ソフトの技術力で群を抜くファナックが2018年2月に買収したロボットベンチャーのライフロボティクス。伸縮式の機構を採用することでロボットの肘関節をなくし、省スペースに設置できる協働ロボット「CORO」を手掛ける（図1）。 トヨタ自動車や外食大手の吉野家、ロイヤルホストなどが相次いで自社工場・店舗への採用を決定するなど、注目が高まりつつある（導入事例の記事）。 このライフロボティクスというベンチャー、実はロボットのハードウエア面だけでなく、ロボットに組み込むソフトウエアの面でも、その開発において先駆的なアプローチを取り入れている。それが「形式手法（formal methods）」である。 形式手法は日本ではあまり知られていないが、システムやソフトウエアの仕様を厳密に記述し、仕様の品質を高めるための手法である（形式手法については、筆者が2005年に執筆した特集記事「ソフトウエアは硬い」を参照）1）。プログラムなど実装
恊働ロボットCOROの開発における形式的仕様の適用事例
