The doctoral work of Atef Azaiez shows how mathematical verification can guide the design of farm robots and keep them safe in the field, with a fallback ready for the unexpected.
Robots are moving out of fenced factory halls into fields, orchards and polytunnels, where they work close to people and plants. In his thesis, Atef Azaiez studied how engineers can show that such robots are safe, by using formal methods. These are mathematical techniques that check a model of the robot against every situation the model allows, instead of only the situations a test team thought to try.
A review of 180 studies published between 2007 and 2024 found that researchers mostly apply these techniques to a design that is already fixed, or use them to monitor a robot while it runs. Agriculture made up two per cent of the applications. Few studies dealt with robot components that learn from data, such as camera-based plant recognition.
Azaiez then developed two methods for the stages earlier work had barely touched, and tested them on a model of a robot working among strawberry plants in a polytunnel.
The first method lets engineers compare design ideas mathematically before anyone builds hardware, and drop the ideas that cannot meet the safety requirements. The second runs on the robot during work. A planner adjusts the robot’s behavior when conditions change, while a separate supervisor keeps an emergency action ready and switches to it when needed.
What are the most important results?
The central finding is that mathematical guarantees for robots of this kind cannot cover everything. Some learning-based components cannot be described precisely enough to check, and a complete robot is too large to analyze in full.
The thesis states what each method covers and what it leaves out. It then builds the safety argument so that it does not depend on the unchecked parts behaving well.
What was the goal of the research?
The work set out to find at which stages of a robot’s development engineers can establish formal safety guarantees, and what can support a safety claim at the stages where they cannot.
Why is this research important?
A robot that works without a fence needs a safety claim that convinces regulators, certification bodies and the farmer who runs it. Testing covers only the situations someone tried. A mathematical guarantee covers every situation in the model, but it stops holding, without warning, once real conditions move outside that model. In a field this happens more often than in a factory, because light, weather and plants change from day to day.
For research on robot safety, Azaiez' thesis brings formal methods into two stages with little prior work: early concept design and operation in the field. Neither method depends on the strawberry case, so engineers could apply them to other robots in open environments. The thesis does demonstrate them on only one platform. More broadly, the approach can help manufacturers give certification bodies formal evidence from the earliest design decisions. It can also give farmers robots whose safety claims say what they cover.
The work was part of the RoboFarmer project, funded by the Research Council of Norway.
Atef Azaiez will defend his thesis, Assurance of Safety and Reliability of Robotic Autonomous Systems: Handling Uncertainties Through Model Checking, on 20 November 2026. Read more about the event here.