vera

Vera - язык программирования, созданный для написания LLM, а не людьми. Исходная предпосылка: главный сбой сгенерированного LLM кода кроется не в синтаксисе, а в связности на масштабе: инварианты размываются между файлами, возникают ошибки именования (вводящие в заблуждение имена, повторное использование имён, потерянные ссылки - см. arXiv:2307.12488) и неверные рассуждения о состоянии во времени. Vera пытается перевести эти ошибки в разряд сбоев компиляции.

Компилятор представляет собой эталонную реализацию на Python, которая компилирует в WebAssembly и работает через CLI или в браузере. Автор - Alasdair Allan (автор книг по IoT и мейкерству, по образованию также физик).

Три архитектурных решения, определяющих всё остальное

Никаких имён переменных. Привязки адресуются типизированными индексами Де Брёйна - @Int.0 обозначает самую свежую привязку типа Int в области видимости, @Int.1 - предшествующую ей. Ошибки, вызванные путаницей в именах, исчезают, потому что путать нечего. Отдельно сама концепция описана в typed-de-bruijn-for-llms.

Обязательные контракты. У каждой функции между сигнатурой и телом расположены секции requires(), ensures() и effects(). Сигнатура - это спецификация, а не просто тип. Z3 статически доказывает контракты Tier-1 (разрешимая арифметика, сравнения, булевы выражения, ADT, завершаемость); контракты, которые решатель не может доказать, становятся проверками во время выполнения Tier-3.

Алгебраические эффекты в сигнатурах. Функция, вызывающая LLM, объявляет effects(<Inference>); функция, отправляющая HTTP-запросы, объявляет effects(<Http>). Вызывающий код обязан разрешить всю строку эффектов. Чистые функции объявляются как effects(pure), и компилятор строго за этим следит. Это ближе к Koka или F*, чем к IO в Haskell: строка эффектов крепится к функциональной стрелке, а не сидит в типе возвращаемого значения.

public fn safe_divide(@Int, @Int -> @Int)
  requires(@Int.1 != 0)
  ensures(@Int.result == @Int.0 / @Int.1)
  effects(pure)
{
  @Int.0 / @Int.1
}

Деление на ноль в Vera - это не ошибка во время выполнения, а ошибка типов, отлавливаемая в каждом месте вызова.

Ошибки сформулированы для модели, написавшей код

Диагностика включает суть ошибки, причину, конкретный исправленный пример и ссылку на спецификацию. Каждая ошибка имеет стабильный код (E001-E702) и доступна в виде структурированного JSON через флаг --json для циклов обратной связи агентов:

[E001] Error at main.vera, line 14, column 1:
  Function is missing its contract block. Every function in Vera must declare
  requires(), ensures(), and effects() clauses between the signature and the body.
  Fix: ...
  See: Chapter 5, Section 5.1 "Function Structure"

Флаг --json выдаёт замысел. Весь язык относится к LLM как к основному пользователю - вывод ошибок отформатирован под автономный цикл, а не под человека в терминале.

Инструментарий для агентов

Репозиторий поставляется с файлами SKILL.md, AGENTS.md, CLAUDE.md и DE_BRUIJN.md - отдельными документами для Claude Code, типовых агентных систем и академической справкой по слотовой системе. Claude Code автоматически находит skill в репозитории; для других проектов он устанавливается в ~/.claude/skills/vera-language/SKILL.md.

Рабочий процесс

vera check    # parse + type-check
vera verify   # add Z3 contract verification
vera run      # compile to WASM + execute
vera test     # contract-driven testing
vera fmt      # canonical formatter

vera compile --target browser генерирует самодостаточный бандл (wasm + JS runtime + HTML), а система сборки прогоняет тесты на паритет, чтобы поведение в CLI и браузере оставалось одинаковым.

VeraBench

Сопутствующий бенчмарк автора (vera-bench) содержит 50 задач в 5 уровнях сложности на 6 моделях от 3 провайдеров. Заявленные главные цифры: Kimi K2.5 показывает 100% run_correct на Vera против 86% на Python и 91% на TypeScript; три модели обошли TypeScript на Vera; среднее значение для флагманских моделей составляет 93% на Vera против 93% на Python. Это разовый прогон с высокой дисперсией - не окончательный вердикт, но ранний сигнал указывает на то, что "специально созданные ограничения повышают корректность, не снижая беглость генерации".

Статус и watchlist

На момент импорта версия v0.0.127, репозиторий создан 2026-02-22 (возраст около 10 недель), 810+ коммитов, 127 релизов, 261 звезда, лицензия MIT, один автор. Компилятор включает парсер, проверку типов, верификатор контрактов на Z3, генерацию кода WASM, модульную систему, среду выполнения для браузера и вставку контрактов во время выполнения. Спецификация из 13 глав находится в статусе черновика. В roadmap главной целью обозначен верифицированный сервер инструментов MCP.

Добавлен в watchlist - один автор, проект очень молодой, намеренно плывущий против привычек экосистемы (отсутствие имён переменных трудно продать). Вопросы для следующей проверки: пишет ли кто-то нетривиальный код на Vera помимо Alasdair, появятся ли независимые воспроизведения VeraBench и будет ли закрыт этап с верифицированным MCP-сервером.

Перекрёстные ссылки

• typed-de-bruijn-for-llms - концепция ссылок через слоты отдельно от Vera.
• vamp-ai-frontend - та же идея на стороне фронтенда: явные, изначально спроектированные под ИИ языковые интерфейсы превосходят традиционные при генерации кода.
• clippy-stricter-config - вариант доработки существующего: ужесточение языка линтерами вместо полной перестройки синтаксиса.
• clean-code-coding-agents - экономика контекстного окна, стимулирующая дизайн языков под ИИ.

Репозиторий

https://github.com/aallan/vera - 261 звезда, MIT, Python (компилятор) / WASM (среда выполнения).