Programmation Langage Sémantique Prototypage Outil

Question

Existe-t-il un outil pour prototyper une sémantique et un système de type en langage de programmation et qui permet également une sorte de Vérification du modèle des propriétés standard, comme la solidité de type?

Je demande ceci, parce que je lis un livre sur Alliage Et il fournit les fonctionnalités exactes que je veux, mais pour les modèles exprimés en utilisant la logique relationnelle.

Je suis conscient de Ott, mais il n'a pas ce type de capacité de "vérification du modèle", car il se concentre sur la génération de code pour les systèmes d'assistant de preuve.

Toute référence sur une telle existence d'outils serait bien.