O operador universal FORALL é usado para testar condições em que um elemento pertença a um determinado vetor segundo um critério de universalidade. Sua forma de uso é FORALL <elem> IN |vect| : <elem.x> == 10, ou seja, se todos os elem de vect é válido que <elem.x> == 10.