A Coq library for Homotopy Type Theory

A work-in-progress language and compiler for verified low-level programming

Convert Haskell source code to Coq source code

A Verified Compiler for Gallina, Written in Gallina

A framework for smart contract verification in Coq

A library for effects in Coq.

Gallina to Bedrock2 compilation toolkit

Formal verification for Solidity smart contracts with the theorem prover Rocq. Ensure no vulnerabilities for your smart contracts.

IO for Gallina

Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.

A Vyper compiler in Coq (just started)

<Logical Foundations> personal study record.

Proving non-trivial identities of the Fibonacci sequence with Coq Proof Assistant