BehaVerify: Formal Verification for Behavior Trees

BehaVerify is a Python toolbox that takes a behavior-tree specification and produces a formally verified model, an executable runtime, and a publication-quality diagram — from a single .tree source file.

BehaVerify end-to-end pipeline: inputs (.tree, .onnx, .smv) flow through a TextX parser, model builder, and internal IR; the IR is lowered by six code generators (nuxmv, python, cpp, haskell, latex, monitor) into SMV, py_trees, BT.CPP, Haskell, TikZ, and runtime-monitor artefacts, which feed three verification strategies (model checking, simulation, runtime monitors).

Note

BehaVerify is an active research tool first released at SEFM 2022 and maintained at Vanderbilt’s VeriVITAL lab. The landing diagram above is the same pipeline that underlies every peer-reviewed result; see Publications.

Behavior-tree DSL

A compact TextX grammar — seven blocks, prefix-notation expressions, first-class temporal operators.

The .tree DSL
Seven generation modes

nuxmv, python, cpp, haskell, latex, trace, grid — single DSL, many targets.

Generation Modes
Neural leaves (ONNX)

Drop ONNX classifiers or regressors straight into an action; formally verify the composed neuro-symbolic tree.

Neural-Network Leaves
Scales past 2,000 nodes

Fast-forwarding SMV encoding + aggressive node trimming = verification at industrial tree sizes.

Encodings
Contingency monitors

Compile an LTL formula into a runtime monitor that can fire a BT action when violated.

Specifications
Reproducibility baked in

Every paper ships its own REPRODUCIBILITY/<year>_<venue>/ directory with Docker, timing scripts, and expected results.

Publications

What flows through the pipeline

The landing diagram above annotates every file type. In one sentence:

Inputs are a .tree behavior-tree description, optional .onnx neural-network weights, and (optionally) an already-compiled .smv model. The core pipeline parses the DSL, runs static validation, and builds an internal IR of nodes, variables, and expressions. Code generators lower that IR into six target languages. The resulting artefacts then feed the verification strategies:

Strategy

What it answers

Model checking (nuXmv on .smv)

Is every reachable state safe? Does every path eventually reach the goal? Any LTL/CTL query in the specifications block.

Simulation (py_trees on .py)

How does the tree behave under a specific input trace or random seed?

Runtime monitors

On a deployed robot, has the specification just been violated? If yes, run the trigger_action.

Getting started

Installation

pip install . plus nuXmv for the verification mode.

Installation
Quickstart

End-to-end DrunkenDrone in five minutes.

Quickstart
Your first model

Author a minimal .tree file from scratch.

Your First Model