PROMELA ( PROtocol MEta LAnguage ) je specifikační jazyk pro asynchronní systémy, což jinými slovy znamená, že tento jazyk umožňuje popis souběžných systémů, jako jsou komunikační protokoly . Umožňuje dynamické vytváření procesů. Komunikace mezi těmito různými procesy může být prováděna sdílením globálních proměnných nebo pomocí komunikačních kanálů. Je tedy možné simulovat synchronní nebo asynchronní komunikaci.
V PROMELA není rozdíl mezi pokyny a podmínkami. Pokyn lze předat, pouze pokud je spustitelný, podmínka pouze v případě, že je pravdivá. Jinak je proces blokován, dokud se podmínka nestane pravdivou.
Promela je spojena s nástrojem pro ověření Spin.