Библиотеки, написанные на Coq

CompCert

Компилятор C, официально проверенный CompCert.
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

Добавьте алгоритм сталинской сортировки на любом языке, который вам нравится ❣️, если хотите, дайте нам ⭐️.
  • 1.2k
  • MIT

Coq-HoTT

Библиотека Coq для теории гомотопических типов.
  • 1.2k
  • GNU General Public License v3.0

UniMath

Эта библиотека coq предназначена для формализации значительной части математики с использованием универсальной точки зрения.
  • 853
  • GNU General Public License v3.0

magmide

Язык проверки с зависимой типизацией, предназначенный для того, чтобы сделать возможным доказуемо правильный программный код для работающих разработчиков программного обеспечения.
  • 771

fiat-crypto

Генерация криптографического примитивного кода с помощью Fiat.
  • 594
  • GNU General Public License v3.0

math-comp

Математические компоненты.
  • 501

CoqGym

Учебная среда для доказательства теорем с помощником по доказательству Coq.
  • 332
  • GNU Lesser General Public License v3.0 only

sail-riscv

Модель паруса RISC-V.
  • 306
  • GNU General Public License v3.0

proofs

Мой личный репозиторий официально проверенной математики..
  • 259
  • GNU General Public License v3.0

hacspec

Язык спецификации для криптографических примитивов.
  • 218
  • MIT

Coq-Equations

Пакет определения функции для Coq.
  • 197
  • GNU Lesser General Public License v3.0 only

verdi-raft

Реализация протокола распределенного консенсуса Raft, проверенная в Coq с использованием инфраструктуры Verdi.
  • 168
  • BSD 2-clause "Simplified"

jasmin

Язык высоконадежной и высокоскоростной криптографии (от jasmin-lang).
  • 159
  • MIT

analysis

Библиотека анализа, совместимая с математическими компонентами (от math-comp).
  • 158
  • GNU General Public License v3.0

fiat

В основном автоматизированный синтез программ правильного построения.
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

Появление Code 2018 в Coq! (https://adventofcode.com/2018).
  • 139

fourcolor

  • 131
  • GNU General Public License v3.0

kami

Платформа для высокоуровневой параметрической спецификации оборудования и ее модульной проверки (от mit-plv).
  • 126
  • MIT

corn

  • 108
  • GNU General Public License v3.0 only

toychain

Минималистичный блокчейн-консенсус, реализованный и проверенный в Coq.
  • 106
  • BSD 2-clause "Simplified"

koika

Основной язык для проектирования оборудования на основе правил 🦑.
  • 104
  • GNU General Public License v3.0 only

silveroak

Официальная спецификация и проверка оборудования, особенно для обеспечения безопасности и конфиденциальности.
  • 97
  • Apache License 2.0

coq-library-undecidability

Библиотека механизированных доказательств неразрешимости в помощнике по доказательству Coq.
  • 96
  • GNU General Public License v3.0

ConCert

Фреймворк для проверки смарт-контрактов в Coq.
  • 92
  • MIT

riscv-coq

Спецификация RISC-V в Coq.
  • 87
  • BSD 3-clause "New" or "Revised"

vericert

Формально проверенный инструмент высокоуровневого синтеза, основанный на CompCert и написанный на Coq..
  • 71
  • GNU General Public License v3.0 only

hs-to-coq

Преобразование исходного кода Haskell в исходный код Coq.
  • 69
  • MIT

scala-escape

Плагин компилятора для управления временем жизни объектов в Scala (от TiarkRompf).
  • 62
  • BSD 3-clause "New" or "Revised"

rupicola

Набор инструментов для компиляции Gallina в Bedrock2.
  • 46
  • MIT