GitHub topics: proof | Ecosyste.ms: Repos

daviddoret/punctilious

A human-friendly and developer-friendly math proof assistant

Language: Python - Size: 55.1 MB - Last synced at: about 4 hours ago - Pushed at: about 5 hours ago - Stars: 2 - Forks: 0

agda/agda-stdlib

The Agda standard library

Language: Agda - Size: 550 MB - Last synced at: about 11 hours ago - Pushed at: about 12 hours ago - Stars: 610 - Forks: 247

eyereasoner/eye-js

A distribution of EYE reasoner in the JavaScript ecosystem using Webassembly.

Language: TypeScript - Size: 477 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 48 - Forks: 5

GuilhermeStracini/POC-react-dotnet-UploadStream

🔬 Proof of Concept of an upload stream from React (JS & Native) app to.NET

Language: JavaScript - Size: 3.58 MB - Last synced at: 2 days ago - Pushed at: 3 days ago - Stars: 1 - Forks: 0

creusot-rs/creusot

Creusot helps you prove your code is correct in an automated fashion.

Language: Rust - Size: 66.1 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1,243 - Forks: 57

xayahrainie4793/minimal-elements-of-the-prime-numbers

The minimal elements of the prime numbers which are > b written in the positional numeral system with radix b, as digit strings under the subsequence ordering, for 2 ≤ b ≤ 36

Language: C++ - Size: 170 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1 - Forks: 0

formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

Language: Coq - Size: 98.5 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 889 - Forks: 31

msoos/cryptominisat

An advanced SAT solver

Language: C++ - Size: 58.5 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 844 - Forks: 193

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 74.5 MB - Last synced at: 13 minutes ago - Pushed at: about 1 hour ago - Stars: 460 - Forks: 93

jirilebl/ra

Basic Analysis, undergraduate real analysis textbook

Language: TeX - Size: 6.64 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 72 - Forks: 25

iiithf/software-foundations

Software Foundations is a broad introduction to the mathematical underpinnings of reliable software.

Language: Coq - Size: 33.6 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 4 - Forks: 0

GoPlausible/.github

Plausible is a proof of anything protocol for Algorand

Size: 17.3 MB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 2 - Forks: 2

davidfstr/idris-insertion-sort

Provably correct implementation of insertion sort in Idris.

Language: Idris - Size: 5.86 KB - Last synced at: 3 days ago - Pushed at: almost 4 years ago - Stars: 31 - Forks: 4

ozekik/mathesis

Python library for computational formal logic, formal semantics, and theorem proving

Language: Python - Size: 1.18 MB - Last synced at: 3 days ago - Pushed at: about 2 months ago - Stars: 21 - Forks: 3

uwplse/verdi-raft

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

Language: Coq - Size: 2.96 MB - Last synced at: 12 days ago - Pushed at: over 1 year ago - Stars: 186 - Forks: 19

seL4/l4v

seL4 specification and proofs

Language: Isabelle - Size: 93.9 MB - Last synced at: 4 days ago - Pushed at: 5 days ago - Stars: 537 - Forks: 109

seL4/website

The seL4.systems website

Language: HTML - Size: 347 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 3 - Forks: 13

w3c/vc-di-bbs

A linked data proof suite specification for BBS+ signatures

Language: HTML - Size: 733 KB - Last synced at: 12 days ago - Pushed at: 18 days ago - Stars: 49 - Forks: 19

This Discord Nitro Proof generator allows you to generate an image (.png) simulating the donation of a nitro to a user. It is possible to choose by entering the ID a real user or to choose manually the name, the profile picture and the message of the user. The use of the script is done with the help of commands using Discord modals.

Language: Python - Size: 388 KB - Last synced at: 15 days ago - Pushed at: 26 days ago - Stars: 77 - Forks: 45

Merlin04/truthtabl.es

Truth table generator, (basic) proof builder, and more, built with Next.js and Ohm

Language: TypeScript - Size: 252 KB - Last synced at: about 6 hours ago - Pushed at: over 1 year ago - Stars: 23 - Forks: 3

seL4/graph-refine

Language: Python - Size: 1.09 MB - Last synced at: 17 days ago - Pushed at: about 1 month ago - Stars: 14 - Forks: 12

scoredetect/timestamps

Timestamp your WordPress content into the blockchain to empower your content authenticity and increase user trust.

Language: PHP - Size: 1.73 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 2 - Forks: 0

francoisschwarzentruber/prooffold

Another attempt for visualizing proofs

Language: JavaScript - Size: 1.4 MB - Last synced at: 6 days ago - Pushed at: 5 months ago - Stars: 12 - Forks: 4

