Мой проект выходного дня: полностью автономно написать сетевой сервис на C. Да, именно на C, чтобы агенты со всякими borrow checkers не расслаблялись 🙃

Процесс выглядел так:
1. Найти и скачать спеку на протокол
2. Написать три документа: дизайн с декомпозицией, реализацию и план тестирования на соответствие спеке
3. Написать код сервиса и функциональных тестов
4. Провести аудит на полноту функциональных тестов
5. Провести валидацию через сторонний клиент
6. Провести перформанс-тест: держать 10к клиентов с латенси <10 мс
7. Добиться 100% покрытия кода тестами и отловить все ошибки asan/ubsan
8. Верифицировать с помощью CBMC (вместо фаззинга)

100% каверадж оказывается получается довольно просто, через fault injection в тестах.

MC/DC — модель начинает жутко срезать углы, потому что не может сама легко подобрать инпут под условие, но надежа есть.

CBMC — пока так себе, но я особо даже и не рассчитывал, что до этого дойдет, поэтому плохо описал критерии приемки этапа.

Конечно, я ещё нашел там парочку крашей после этого, но они скорее следствие плохого использования CBMC — я выставил требование, что должно отработать за 3 мин и моделька стала срезать углы.

Я полагал, что агенты осилят только часть задач, но все дошли до финиша, и всё даже работает 🤯