176 Open source projects that are alternatives of or similar to coq-tal

Mostly Automated Synthesis of Correct-by-Construction Programs

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

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

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

FSCQ is a certified file system written and proven in Coq

Interactive Coq Proofs in Vim

A Domain Representation Language

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

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

A library for formalizing Haskell types and functions in Coq

SoftwareFoundations(Ja)

The Vellvm (Verified LLVM) coq development.

formalization of the Dependent Object Types (DOT) calculus

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

Coq formalizations of functional languages.

Metaprogramming in Coq

Verified hash-based AMQ structures in Coq

No description or website provided.

PeaCoq is a pretty Coq, isn't it?

Recipe for FPGA cooking

Coq Support for Visual Studio Code

A mechanisation of Wasm in Coq

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

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

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

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

Fωμ type checker and compiler

A selection of formal proofs in Coq.

Coq plugin embedding elpi

A Library for Representing Recursive and Impure Programs in Coq

Voevodsky's original development of the univalent foundations of mathematics in Coq

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

Stable sort algorithms and their stability proofs in Coq

Import OCaml programs to Coq 🐓 🐫

A Learning Environment for Theorem Proving with the Coq proof assistant

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

Proof of concept to generate safe and fast JavaScript

The Language for Smart Legal Contracts

Randomized Property-Based Testing Plugin for Coq

Mindless, verified (erasably) coding using dependent types

A core language for rule-based hardware design 🦑

🐣 A blog engine written and proven in Coq

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

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

Formal proof of the Four Color Theorem

A function definition package for Coq

The mathematical study of type theories, in univalent foundations

Reference sheet for the Coq language.

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

A Verified Compiler for Gallina, Written in Gallina

Goose converts a small subset of Go to Coq

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

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

Coq to OCaml FFI made easy [maintainer=@lthms]

A minimalistic blockchain consensus implemented and verified in Coq

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe]

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