uwplse/verdi

A framework for formally verifying distributed systems implementations in Coq

Language: Coq - Size: 2.55 MB - Last synced at: 18 days ago - Pushed at: 11 months ago - Stars: 601 - Forks: 56

aaditya29/Formal-Method-Proofs-by-Coq

Proofs in Coq

Language: Coq - Size: 45.9 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

GuilhermeStracini/POC-dotnet-Dijkstra

🔬 Proof of Concept of Dijkstra's algorithm in .NET

Language: C# - Size: 493 KB - Last synced at: 19 days ago - Pushed at: about 1 month ago - Stars: 3 - Forks: 0

GrahamStrickland/math_lean

Examples and exercises from "Mathematics in Lean" - Jeremy Avigad & Patrick Massot

Language: Lean - Size: 16.6 KB - Last synced at: 13 days ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

DistributedComponents/InfSeqExt

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

Language: Coq - Size: 88.9 KB - Last synced at: 19 days ago - Pushed at: over 2 years ago - Stars: 17 - Forks: 4

DistributedComponents/disel

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

Language: Coq - Size: 1.24 MB - Last synced at: 17 days ago - Pushed at: 9 months ago - Stars: 98 - Forks: 7

OpenRarity/open-rarity

Reference implementation of the OpenRarity protocol with Python.

Language: Python - Size: 9.9 MB - Last synced at: 15 days ago - Pushed at: over 1 year ago - Stars: 222 - Forks: 49

Deducteam/nubo

Nubo is a repository of interoperable formal proofs written in Dedukti.

Language: Makefile - Size: 124 KB - Last synced at: 29 days ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 0

gallais/generic-syntax

A Scope-and-Type Safe Universe of Syntaxes with Binding, Their Semantics and Proofs

Language: Agda - Size: 10.6 MB - Last synced at: 26 days ago - Pushed at: about 3 years ago - Stars: 72 - Forks: 11

discus-lang/iron

Coq formalizations of functional languages.

Language: Coq - Size: 800 KB - Last synced at: 15 days ago - Pushed at: almost 5 years ago - Stars: 143 - Forks: 8

eddieoz/haal

Hääl - Anonymous Electronic Voting System on Public Blockchains

Language: JavaScript - Size: 1.42 MB - Last synced at: 7 days ago - Pushed at: over 2 years ago - Stars: 113 - Forks: 17

chakravala/Math-Research-Notes

Theorems, Definitions, Papers, Research

Language: TeX - Size: 1.38 MB - Last synced at: 13 days ago - Pushed at: almost 6 years ago - Stars: 17 - Forks: 4

silvinor/bootstrap-dark 📦

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

Language: HTML - Size: 3.21 MB - Last synced at: 15 days ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

DistributedComponents/verdi-lockserv

An implementation of a simple asynchronous message-passing lock server, verified in Coq using the Verdi framework

Language: Coq - Size: 58.6 KB - Last synced at: 19 days ago - Pushed at: over 7 years ago - Stars: 14 - Forks: 5

gapt/gapt

GAPT: General Architecture for Proof Theory

Language: Scala - Size: 182 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 98 - Forks: 18

ivomac/UniquenessSpinHamiltonian

Proof of 1-to-1 correspondence between classical spin Hamiltonian spectrum and model weights

Language: TeX - Size: 1.95 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

Splines/lean-continuous

Continuous functions formalized in Lean4. A students project accompanied by a YouTube video.

Language: TeX - Size: 5.44 MB - Last synced at: about 1 month ago - Pushed at: 9 months ago - Stars: 12 - Forks: 1

andrew222651/semkon

LLM-based proof checker for codebases

Language: Python - Size: 73.2 KB - Last synced at: 9 days ago - Pushed at: 3 months ago - Stars: 3 - Forks: 0

kth-step/HolBA

Binary analysis in HOL

Language: Standard ML - Size: 8.28 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 35 - Forks: 21

FL45h-09/SocialHack

In this repository you can find stuff related to hack Facebook & Instagram. Disclaimer: This is only the proof of concept of my piece of code and only for educational purpose. So we are not responsible for any illegal use of this code.

Language: PHP - Size: 147 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 136 - Forks: 22

permutationlock/path_coloring_bgl

Implementations of several path coloring algorithms for the Boost Graph Library.

Language: C++ - Size: 8.62 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

xiaoshihou514/ndpc

Natural deduction proof compiler

Language: Scala - Size: 227 KB - Last synced at: about 13 hours ago - Pushed at: 2 months ago - Stars: 7 - Forks: 0

RaphaelBonatti/propositional-logic-prover-python

