Без заголовка

Есть такая немецкая тулза для верификации KeY, она интересно тем, что интерфейс заточен на человека, т.е. работать с ней комфортней и понятней, чем с обычными верификационными тулзами, построенными вокруг формальных моделей. Но он очень медленный, и слаборасширяемый, т.е. тоже не совсем практичный. В данном случае, нужно промежуточное решение - язык/интерфейс для человека и язык для машины. Ну и трансялция между ними, ИДЕ и все такое.