Existuje několik specifikačních jazyků (např. ACSL), ve kterých může uživatel složité vlastnosti, které pak může použít jako aserce v počítačových programech. Důležitý scénář použití takovýchto jazyků jsou aserce, které ověřují jestli daná funkce v určitém programovacím jazyku splňuje svoji specifikace. Cílem tohoto tématu je psaní nástroje, pomocí kterého uživatel se může úplně vyhnout psaní kódu: nástroj by měl ze specifikace funkce automaticky vytvořit kód, který tuto specifikaci splní.