Используете ли вы ACSL в ваших C-программах?

Нет. А тебе следует определиться, используешь ты SPARK или Frama-C. Или Coq на пару с Agda.

Используете ли вы ACSL в ваших C-программах?

Нет, но идея интересная. Спасибо за ссылку

тебе следует определиться

как же я это сделаю, не поковыряв всё по чуть-чуть?

как же я это сделаю, не поковыряв всё по чуть-чуть?

Для начала, перестань ковырять всё одновременно.

Пробовал ниасилил, остановился на lint и тестах.

Я немного тыкал в ACLS. Интересная в общем-то штука, можно эти контракты переводить через Why3 в теоремы(код) на Coq и через Coq доказывать потом. Только это очень долго и муторно. Тебе это может быть нужно только если ты пишешь что-то очень серьезное, вроде софта для АЭС, авионики самолетов, прошивок для автомобилей, кардиостимуляторов. For safety- and security-critical software в общем. Но даже в таких областях на это часто забивают болт. А вот например прошивка для марсохода как раз писалась с использованием подобных инструментов

https://dev.by/news/marsokod-ili-kak-sozdavalos-po-dlya-marsohoda-curiosity

Инструмент Spin для проверки моделей специально предназначен для верификации программ, работающих в распределенных системах и имеющих множество потоков выполнения. Его внутренний проверочный алгоритм основан на методе формальной верификации с применением конечных автоматов, сформулированном Варди и Вольпером. Неформально Spin играет роль фонового планировщика процессов и пытается найти такие варианты выполнения кода в системе, которые нарушают требования, заданные пользователем. Простые примеры типов требований, выполнение которых может быть доказано или опровергнуто таким способом — допустимость программных утверждений и отсутствие сценариев, приводящих к возникновению взаимных блокировок. Но возможности программы для проверки моделей этим далеко не ограничиваются. Инструмент может верифицировать осуществимость или неосуществимость значительно более сложных требований, которые могут быть выражены средствами линейной темпоральной логики.

Попробуй кстати K framework

Для Си вот: https://github.com/kframework/c-semantics

линейной темпоральной логики.

вау, как это звучит!

Приведите примеры опенсорсных проектов, которые используют.

Поиском по гитхабу поищи https://github.com/search?l=C&p=2&q="ensures result"&type=Code

По поводу аналогов этого ACSL:

Для C/C++ есть еще мокросовтофский SAL https://docs.microsoft.com/ru-ru/visualstudio/code-quality/using-sal-annotati...

Для дотнета есть какой-то System.Diagnostics.Contracts https://docs.microsoft.com/en-us/dotnet/api/system.diagnostics.contracts.cont...

Ну и еще Java с этим Java Modeling Language можно найти : https://github.com/kiniry/SenseTile/blob/544e1c5be6109d8381f99233aac80551aef3...

вау, как это звучит!

Да нормально в общем-то звучит. https://ru.wikipedia.org/wiki/Темпоральная_логика

Темпоральная логика (англ. temporal (от лат. tempus) logic) — это логика, в высказываниях которой учитывается временной аспект. Используется для описания последовательностей явлений и их взаимосвязи по временной шкале.

Очевидно, эта логика используется для обнаружения ошибок, характерных для многопоточных приложений (всякие взаимные блокировки, гонки и пр.)