A propositional logic prover implemented using resolution refutation.

Language: Python - Size: 43 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

janaSunrise/blockchain-python

This is a implementation of a basic blockchain structure in python, with all the description, and documentation of it's working and things.

Language: HTML - Size: 66.4 KB - Last synced at: 7 days ago - Pushed at: over 3 years ago - Stars: 15 - Forks: 9

appliedfm/vstyle

A style guide for Coq

Size: 646 KB - Last synced at: 15 days ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 0

Isaac-DeFrain/dependent

An implementation of dependently typed lambda calculus

Language: OCaml - Size: 43 KB - Last synced at: 20 days ago - Pushed at: almost 3 years ago - Stars: 5 - Forks: 0

d-plaindoux/tyasta

A journey with F*

Language: F* - Size: 53.7 KB - Last synced at: 20 days ago - Pushed at: almost 2 years ago - Stars: 8 - Forks: 0

paragonie/chronicle

Public append-only ledger microservice built with Slim Framework

Language: PHP - Size: 301 KB - Last synced at: 17 days ago - Pushed at: over 3 years ago - Stars: 469 - Forks: 25

shauryashaurya/elegant

Proof checker from scratch in Python and coq / rocq

Language: Jupyter Notebook - Size: 38.5 MB - Last synced at: 3 days ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

weakmemory/imm

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

Language: Coq - Size: 1.52 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 23 - Forks: 3

binary-translation/lasagne-proofs

Architecture mapping proofs written in Agda for the paper "Lasagne: A Static Binary Translator for Weak Memory Model Architectures"

Language: Agda - Size: 163 KB - Last synced at: 2 days ago - Pushed at: about 3 years ago - Stars: 12 - Forks: 2

GuilhermeStracini/POC-react-dotnet-SplitUpload

🔬 Proof of Concept of an upload split in .NET and React JS

Language: JavaScript - Size: 414 KB - Last synced at: 19 days ago - Pushed at: 23 days ago - Stars: 2 - Forks: 0

COSC3020/log-o

Size: 1000 Bytes - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

metamath/lamp-guide

Guide on how to use the metamath-lamp proof assistant

Language: HTML - Size: 22.2 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 3 - Forks: 1

TimothyEarley/incompleteness

Gödels Incompleteness Theorem Proven in Arend

Size: 79.1 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

beyarkay/provenance-rs

A history-of-ownership protocol to stop misinformation

Language: Rust - Size: 2.94 MB - Last synced at: 17 days ago - Pushed at: 4 months ago - Stars: 3 - Forks: 0

xiaoshihou514/aristotle

Easy to use gui frontend for ndpc

Language: C++ - Size: 162 KB - Last synced at: about 13 hours ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

xiaoshihou514/ndp.vim

Vim support for the natural deduction markup language

Language: Vim Script - Size: 18.6 KB - Last synced at: about 13 hours ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

ttwag/MAT115A-Number_Theory

Number Theory

Language: TeX - Size: 744 KB - Last synced at: about 2 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

ttwag/p13_lean4_natural_number_game_solution

Contains the solution to the natural number game in lean 4

Language: Lean - Size: 12.7 KB - Last synced at: 2 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

denismurphy/simplified-blockchain 📦

Simplified Blockchain: A Playful Approach

Language: Rust - Size: 23.4 KB - Last synced at: 3 days ago - Pushed at: 8 months ago - Stars: 3 - Forks: 0

Monislav/Discord-Fake-Nitro-Proof-Generator

This Fake Proof generator allows you to generate an image (.png) simulating the donation of a nitro to a user. It is possible to choose by entering the ID a real user or to choose manually the name, the profile picture and the message of the user. The use of the script is done with the help of commands using Discord modals.

Language: Python - Size: 0 Bytes - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

smorimoto/coq-to-ocaml-to-js

Proof of concept to generate safe and fast JavaScript

Language: JavaScript - Size: 402 KB - Last synced at: 22 days ago - Pushed at: over 2 years ago - Stars: 24 - Forks: 2

deivid69e/Discord-Fake-Nitro-Proof-Generator

This Fake Proof generator allows you to generate an image (.png) simulating the donation of a nitro to a user. It is possible to choose by entering the ID a real user or to choose manually the name, the profile picture and the message of the user. The use of the script is done with the help of commands using Discord modals.

Language: Python - Size: 5.86 KB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

Deducteam/hol2dk

HOL-Light to Dedukti/Lambdapi translator

Language: OCaml - Size: 560 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 6 - Forks: 3

RyanMarcus/vulcan

A JavaScript propositional logic and resolution library

