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

Implementation of sprintf for Coq

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

Collapsing Towers of Interpreters

Coq plugin for parametricity [[email protected]]

A Verified Compiler for Gallina, Written in Gallina

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

CoqPIE (an IDE for the Coq theorem prover + PEDANTIC)

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

Total Parser Combinators in Coq

KCoFI Pudding: The formal proofs for the KCoFI system

Bidirectional programming in Haskell with monadic profunctors

A Hello World program in Coq.

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

Coq executable semantics and resource verifier

The Language for Smart Legal Contracts

Combinatorial species in HoTT

Verifying concurrent crash-safe systems

Automation for de Bruijn syntax and substitution in Coq

Formal proof of the Four Color Theorem

Certified Relational to Imperative

A blog about Coq

A Certified Interpreter for ML with Structural Polymorphism

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

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

The CompCert formally-verified C compiler

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

Implementation of Nuprl's type theory in Coq

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

Homotopy type theory

Interactive Coq Proofs in Vim

Verified vector clocks, with Coq!

SoftwareFoundations(Ja)

sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility

PeaCoq is a pretty Coq, isn't it?

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

RISC-V Specification in Coq

Formalisation of the linear lambda calculus in Coq

Coq formalizations of functional languages.

Coq code accompanying several articles on semantics of functional programming languages

A compiler plug-in to control object lifetimes in Scala

An introductory tutorial for the Coq proof assistant.

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

Formalization of C++ for verification purposes.

Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors

Verified hash-based AMQ structures in Coq

A Coq library for extensional finite sets and comprehension

The Penn Locally Nameless Metatheory Library

Coq proofs of exercises in Pierce's book

Coq Support for Visual Studio Code

Porn browser formally-verified in Coq

Import OCaml programs to Coq 🐓 🐫

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

Mindless, verified (erasably) coding using dependent types

The mathematical study of type theories, in univalent foundations

A framework for implementing and certifying impure computations in Coq