formal-verification | Topic | Ecosyste.ms: Repos

Topic: "formal-verification"

p-org/P

The P programming language.

Language: C# - Size: 159 MB - Last synced at: 4 days ago - Pushed at: about 1 month ago - Stars: 3,456 - Forks: 205

hacl-star/hacl-star

HACL*, a formally verified cryptographic library written in F*

Language: F* - Size: 580 MB - Last synced at: 5 days ago - Pushed at: 9 days ago - Stars: 1,791 - Forks: 180

viperproject/prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.

Language: Rust - Size: 1.26 GB - Last synced at: 5 days ago - Pushed at: 7 days ago - Stars: 1,692 - Forks: 117

creusot-rs/creusot

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

Language: Rust - Size: 86.5 MB - Last synced at: about 5 hours ago - Pushed at: about 7 hours ago - Stars: 1,352 - Forks: 60

CakeML/cakeml

CakeML: A Verified Implementation of ML

Language: Standard ML - Size: 129 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 1,089 - Forks: 90

formal-land/coq-of-rust

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

Language: Rocq Prover - Size: 124 MB - Last synced at: about 2 hours ago - Pushed at: about 3 hours ago - Stars: 990 - Forks: 35

magmide/magmide

A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

Language: Coq - Size: 38.5 MB - Last synced at: 22 days ago - Pushed at: over 1 year ago - Stars: 830 - Forks: 14

niltok/magic-in-ten-mins

十分钟魔法练习

Language: HTML - Size: 31.5 MB - Last synced at: 7 months ago - Pushed at: about 2 years ago - Stars: 800 - Forks: 38

sarsko/CreuSAT

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

Language: Rust - Size: 169 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 637 - Forks: 12

ben-marshall/awesome-open-hardware-verification

A List of Free and Open Source Hardware Verification Tools and Frameworks

Size: 166 KB - Last synced at: 13 days ago - Pushed at: about 2 years ago - Stars: 560 - Forks: 55

ligurio/practical-fm

A gently curated list of companies using verification formal methods in industry

Size: 122 KB - Last synced at: 6 months ago - Pushed at: 9 months ago - Stars: 537 - Forks: 42

PrincetonUniversity/VST

Verified Software Toolchain

Language: Rocq Prover - Size: 75.9 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 474 - Forks: 96

AeneasVerif/aeneas

A verification toolchain for Rust programs

Language: OCaml - Size: 10.8 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 428 - Forks: 36

acl2/acl2

ACL2 System and Books as Maintained by the Community

Language: Common Lisp - Size: 1.43 GB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 405 - Forks: 118

mesalock-linux/mesapy

A Fast and Safe Python based on PyPy

Language: Python - Size: 31.5 MB - Last synced at: 7 months ago - Pushed at: about 2 years ago - Stars: 371 - Forks: 27

NASA-SW-VnV/fret

A framework for the elicitation, specification, formalization and analysis of requirements.

Language: JavaScript - Size: 136 MB - Last synced at: 4 months ago - Pushed at: 5 months ago - Stars: 362 - Forks: 58

newca12/awesome-rust-formalized-reasoning

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

Size: 328 KB - Last synced at: about 8 hours ago - Pushed at: 16 days ago - Stars: 359 - Forks: 12

troyguo/awesome-dv

Awesome ASIC design verification

Size: 18.6 KB - Last synced at: 6 days ago - Pushed at: over 3 years ago - Stars: 329 - Forks: 77

cryspen/hax

A Rust verification tool

Language: OCaml - Size: 58.8 MB - Last synced at: about 10 hours ago - Pushed at: about 10 hours ago - Stars: 324 - Forks: 39

stepchowfun/proofs

My personal repository of formally verified mathematics.

Language: Rocq Prover - Size: 1.55 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 305 - Forks: 14

Raiders0786/web3-security-resources

The Web3 Security Resources Hub is a comprehensive collection of curated tools, guides, and best practices for securing decentralized systems and smart contracts in the blockchain space.

Size: 78.1 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 294 - Forks: 49

statebox/idris-ct

formally verified category theory library

Language: Idris - Size: 376 KB - Last synced at: 6 months ago - Pushed at: over 5 years ago - Stars: 263 - Forks: 23

