project-oak/silveroak

Formal specification and verification of hardware, especially for security and privacy.

JBakouny/Scallina

A Coq-based synthesis of Scala programs which are correct-by-construction

formal-land/rocq-of-solidity

Formal verification for Solidity smart contracts with the theorem prover Rocq. Providing higher…

jaalonso/Lecturas_GLC

Readings on computational logic, interactive theorem proving and functional programming.

pmer/tla-bin

Command line binaries for the TLA+ language

anton-trunov/coq-lecture-notes

Coq Lecture Notes (WIP)

jasisz/aver

Aver is a programming language for auditable AI-written code

SatyendraBanjare/plt-formal-methods-resources

Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language…