rust

9 статей

9 июл. 2026 г.

AutoVerus превращает 40 часов написания proof в 3 вызова LLM. Хитрость в том, чтобы знать, когда сдаваться.

AutoVerus использует сеть агентов LLM для генерации proof корректности Verus для кода на Rust, автоматизируя более 90% proof obligations через цикл generate-repair-discharge, управляемый обратной связью SMT-solver.

8 июл. 2026 г.

LLM могут генерировать код на Rust. Формальные доказательства — это совершенно другая проблема.

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

model-checking llm rust formal-proofs

5 июл. 2026 г.

Можно доказать корректность кода на Rust, не написав ни одного доказательства, но пространство состояний — это плата

Инструменты model checking вроде Kani позволяют верифицировать свойства Rust с помощью assertions вместо формальных доказательств. Проблема в том, что происходит, когда ваши циклы не имеют маленьких границ.

model-checking rust verification formal-methods

26 июн. 2026 г.

Ваши зависимости могут читать любые файлы на диске. cap-std заставляет их запрашивать разрешение.

Стандартная библиотека Rust предоставляет окружающее файловое полномочие каждой зависимости. cap-std заменяет его API на основе полномочий, которые заставляют код доказывать, что у него есть право доступа к пути, прежде чем он откроет его.

capability-based-security rust cap-std sandboxing

22 июн. 2026 г.

Хватит выбрасывать ошибки, которые не видит ваша система типов

Выброшенные исключения скрывают пути отказа от вашей системы типов. Вот почему явный возврат ошибок делает ваш код более честным, и как перейти на него, не ненавидя свою жизнь.

type-level-correctness error-handling typescript rust

21 июн. 2026 г.

Newtypes в Rust делают некорректные состояния невыразимыми на этапе компиляции бесплатно

Однополевая обёрточная структура ловит баги смешения единиц измерения и путаницу типов, не добавляя ни одного байта накладных расходов.

type-level-correctness rust newtypes zero-cost-abstractions

28 мая 2026 г.

Mutation testing в Rust работает, но ваше время компиляции этого не простит

cargo-mutants находит тесты, которые только притворяются, что проверяют ваш код. Вот как работает mutation testing в Rust, что он ловит и стоит ли затрат времени компиляции.

deep-dives mutation-testing rust cargo-mutants test-quality

23 мая 2026 г.

Тесты на основе свойств в Rust находят баги, которые пропускают ваши юнит-тесты

Тестирование на примерах покрывает только те входные данные, о которых вы подумали. Тестирование на основе свойств генерирует случайные данные, проверяет инварианты и сокращает ошибки до минимальных контрпримеров.

deep-dives rust property-based-testing quickcheck proptest

21 мая 2026 г.

Runtime contracts в Rust могут быть бесплатными в релизных сборках, но компилятор не сделает это за вас

Rust автоматически удаляет debug assertions, но настоящий design-by-contract требует большего, чем debug_assert!. Вот как построить zero-cost runtime contracts, которые исчезают из вашего релизного бинарника.

deep-dives rust runtime-contracts performance