Language: JavaScript - Size: 47.9 KB - Last synced at: 19 days ago - Pushed at: over 7 years ago - Stars: 61 - Forks: 8

ethereumjs/merkle-patricia-tree 📦

Project is in active development and has been moved to the EthereumJS VM monorepo.

Language: TypeScript - Size: 1.27 MB - Last synced at: 27 days ago - Pushed at: over 4 years ago - Stars: 307 - Forks: 89

GasStationManager/CodeProofTheArena

Lean coding problem solving challenge website with proof verification

Language: Python - Size: 88.9 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 6 - Forks: 0

spamegg1/spamegg1-thm-prov-lean4

Working through Theorem Proving in Lean4

Language: Lean - Size: 111 KB - Last synced at: about 1 month ago - Pushed at: 5 months ago - Stars: 1 - Forks: 0

nclarius/pyPL

Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions

Language: Python - Size: 6.22 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 19 - Forks: 2

barton-willis/Foundations-of-Mathematics

Here you will find some course materials for my Spring 2023 course MATH 250 (Foundations of Mathematics)

Language: TeX - Size: 2.23 MB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 1 - Forks: 0

lemmy/lets-prove-blocking-queue

Proving a blocking queue deadlock free in a dozen different ways

Language: Dafny - Size: 123 KB - Last synced at: 26 days ago - Pushed at: 6 months ago - Stars: 43 - Forks: 5

lukaszcz/sortalgs

Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.

Language: Coq - Size: 23.4 KB - Last synced at: about 2 months ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0

baro77/ZKbasicsCS

Zero-Knowledge Proofs "for (not too much :wink: ) dummies"

Size: 854 KB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 119 - Forks: 7

miklosn/node-pow-argon2

An Argon2-based proof of work library for Node

Language: JavaScript - Size: 479 KB - Last synced at: 4 months ago - Pushed at: about 5 years ago - Stars: 1 - Forks: 2

data61/PSL

Language: Isabelle - Size: 175 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 65 - Forks: 9

sourceduty/Prediction_Proof

🔮 Prove or disprove and make future predictions.

Size: 5.86 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

SouthbankSoftware/proofable

General purpose proving framework for certifying digital assets to public blockchains

Language: Go - Size: 101 MB - Last synced at: 3 days ago - Pushed at: about 2 years ago - Stars: 10 - Forks: 4

NuID/examples

Examples of NuID's zero knowledge authentication and key management facilities in various languages and frameworks. Open an Issue or PR if you'd like to see your favorite tool here.

Language: JavaScript - Size: 1.86 MB - Last synced at: 14 days ago - Pushed at: over 2 years ago - Stars: 43 - Forks: 3

binsarjr/sql-bypass-waf

SQL Bypass WAF merupakan tools yang membantu membypass WAF pada sql dengan menggunakan payload yg sudah ditentukan

Language: PHP - Size: 42 KB - Last synced at: 8 days ago - Pushed at: over 4 years ago - Stars: 8 - Forks: 8

ekmett/linear-logic

They see me rollin'. They're Heyting. -- Chamillionaire, 2005

Language: Haskell - Size: 331 KB - Last synced at: 8 days ago - Pushed at: about 4 years ago - Stars: 83 - Forks: 2

MRandl/verith

A small coq library for verifying OCaml native integer computations

Language: Coq - Size: 39.1 KB - Last synced at: about 2 months ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0

AtticusKuhn/proofs-from-the-book

Proofs from THE BOOK by Aigner and Ziegler proved in the Lean proving assistant

Language: Lean - Size: 181 KB - Last synced at: 10 days ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0

CE-Storage/CE115-DS

Discrete Structures course at Sharif University of Technology

Size: 38.4 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

ShanksPranks/catship_production

The CatShip & CatShipCoin Live Production Repo

Language: PHP - Size: 9.71 MB - Last synced at: 2 months ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 0

chainpoint/chainpoint-cli

A Command Line Interface (CLI) for creating and verifying Chainpoint proofs.

Language: JavaScript - Size: 705 KB - Last synced at: 17 days ago - Pushed at: almost 5 years ago - Stars: 58 - Forks: 11

Jumaruba/LPL-solutions

Solutions for the book "Language Proof and Logic".

Size: 10.3 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 67 - Forks: 155

LS-Lab/KeYmaeraX-projects

Projects, models, and proofs in KeYmaera X

Language: Shell - Size: 1000 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 5 - Forks: 8

InCogNiTo124/recursive-sgd 📦

A proof of concept of a recursion doing stochastic gradient descent for a simple neural network. Done in Python3 with numpy

Language: Python - Size: 192 KB - Last synced at: 3 days ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0