coq

Der Rocq Prover ist ein interaktiver Theorembeweiser bzw. Beweisassistent. Er bietet eine formale Sprache zum Schreiben mathematischer Definitionen, ausführbarer Algorithmen und Theoreme sowie eine Umgebung für die semi-interaktive Entwicklung maschinell überprüfter Beweise.

Der formal verifizierte C-Compiler CompCert

Diese Rocq-Bibliothek zielt darauf ab, einen wesentlichen Teil der Mathematik unter Verwendung der univalenten Sichtweise zu formalisieren.

„Software-Grundlagen“ (Chinesische Ausgabe)

Eine Verifizierungstoolchain für Rust-Programme

Eine abhängig typisierte Beweissprache, die es Softwareentwicklern ermöglichen soll, nachweislich korrekten Bare-Metal-Code zu schreiben.

Eine axiomfreie Formalisierung der Kategorietheorie in Coq für das persönliche Studium und die praktische Arbeit.

Mathematische Komponenten

Cosette ist ein automatisierter SQL-Solver.

Ein Framework zur formalen Verifikation von Implementierungen verteilter Systeme in Coq

Eine sorgfältig zusammengestellte Liste von Unternehmen, die formale Verifikationsmethoden in der Industrie einsetzen

Dieses Repository ist das neue Zuhause von Proof General

Tricks, die man sich im Coq-Handbuch gewünscht hätte [maintainer=@tchajed]

Metaprogrammierung, verifizierte Metatheorie und Implementierung von Rocq in Rocq.

Ein Port von Coq nach Javascript – Führen Sie Coq in Ihrem Browser aus

Verified Software Toolchain