fizzbee-io/fizzbee

Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

Language: Python - Size: 1.26 MB - Last synced at: about 4 hours ago - Pushed at: about 5 hours ago - Stars: 261 - Forks: 18

JuliaReach/LazySets.jl

Scalable symbolic-numeric set computations in Julia

Language: Julia - Size: 42.8 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 252 - Forks: 37

Certora/CertoraProver

The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar

Language: Kotlin - Size: 24.7 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 248 - Forks: 26

hacspec/hacspec 📦

Please see https://github.com/hacspec/hax

Language: Coq - Size: 131 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 244 - Forks: 41

awesomo4000/awesome-provable

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

Size: 25.4 KB - Last synced at: 13 days ago - Pushed at: almost 4 years ago - Stars: 213 - Forks: 10

hwayne/learntla-v2

Learn TLA+ for free! No prior experience necessary!

Language: TLA - Size: 2.14 MB - Last synced at: 8 months ago - Pushed at: 9 months ago - Stars: 209 - Forks: 43

AeneasVerif/charon

Interface with the rustc compiler for the purpose of program verification

Language: Rust - Size: 8.74 MB - Last synced at: about 6 hours ago - Pushed at: about 8 hours ago - Stars: 207 - Forks: 25

JuliaReach/ReachabilityAnalysis.jl

Computing reachable states of dynamical systems in Julia

Language: Julia - Size: 15.2 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 206 - Forks: 17

IBM/ACE-RISCV

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for embedded RISC-V systems with focus on a formally verified and auditable firmware.

Language: Rust - Size: 2.08 MB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 190 - Forks: 19

cryspen/libcrux

The formally verified crypto library for Rust

Language: C - Size: 66.2 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 176 - Forks: 26

CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

Language: Rocq Prover - Size: 32.3 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 155 - Forks: 32

Frama-C/Frama-C-snapshot

Release snapshots of the Frama-C platform for source code analysis

Language: OCaml - Size: 75.1 MB - Last synced at: about 2 years ago - Pushed at: about 5 years ago - Stars: 152 - Forks: 36

tofgarion/spark-by-example

SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada

Language: Ada - Size: 1.03 MB - Last synced at: over 1 year ago - Pushed at: about 3 years ago - Stars: 150 - Forks: 16

leonardoalt/yools

Tools for Yul.

Language: SMT - Size: 445 KB - Last synced at: 5 months ago - Pushed at: over 2 years ago - Stars: 138 - Forks: 6

verivital/nnv

Neural Network Verification Software Tool

Language: MATLAB - Size: 2.97 GB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 131 - Forks: 57

project-oak/silveroak 📦

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

Language: Coq - Size: 36.1 MB - Last synced at: 10 months ago - Pushed at: over 3 years ago - Stars: 123 - Forks: 20

Verified-zkEVM/ArkLib

Formally Verified Arguments of Knowledge in Lean

Language: Lean - Size: 48.4 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 121 - Forks: 25

AdaCore/RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

Language: Ada - Size: 32.6 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 120 - Forks: 8

pq-code-package/mlkem-native

Secure, fast, and portable C90 implementation of ML-KEM / FIPS 203

Language: Assembly - Size: 47.9 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 113 - Forks: 38

fraunhoferfokus/acsl-by-example

Public snapshots of "ACSL by Example"

Language: TeX - Size: 20.8 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 109 - Forks: 21

sec-bit/tokenlibs-with-proofs

Correctness proofs of Ethereum token contracts

Language: Coq - Size: 268 KB - Last synced at: about 1 year ago - Pushed at: over 6 years ago - Stars: 98 - Forks: 23

kupl/VeriSmart-public

a safety verifier for Solidity smart contracts

Language: OCaml - Size: 220 KB - Last synced at: 14 days ago - Pushed at: almost 3 years ago - Stars: 97 - Forks: 25

aman-goel/avr

Reads a state transition system and performs property checking

Language: C++ - Size: 910 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 85 - Forks: 24

scarv/xcrypto

XCrypto: a cryptographic ISE for RISC-V

Language: Verilog - Size: 2.03 MB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 81 - Forks: 10

input-output-hk/high-assurance-legacy 📦

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

