SAFE Base is a existential-quantifier version of the Swarm Safety Detector, which allows to capture asynchronous execution semantics of parameterized multi-agent systems. Under this execution semantics, agents are not forced to select a local or synchronization action at each step but can freely remain idle.

For the first time, this problem was addressed via model-checking based on satisfiability-modulo theory (SMT): the SAFE verification technique is based on the theory of array-based systems (ABS). Swarm Safety Detector allows you to model your agent templates and environment and translate this into an array-based system representation, ready to be verified by the MCMT model-checker.