project-oak/silveroak

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

foreverbell/verified

Coq formalizations and proofs of (data) structures and algorithms.

dafny-lang/dafny

Dafny is a verification-aware programming language

dunhamsteve/newt

A toy dependent typed language.

fluid-org/fluid

A Pythonic functional programming language with provenance-tracking

formal-land/rocq-of-solidity

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

JBakouny/Scallina

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

pmer/tla-bin

Command line binaries for the TLA+ language