Language: Haskell - Size: 4.53 MB - Last synced at: 8 months ago - Pushed at: over 3 years ago - Stars: 78 - Forks: 16

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.

Language: Haskell - Size: 26.8 MB - Last synced at: 5 days ago - Pushed at: over 5 years ago - Stars: 78 - Forks: 7

interchainio/funding

Information about the Interchain Foundation Funding Program

Size: 152 KB - Last synced at: almost 2 years ago - Pushed at: over 3 years ago - Stars: 77 - Forks: 33

NethermindEth/horus-checker

Horus, a formal verification tool for StarkNet smart contracts.

Language: Haskell - Size: 1 MB - Last synced at: 17 days ago - Pushed at: 5 months ago - Stars: 76 - Forks: 9

cristian-mattarei/CoSA

CoreIR Symbolic Analyzer

Language: Python - Size: 7.98 MB - Last synced at: about 2 months ago - Pushed at: about 5 years ago - Stars: 74 - Forks: 18

AthenaFoundation/athena

Athena is a modern, practical language for proof engineering & natural deduction.

Language: Standard ML - Size: 12.7 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 73 - Forks: 4

gipsyh/rIC3

Hardware Formal Verification Tool

Language: Rust - Size: 2.58 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 71 - Forks: 18

data61/PSL

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

SSProve/ssprove

A foundational framework for modular cryptographic proofs in Coq

Language: Rocq Prover - Size: 3.54 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 67 - Forks: 14

workcraft/workcraft

Toolset to capture, simulate, synthesize and verify graph models

Language: Java - Size: 65.9 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 67 - Forks: 142

KeYProject/key

KeY Theorem Prover for Deductive Java Verification

Language: Java - Size: 216 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 66 - Forks: 37

tmeissner/psl_with_ghdl

Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)

Language: VHDL - Size: 92.8 KB - Last synced at: 24 days ago - Pushed at: 9 months ago - Stars: 66 - Forks: 6

ElNiak/awesome-formal-verification

Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.

Size: 52.7 KB - Last synced at: 12 days ago - Pushed at: 14 days ago - Stars: 61 - Forks: 5

symbolicsoft/verifpal

Cryptographic protocol analysis for real-world protocols.

Language: Go - Size: 2.34 MB - Last synced at: 14 days ago - Pushed at: about 1 year ago - Stars: 60 - Forks: 6

awslabs/aws-lc-verification

This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.

Language: Rocq Prover - Size: 639 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 58 - Forks: 22

AllanBlanchard/tutoriel_wp

Frama-C and WP tutorial

Language: TeX - Size: 10.3 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 58 - Forks: 18

IBM/vsrl-framework 📦

The Verifiably Safe Reinforcement Learning Framework

Language: Python - Size: 1.92 MB - Last synced at: 5 months ago - Pushed at: over 4 years ago - Stars: 57 - Forks: 12

SatyendraBanjare/plt-formal-methods-resources

Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.

Size: 3.24 MB - Last synced at: 7 months ago - Pushed at: about 6 years ago - Stars: 55 - Forks: 1

imandra-ai/fix-engine

Imandra FIX Engine

Language: OCaml - Size: 7.88 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 53 - Forks: 3

redtrama/awesome-halmos

List of Halmos resources.

Size: 27.3 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 53 - Forks: 7

lthms/FreeSpec

A framework for implementing and certifying impure computations in Coq

Language: Coq - Size: 958 KB - Last synced at: 6 months ago - Pushed at: almost 2 years ago - Stars: 52 - Forks: 11

SRI-CSL/solidity Fork of ethereum/solidity

This is solc-verify, a modular verifier for Solidity.

Language: C++ - Size: 47.2 MB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 51 - Forks: 14

JuliaReach/Reachability.jl

Reachability and Safety of Nondeterministic Dynamical Systems

Language: Julia - Size: 1.77 MB - Last synced at: 7 months ago - Pushed at: over 4 years ago - Stars: 50 - Forks: 4

verified-optimization/CvxLean

Convex optimization modeling in Lean 4

Language: Lean - Size: 22.5 MB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 49 - Forks: 6

tweag/pirouette 📦

Language-generic workbench for building static analysis

