152 Open source projects that are alternatives of or similar to Foundations

Formalising Type Theory in a modular way for translations between type theories

Coq formalizations of functional languages.

Coq Support for Visual Studio Code

The CompCert formally-verified C compiler

formalization of the Dependent Object Types (DOT) calculus

RISC-V Specification in Coq

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

Porn browser formally-verified in Coq

Verified hash-based AMQ structures in Coq

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

Homotopy type theory

A library of abstract interfaces for mathematical structures in Coq [[email protected]]

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT

SoftwareFoundations(Ja)

Mostly Automated Synthesis of Correct-by-Construction Programs

A compiler plug-in to control object lifetimes in Scala

A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter

The Penn Locally Nameless Metatheory Library

Interactive Coq Proofs in Vim

A Certified Interpreter for ML with Structural Polymorphism

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

Implementation of Nuprl's type theory in Coq

A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]

A SuperCompiler for Martin-Löf's Type Theory

Implementation of sprintf for Coq

A selection of formal proofs in Coq.

Formal proof of the Four Color Theorem

A function definition package for Coq

The mathematical study of type theories, in univalent foundations

A Library for Representing Recursive and Impure Programs in Coq

Randomized Property-Based Testing Plugin for Coq

A Verified Compiler for Gallina, Written in Gallina

A formalization of geometry in Coq based on Tarski's axiom system

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

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

Collapsing Towers of Interpreters

Import OCaml programs to Coq 🐓 🐫

Verifying concurrent crash-safe systems

A Learning Environment for Theorem Proving with the Coq proof assistant

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

A curated set of links to formal methods involving provable code.

A blog about Coq

A Visual Studio Code extension for Coq [[email protected],@fakusb]

A framework for implementing and certifying impure computations in Coq

The Language for Smart Legal Contracts

Total Parser Combinators in Coq

🐣 A blog engine written and proven in Coq

Coq plugin for parametricity [[email protected]]

Mindless, verified (erasably) coding using dependent types

Bidirectional programming in Haskell with monadic profunctors

Advent of Code 2018, in Coq! (https://adventofcode.com/2018)

FSCQ is a certified file system written and proven in Coq

Metaprogramming in Coq

Recipe for FPGA cooking

A library for formalizing Haskell types and functions in Coq

PeaCoq is a pretty Coq, isn't it?