169 Open source projects that are alternatives of or similar to FreeSpec

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.

Algebraic proof discovery in Agda

Formalization of the polymorphic lambda calculus and its parametricity theorem

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

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

Template project for program verification in Coq

A minimalistic blockchain consensus implemented and verified in Coq

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

The Vellvm (Verified LLVM) coq development.

Source code for the equivalence checker presented in the PLDI 2019 paper, "Semantic Program Alignment for Equivalence Checking"

Metaprogramming in Coq

Formalization of Typed Assembly Language (TAL) in Coq

A library of mechanised undecidability proofs in the Coq proof assistant.

A core language for rule-based hardware design 🦑

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

No description or website provided.

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

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

TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus

Goose converts a small subset of Go to Coq

Archive for all Coq related OPAM packages organized in various repositories

FSCQ is a certified file system written and proven in Coq

Legacy code connected to the high-assurance implementation of the Ouroboros protocol family

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

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

Recipe for FPGA cooking

Formalization of the basic actuarial mathematics using Coq

www.imandra.ai

Formalization of Tendermint proposer election properties

Trying to verify Verilog/VHDL designs with formal methods and tools

Read-only mirror of the Klever Git repository

An Eclipse-based modeling framework for the component-based design and analysis of reactive systems

The formal proof of the Odd Order Theorem

Stable sort algorithms and their stability proofs in Coq

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

Reference sheet for the Coq language.

Gallina to Bedrock2 compilation toolkit

Coq plugin embedding elpi

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

Proof of concept to generate safe and fast JavaScript

No description or website provided.

A mechanisation of Wasm in Coq

Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker

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

Partial Commutative Monoids

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

Convert Haskell source code to Coq source code.

A Learning Environment for Theorem Proving with the Coq proof assistant

Mutation analysis tool for Coq verification projects

Randomized Property-Based Testing Plugin for Coq

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

🐣 A blog engine written and proven in Coq

A formally verified high-level synthesis tool based on CompCert and written in Coq.

Jupyter kernel for Coq

Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]

A function definition package for Coq

Reads a state transition system and performs property checking

A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.

Fully proved small C functions (examples for verification course).