Examples¶

Worked examples from the examples/ directory. Each entry highlights the DSL features it exercises and the verification queries it answers.

DrunkenDrone

Battery-aware navigation; LTL “eventually returns home”.

Collatz

The textbook Collatz recurrence in a 6-node tree.

ACAS-Xu

Neural collision-avoidance cascade (five ONNX models).

Simple Robot with NN

Grid-world navigation with an ONNX policy leaf.

Grid-World (scalability)

49 × 478 obstacle map; BehaVerify’s canonical 2,055-node scalability benchmark.