Bridging higher-order logic and efficient computations for a rigorous analysis of idealised pathfinding ants

We present a novel approach to modelling and verifying ant colony pathfinding behaviour in an idealised scenario mirroring the double bridge experiment from biological research. We implement our analysis framework in the HOL Light proof assistant to provide rigorous verification of emergent collective dynamics. Unlike most of the existing approaches, which are limited by state explosion or fixed-size constraints, we formally prove that an ant colony of any size converges on the optimal path, given specified preconditions. This establishes that the selection of a shortest path is a stable, emergent property independent of the colony’s population. To enhance the computational performance of the analysis on colonies of a given size, we implement a faithful translation between HOL Light and SMT-LIB2. This bridge allows proof obligations to be discharged efficiently by modern SAT solvers, thereby integrating the expressive power of higher-order logic with the speed of automated reasoning tools, and creating a division of labour between formal verification and dynamic simulation. Our work advances the application of computerised mathematics to collective adaptive systems, providing a unified framework for modelling, simulation, and formal verification.