Исправление hateyoufeel, (текущая версия) :
Прямо как ты хочешь нету, но для верификации есть Frama-C.
А вообще можно просто eDSL на хацкелле верифицировать и в C компилить. Я видел типизированный ассемблер для 6502, сделанный таким образом.
Исходная версия hateyoufeel, :
Прямо как ты хочешь нету, но для верификации есть Frama-C.