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

Formalization of the basic actuarial mathematics using Coq

A minimalistic blockchain consensus implemented and verified in Coq

Gallina to Bedrock2 compilation toolkit

Archive for all Coq related OPAM packages organized in various repositories

The Vellvm (Verified LLVM) coq development.

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.

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

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

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

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

Formalization of the polymorphic lambda calculus and its parametricity theorem

Metaprogramming in Coq

Jupyter kernel for Coq

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

Ltac2 tutorial

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

Mutation analysis tool for Coq verification projects

No description or website provided.

A proof of Abel-Ruffini theorem.

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

Partial Commutative Monoids

Goose converts a small subset of Go to Coq

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

FSCQ is a certified file system written and proven in Coq

Template project for program verification in Coq

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

Randomized Property-Based Testing Plugin for Coq

A framework for implementing and certifying impure computations in Coq

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

Finite sets, finite maps, multisets and generic sets

Convert Haskell source code to Coq source code.

No description or website provided.

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

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

Formalization of Typed Assembly Language (TAL) in Coq

The formal proof of the Odd Order Theorem

A core language for rule-based hardware design 🦑

Mtac in Agda

Stable sort algorithms and their stability proofs in Coq

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

Reference sheet for the Coq language.

IO for Gallina

Coq plugin embedding elpi

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

Proof of concept to generate safe and fast JavaScript

Multinomials for the Mathematical Components library.

A mechanisation of Wasm in Coq

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

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

Formal verification of OCaml programs

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

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

A Learning Environment for Theorem Proving with the Coq proof assistant

A Coq library providing tactics to deal with hypothesis

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

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Coq encoding of ZFC and formalization of the textbook Elements of Set Theory

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

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