Các thư viện được viết bằng Coq
CompCert
Trình biên dịch C được xác minh chính thức của CompCert.
- 1.6k
- GNU General Public License v3.0
stalin-sort
Thêm thuật toán sắp xếp stalin bằng bất kỳ ngôn ngữ nào bạn thích ❣️ nếu bạn thích, hãy cho chúng tôi một ⭐️.
- 1.2k
- MIT
UniMath
Thư viện coq này nhằm mục đích chính thức hóa một khối toán học quan trọng bằng cách sử dụng quan điểm thống nhất..
- 853
- GNU General Public License v3.0
magmide
Một ngôn ngữ bằng chứng được gõ phụ thuộc nhằm tạo ra mã kim loại trần chính xác có thể chứng minh được cho các kỹ sư phần mềm đang làm việc..
- 771
CoqGym
Môi trường học tập để chứng minh định lý với trợ lý chứng minh Coq.
- 332
- GNU Lesser General Public License v3.0 only
proofs
Kho lưu trữ cá nhân của tôi về toán học đã được xác minh chính thức..
- 259
- GNU General Public License v3.0
verdi-raft
Việc triển khai giao thức đồng thuận phân tán Raft, được xác minh trong Coq bằng khung Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
Thư viện phân tích tuân thủ các thành phần toán học (bởi math-comp).
- 158
- GNU General Public License v3.0
fiat
Chủ yếu là tổng hợp tự động các chương trình đúng theo cách xây dựng.
- 140
- GNU General Public License v3.0
kami
Nền tảng dành cho Thông số kỹ thuật phần cứng tham số cấp cao và Xác minh mô-đun của nó (bởi mit-plv).
- 126
- MIT
toychain
Một sự đồng thuận blockchain tối giản được triển khai và xác minh trong Coq.
- 106
- BSD 2-clause "Simplified"
koika
Một ngôn ngữ cốt lõi cho thiết kế phần cứng dựa trên quy tắc 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Thông số kỹ thuật chính thức và xác minh phần cứng, đặc biệt là về bảo mật và quyền riêng tư..
- 97
- Apache License 2.0
coq-library-undecidability
Một thư viện các bằng chứng về tính không quyết định được cơ giới hóa trong trợ lý bằng chứng Coq..
- 96
- GNU General Public License v3.0
vericert
Một công cụ tổng hợp cấp cao đã được kiểm chứng chính thức dựa trên CompCert và được viết bằng Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Trình cắm trình biên dịch để kiểm soát thời gian tồn tại của đối tượng trong Scala (bởi TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"