Coq 로 작성된 라이브러리

CompCert

CompCert는 정식으로 검증된 C 컴파일러입니다.
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

원하는 언어로 스탈린 정렬 알고리즘을 추가하세요 ❣️ 원하시면 ⭐️를 주세요.
  • 1.2k
  • MIT

Coq-HoTT

Homotopy Type Theory를 위한 Coq 라이브러리.
  • 1.2k
  • GNU General Public License v3.0

UniMath

이 coq 라이브러리는 1가 관점을 사용하여 실질적인 수학 체계를 공식화하는 것을 목표로 합니다.
  • 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

Verdi 프레임워크를 사용하여 Coq에서 검증된 Raft 분산 합의 프로토콜의 구현입니다.
  • 168
  • BSD 2-clause "Simplified"

jasmin

높은 보증 및 고속 암호화를 위한 언어(jasmin-lang 제공).
  • 159
  • MIT

analysis

수학 구성 요소 준수 분석 라이브러리(math-comp 제공).
  • 158
  • GNU General Public License v3.0

fiat

Correct-by-Construction 프로그램의 대부분 자동화된 합성.
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

Coq에서 코드 2018 출현! (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

Coq의 RISC-V 사양.
  • 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 to Bedrock2 컴파일 툴킷.
  • 46
  • MIT