# Пошаговое руководство: как использовать LLM для формальной верификации кода и поиска логических ошибок

> AI Release · @ai_release1 · https://ai-release.org/guides/poshagovoe-rukovodstvo-kak-ispolzovat-llm-dlya-formalno.html

## TL;DR

- Время выполнения: 40–60 минут
- Уровень сложности: Intermediate
- Понадобится: Python 3 и pip (минимальную версию сверьте с документацией пакета `z3-solver`), пакет `z3-solver` из PyPI, терминал, редактор, доступ к LLM (облачный API или локальная модель)

Роли в процессе жёстко разделены: LLM пишет черновик спецификации и переводит код в формулу, решатель Z3 ищет контрпример, человек подтверждает контрпример запуском обычного Python-кода.

| Этап | Кто делает | Артефакт |
|---|---|---|
| Контракт (пред-/постусловия) | LLM + человек | `contract.md` |
| Формула для решателя | LLM | `verify_withdraw.py` |
| Доказательство или контрпример | Z3 | `sat` / `unsat` |
| Подтверждение на реальном коде | Python | воспроизведённый баг |

## Требования и подготовка
![Иллюстрация к разделу «Требования и подготовка»](https://ai-release.org/guides/img/poshagovoe-rukovodstvo-kak-ispolzovat-llm-dlya-formalno-ru-1.jpg?v=1792789785)


- ОС: Linux, macOS или Windows с WSL — команды ниже даны для bash.
- Python 3 и pip в `PATH`.
- Свободное место под виртуальное окружение и пакеты — точный размер сверьте с документацией `z3-solver`.
- Доступ к LLM: либо ключ к API hosted-модели (порядок вызова описан в гайде [Как использовать GPT-6.1 Sol через API: полное руководство](https://ai-release.org/guides/kak-ispolzovat-gpt-6-1-sol-cherez-api-polnoe-rukovodstv.html?utm_source=tg&utm_medium=channel&utm_campaign=guide_inline&utm_content=guide_to_guide)), либо локальный сервер, если код нельзя отдавать наружу — см. [Как подключить ИИ к домашнему серверу](https://ai-release.org/guides/kak-podklyuchit-ii-k-domashnemu-serveru-poshagovoe-ruko.html?utm_source=tg&utm_medium=channel&utm_campaign=guide_inline&utm_content=guide_to_guide).
- Права на запись в рабочую папку проекта.

**Что сделать:** создайте изолированное окружение и поставьте решатель.

**Зачем:** Z3 — SMT-решатель (программа, которая проверяет выполнимость логических формул и выдаёт конкретные значения переменных, если формула выполнима). Глобальная установка часто конфликтует с системным Python.

**Как проверить:** команды ниже должны завершиться без ошибок, а импорт — напечатать версию.

```bash
python3 --version
mkdir -p ~/llm-verify && cd ~/llm-verify
python3 -m venv .venv
source .venv/bin/activate
pip install z3-solver
python -c "import z3; print(z3.get_version_string())"
```

**Пример:** последняя строка печатает что-то вида `4.x.x` — конкретный номер у вас будет свой, сверьтесь с документацией пакета. Если вместо номера появилось `ModuleNotFoundError: No module named 'z3'` — окружение не активировано, см. раздел проблем.

## Шаг 1. Зафиксируйте контракт и воспроизведите ошибку вручную

**Что сделать:** возьмите одну функцию, в которой подозреваете логическую ошибку, и выпишите её контракт: предусловие (что должно быть верно на входе), постусловие (что обязано быть верно на выходе) и инвариант (что не должно меняться). Затем воспроизведите баг конкретным вызовом.

**Зачем:** решатель проверяет не «код вообще», а соответствие кода контракту. Без записанного контракта LLM придумает свой, и проверка будет бессмысленной. Ручное воспроизведение нужно как эталон: им вы потом будете ловить галлюцинации модели.

**Как проверить:** скрипт печатает отрицательный баланс — значит, баг реален.

```python
# billing.py
def withdraw(balance: int, amount: int) -> int:
    """Списывает amount с комиссией 1% (все суммы в копейках)."""
    fee = amount // 100
    if balance >= amount:          # ошибка: комиссия не учтена в проверке
        return balance - amount - fee
    return balance
```

```bash
python3 -c "from billing import withdraw; print(withdraw(100, 100))"
```

**Пример:** вывод — `-1`. Баланс ушёл в минус, хотя требование «баланс не может стать отрицательным» нарушено.

Контракт фиксируем в `contract.md` как таблицу — это вход для LLM:

| Элемент | Формула | Источник |
|---|---|---|
| Предусловие | `balance >= 0`, `amount >= 0` | требование «суммы неотрицательны» |
| Постусловие | `result >= 0` | требование «баланс не уходит в минус» |
| Инвариант | если `balance < amount + fee`, вернуть `balance` | тело функции |

Почему это работает: любая логическая ошибка — это вход, при котором предусловие выполнено, а постусловие нет. Задача решателя — такой вход найти.

## Шаг 2. Переведите тело функции в формулу Z3 с помощью LLM и запустите поиск контрпримера
![Иллюстрация к разделу «Шаг 2. Переведите тело функции в формулу Z3 с помощью LLM и запустите поиск контрпримера»](https://ai-release.org/guides/img/poshagovoe-rukovodstvo-kak-ispolzovat-llm-dlya-formalno-ru-2.jpg?v=1792789796)


**Что сделать:** отправьте LLM тело функции и контракт с запросом на перевод в z3py, затем сохраните ответ в файл и запустите.

**Зачем:** ручной перевод на язык SMT — самая долгая и самая ошибкоопасная часть; LLM делает её за минуту. Но перевод остаётся черновиком: доверять ему нельзя, проверять надо результатом.

**Как проверить:** скрипт печатает `check: sat` и конкретные значения переменных.

```text
Ты — инженер по формальной верификации. Переведи тело функции withdraw
в формулу z3py. Требования:
1. Целочисленное деление amount // 100 запиши как amount / 100 для Int.
2. Используй If(cond, then_value, else_value), не пиши def.
3. Добавь предусловия balance >= 0 и amount >= 0 как ограничения Solver.
4. Добавь отрицание постусловия result >= 0 как ограничение Solver.
5. Печатай check(), а при sat — модель и значение result.
Не добавляй пояснений, только код.
```

```python
# verify_withdraw.py
from z3 import Ints, Solver, If, sat

balance, amount = Ints('balance amount')
fee = amount / 100

result = If(balance >= amount, balance - amount - fee, balance)

s = Solver()
s.add(balance >= 0, amount >= 0)   # предусловие из contract.md
s.add(result < 0)                  # отрицание постусловия

print("check:", s.check())
if s.check() == sat:
    m = s.model()
    print("balance =", m[balance])
    print("amount  =", m[amount])
    print("result  =", m.eval(result))
```

```bash
python3 verify_withdraw.py
```

**Пример:** ожидаемый вывод — `check: sat` и модель, где `result = -1`, например `balance = 100`, `amount = 100`. Конкретные числа Z3 может выбрать другие — важна не модель, а вердикт `sat` и значение `result < 0`.

Почему это работает: `sat` означает «формула выполнима», то есть существует вход, при котором предусловие истинно, а постусловие ложно. Это и есть найденный контрпример — вход, ломающий код.

## Шаг 3. Подтвердите контрпример, исправьте код и докажите отсутствие ошибки
![Иллюстрация к разделу «Шаг 3. Подтвердите контрпример, исправьте код и докажите отсутствие ошибки»](https://ai-release.org/guides/img/poshagovoe-rukovodstvo-kak-ispolzovat-llm-dlya-formalno-ru-3.jpg?v=1792789804)


**Что сделать:** прогоните найденные Z3 значения через настоящую функцию, исправьте код, перезапустите проверку до `unsat`, отдельно убедитесь, что спецификация не пустая.

**Зачем:** `sat` от LLM-перевода может быть артефактом модели. Пока контрпример не воспроизвёлся в Python, это гипотеза, а не баг. А `unsat` без проверки на вакуумность может означать, что предусловия невыполнимы и доказывать нечего.

**Как проверить:** три шага ниже дают `-1` (баг подтверждён), затем `unknown`-безопасный `unsat` и `sat` для самих предусловий.

```bash
python3 -c "from billing import withdraw; print(withdraw(100, 100))"
# -1  -> контрпример воспроизвёлся
```

Исправление — комиссия входит в проверку:

```python
# billing.py (после исправления)
def withdraw(balance: int, amount: int) -> int:
    fee = amount // 100
    if balance >= amount + fee:
        return balance - amount - fee
    return balance
```

В `verify_withdraw.py` замените строку с `result` на ту же логику:

```python
result = If(balance >= amount + fee, balance - amount - fee, balance)
```

```bash
python3 verify_withdraw.py   # ожидаем: check: unsat
```

Проверка на вакуумность — предусловия должны быть выполнимы:

```python
s2 = Solver()
s2.add(balance >= 0, amount >= 0)
print("preconditions:", s2.check())   # ожидаем: sat
```

Чек-лист перед тем, как считать задачу закрытой:

- [ ] Контрпример из модели воспроизведён реальным вызовом функции.
- [ ] Исправление внесено и в код, и в формулу Z3 (это два разных файла).
- [ ] Повторный запуск даёт `unsat`.
- [ ] Проверка предусловий даёт `sat`.
- [ ] Старые тесты проекта проходят: `python -m pytest -q`.

**Пример:** до исправления — `sat` + `result = -1`; после — `unsat`. Разница в одну строку условия — это и есть та логическая ошибка, которую не поймал ни один обычный тест.

## Возможные проблемы и решения

**Проблема. Скрипт не видит пакет z3**

- Ошибка: `ModuleNotFoundError: No module named 'z3'`
- Причина: пакет поставлен в один интерпретатор, а запуск идёт из другого, либо окружение не активировано в текущей сессии терминала.
- Решение: активируйте окружение и проверьте, каким Python вы запускаете файл:
```bash
source .venv/bin/activate
python -c "import sys; print(sys.executable)"
pip install z3-solver
```
Путь в выводе должен указывать внутрь `~/llm-verify/.venv/`.

**Проблема. Z3 выдаёт `unsat`, а баг руками воспроизводится**

- Ошибка: в консоли `check: unsat`, при этом `python3 -c "from billing import withdraw; print(withdraw(100, 100))"` печатает `-1`
- Причина: LLM потерял часть тела функции при переводе (в нашем случае выпал член `- fee`), и проверялась формула, а не ваш код. Это ложное доказательство — самая опасная ошибка в этом процессе.
- Решение: постройте diff между телом функции и формулой, добавьте в промпт требование вывести формулу построчно с комментарием к каждой ветке, и обязательно прогоняйте конкретные тесты рядом с `unsat`:
```bash
python3 -c "from billing import withdraw; print(withdraw(100, 100), withdraw(0, 0), withdraw(1000, 100))"
```
Если хотя бы один вывод расходится с формулой — правьте формулу, а не тест.

**Проблема. Проверка не завершается вердиктом**

- Ошибка: `check: unknown` и `z3.z3types.Z3Exception: model is not available` при попытке взять модель
- Причина: решатель не смог доказать выполнимость или невыполнимость — типично для нелинейной арифметики (умножение двух переменных друг на друга) и для слишком большой области значений. Вызов `model()` при `unknown` или `unsat` невозможен.
- Решение: сначала проверяйте вердикт, потом берите модель, и сузьте область:
```python
r = s.check()
print("reason:", s.reason_unknown())
if r == sat:
    print(s.model())
```
Дробите задачу: замените `a * b` на умножение на константу, ограничьте переменные (`amount <= 100000`) или перейдите на битовые векторы (`BitVec`) — точный синтаксис сверьте с документацией z3py.

## Резюме и следующие шаги

Связка работает так: LLM пишет контракт и формулу, Z3 ищет вход, ломающий постусловие, а вы подтверждаете этот вход реальным запуском и повторяете цикл до `unsat`. Следующий шаг — прогнать этот же цикл по остальным функциям модуля и вынести контракты в docstring, чтобы их нельзя было потерять при рефакторинге.

## FAQ

**Чем это отличается от обычных тестов?**
Тест проверяет несколько конкретных входов, которые вы придумали; SMT-решатель перебирает все входы, удовлетворяющие предусловию, и либо находит контрпример, либо доказывает, что его нет. Поэтому `unsat` сильнее сотни тестов, но только при корректно записанном контракте.

**Можно ли доверять LLM при переводе кода в формулу?**
Нет. Ответ модели — черновик, который проверяется двумя способами: вердиктом решателя и воспроизведением контрпримеров в реальном коде. Ошибка перевода даёт ложный `unsat`, поэтому шаг с прогоном конкретных тестов пропускать нельзя.

**Нужен ли платный API?**
Не обязателен: подойдёт любая модель с достаточным контекстом, включая локальную на своём сервере — это единственный вариант, если код не может покидать контур компании. Порядок подключения локального варианта разобран в [гайде по self-hosted сервисам](https://ai-release.org/guides/kak-podklyuchit-ii-k-domashnemu-serveru-poshagovoe-ruko.html?utm_source=tg&utm_medium=channel&utm_campaign=guide_inline&utm_content=guide_to_guide).

**Подойдёт ли метод для больших проектов на Go или Java?**
Техника та же, но вручную переводить тысячи строк в z3py нерационально: для промышленного масштаба используют дедуктивные верификаторы и аннотации в коде, а не ручной перевод. Конкретные инструменты и их ограничения сверьте с их документацией — в этом гайде проверен только путь «Python + z3-solver».