221 Open source projects that are alternatives of or similar to Iron

Formalisation of the linear lambda calculus in Coq

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

Proof of concept to generate safe and fast JavaScript

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

Formalization of the polymorphic lambda calculus and its parametricity theorem

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

Intermediate Memory Model (IMM) and compilation correctness proofs for it

A framework for formally verifying distributed systems implementations in Coq

The Penn Locally Nameless Metatheory Library

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

implementation of Pure Type Systems (PTS) in Rust.

(λ) Educational lambda calculus interpreter

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)

A blog about Coq

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

A Verified Compiler for Gallina, Written in Gallina

A Certified Interpreter for ML with Structural Polymorphism

Total Parser Combinators in Coq

A statically-typed strictly-evaluated garbage-collected readable programming language.

The Language for Smart Legal Contracts

PeaCoq is a pretty Coq, isn't it?

Fun with λ calculus!

Implementation of Nuprl's type theory in Coq

Homotopy type theory

RISC-V Specification in Coq

Implementation of sprintf for Coq

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

The mathematical study of type theories, in univalent foundations

Mindless, verified (erasably) coding using dependent types

A Hello World program in Coq.

A simple, zero-dependency implementation of the untyped lambda calculus in Safe Rust

Porn browser formally-verified in Coq

🍱 Y Combinator for Non-programmers: A Wild Introduction to Computer Science

A framework for implementing and certifying impure computations in Coq

An implementation of the Formality language in JavaScript

λtext - higher-order file applicator

The CompCert formally-verified C compiler

SoftwareFoundations(Ja)

Coq plugin for parametricity [[email protected]]

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

Bidirectional programming in Haskell with monadic profunctors

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

Tierion Hash API client library for Node.js

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

Verified vector clocks, with Coq!

Collapsing Towers of Interpreters

⛪️ Church Encoding in JS

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

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

A compiler plug-in to control object lifetimes in Scala

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

Verifying concurrent crash-safe systems

Emofishes is a collection of proof of concepts that help improve, bypass or detect virtualized execution environments (focusing on the ones setup for malware analysis).

Formal proof of the Four Color Theorem

The Definitive Guide to Dark Mode and Bootstrap 4 - A proof of concept

Coq executable semantics and resource verifier

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