163 Open source projects that are alternatives of or similar to coqffi

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

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

A function definition package for Coq

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

A Verified Compiler for Gallina, Written in Gallina

Randomized Property-Based Testing Plugin for Coq

Mindless, verified (erasably) coding using dependent types

A mechanisation of Wasm in Coq

The mathematical study of type theories, in univalent foundations

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

A Library for Representing Recursive and Impure Programs in Coq

Collapsing Towers of Interpreters

A Learning Environment for Theorem Proving with the Coq proof assistant

Import OCaml programs to Coq 🐓 🐫

Haskell FFI bindings to CUDA

The Language for Smart Legal Contracts

🐣 A blog engine written and proven in Coq

FFI examples written in Rust

Formal proof of the Four Color Theorem

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

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

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

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

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

A compiler plug-in to control object lifetimes in Scala

FSCQ is a certified file system written and proven in Coq

formalization of the Dependent Object Types (DOT) calculus

Proof of concept to generate safe and fast JavaScript

Mostly Automated Synthesis of Correct-by-Construction Programs

Metaprogramming in Coq

Coq formalizations of functional languages.

A minimalistic blockchain consensus implemented and verified in Coq

Interactive Coq Proofs in Vim

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

Verified hash-based AMQ structures in Coq

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

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

Recipe for FPGA cooking

PeaCoq is a pretty Coq, isn't it?

No description or website provided.

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

Coq Support for Visual Studio Code

Goose converts a small subset of Go to Coq

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

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

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

Coq plugin embedding elpi

SoftwareFoundations(Ja)

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

RISC-V Specification in Coq

The Vellvm (Verified LLVM) coq development.

A library for formalizing Haskell types and functions in Coq

Stable sort algorithms and their stability proofs in Coq

Reference sheet for the Coq language.

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

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

A selection of formal proofs in Coq.