Language: Haskell - Size: 1.54 MB - Last synced at: 6 months ago - Pushed at: about 2 years ago - Stars: 47 - Forks: 2

evdenis/verker 📦

Linux kernel library functions formally verified.

Language: C - Size: 5.37 MB - Last synced at: over 1 year ago - Pushed at: over 4 years ago - Stars: 47 - Forks: 7

lapisla-prover/lapisla-prover

Lapisla is a *battery-pluggable* theorem prover and ecosystem designed for everyone. Greetings! 👋

Language: TypeScript - Size: 9.76 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 46 - Forks: 2

foreverbell/verified

Coq formalizations and proofs of (data) structures and algorithms.

Language: Coq - Size: 135 KB - Last synced at: 7 months ago - Pushed at: over 7 years ago - Stars: 46 - Forks: 3

ElliotSwart/pragmaticformalmodeling

An instructional website with progressively worked examples of TLA+ specifications and model checking.

Language: TLA - Size: 6.79 MB - Last synced at: 11 months ago - Pushed at: over 3 years ago - Stars: 44 - Forks: 2

ben-marshall/croyde-riscv

A barebones 64-bit RISC-V micro-controller class CPU, implementing the I(nteger), M(ul/div), C(ompressed) and K(ryptography) extensions.

Language: SystemVerilog - Size: 754 KB - Last synced at: 8 months ago - Pushed at: almost 4 years ago - Stars: 44 - Forks: 7

tmeissner/formal_hw_verification

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

Language: VHDL - Size: 205 KB - Last synced at: 24 days ago - Pushed at: over 1 year ago - Stars: 42 - Forks: 7

awslabs/AutoCorrode

Verification infrastructure for the Isabelle/HOL interactive proof assistant

Language: Isabelle - Size: 488 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 40 - Forks: 6

will62794/tlaplus_repl

A simple REPL for TLA+.

Language: Python - Size: 21.5 KB - Last synced at: 7 months ago - Pushed at: over 1 year ago - Stars: 40 - Forks: 2

ElNiak/PANTHER

This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.

Language: Python - Size: 1.21 GB - Last synced at: 15 days ago - Pushed at: 15 days ago - Stars: 38 - Forks: 4

reilabs/proven-zk

A support library for working with zero knowledge cryptography in Lean 4.

Language: Lean - Size: 172 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 38 - Forks: 5

haochenpan/rabia

Rabia: Simplifying State-Machine Replication Through Randomization (SOSP 2021)

Language: Go - Size: 58.8 MB - Last synced at: almost 2 years ago - Pushed at: over 2 years ago - Stars: 37 - Forks: 12

Zellic/move-prover-examples

A gentle, example-based guide to getting started with the Move prover.

Language: Move - Size: 55.7 KB - Last synced at: about 1 year ago - Pushed at: about 3 years ago - Stars: 37 - Forks: 5

Ironclad-Project/Ironclad

Mirror of codeberg's repository

Language: Ada - Size: 4.18 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 35 - Forks: 4

bchurchill/pldi19-equivalence-checker Fork of StanfordPL/stoke

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

Language: C++ - Size: 270 MB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 35 - Forks: 9

Ivan-Sergeyev/seymour

This project is about formally verifying Seymour's decomposition theorem for regular matroids.

Language: Lean - Size: 20.2 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 34 - Forks: 12

ftsrg/gamma

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

Language: Xtend - Size: 40.8 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 33 - Forks: 27

formal-land/coq-of-solidity Fork of ethereum/solidity

Formal verification for Solidity smart contracts with Rocq 🐓 Verify arbitrary properties on your smart contracts and make no bugs!

Language: Coq - Size: 101 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 33 - Forks: 2

zenprotocol/zen-wallet

Node and GUI for the Zen Protocol.

Language: C# - Size: 119 MB - Last synced at: over 2 years ago - Pushed at: almost 8 years ago - Stars: 33 - Forks: 13

Ghonimo/Formal-Verification-With-VC-Formal--Tutorials-and-Examples

This repository is dedicated to providing a comprehensive guide and practical examples for using VC Formal for formal verification. Our goal is to help both beginners and experienced users understand the principles of formal verification and how to apply them effectively using VC Formal.

Size: 96.8 MB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 31 - Forks: 2