BehaVerify Software Tool

BehaVerify is a verification tool for behavior trees, the control structure most widely used to specify robot and game-agent behaviour. Trees are written in BehaVerify’s own domain-specific language and compiled into nuXmv models, so that invariant, CTL and LTL properties can be model-checked against them. Decision nodes backed by neural networks can be supplied as ONNX leaves.

From that same specification the tool generates executable implementations in Python (py_trees), C++ (BT.CPP) and Haskell, along with LaTeX/TikZ diagrams and runtime LTL monitors. The model that was verified and the behaviour that runs on the robot therefore come from one source, rather than from a hand-written model that can drift away from the code it is supposed to describe.

BehaVerify is developed by the VeriVITAL group at Vanderbilt University and led by Serena S. Serbinowska. I am a contributor.