IsabeLLM, инструмент автоматического доказательства теорем в Isabelle, включает фреймворк Retrieval-Augmented Generation, трассировку ошибок и генерацию контрпримеров для улучшения контекста для больших языковых моделей. Обновленная версия демонстрирует улучшенную производительность при проверке консенсусного протокола Proof of Work Биткоина по сравнению с оригиналом.