Topic: formal-verification Goto Github

👇 Here are 471 public repositories matching this topic...

acl2 / acl2
formal-verification,ACL2 System and Books as Maintained by the Community
Organization: acl2
Home Page: http://www.cs.utexas.edu/users/moore/acl2
acl2 theorem-prover theorem-proving common-lisp rewriting formal-verification formal-methods first-order-logic logic

adacore / recordflux
formal-verification,Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Organization: adacore
parser binary-parser ada spark formal-verification formal-specification formal-methods communication-protocol protocol-parser protocol-specification

aeneasverif / aeneas
formal-verification,A verification toolchain for Rust programs
Organization: aeneasverif
compiler coq deductive-reasoning formal-methods formal-verification fstar hol4 lean ocaml proofs

aeneasverif / charon
formal-verification,Interface with the rustc compiler for the purpose of program verification
Organization: aeneasverif
compiler formal-methods formal-verification program-verification rust rust-lang static-analysis

aman-goel / avr
formal-verification,Reads a state transition system and performs property checking
User: aman-goel
model-checking formal-verification verilog ic3 pdr

athenafoundation / athena
formal-verification,Athena is a modern, practical language for proof engineering & natural deduction.
Organization: athenafoundation
formal-verification logic proof-assistant theorem-proving natural-deduction functional-programming proof-language

awesomo4000 / awesome-provable
formal-verification,A curated set of links to formal methods involving provable code.
User: awesomo4000
formal-verification certified-programming sel4 coq isabelle isabelle-hol idris agda

ben-marshall / awesome-open-hardware-verification
formal-verification,A List of Free and Open Source Hardware Verification Tools and Frameworks
User: ben-marshall
hardware verification vhdl verilog formal-verification constrained-random-verification python awesome awesome-list coverage

cakeml / cakeml
formal-verification,CakeML: A Verified Implementation of ML
Organization: cakeml
Home Page: https://cakeml.org
programming-language formal-verification formal-semantics compiler theorem-proving hol sml

certicoq / certicoq
formal-verification,A Verified Compiler for Gallina, Written in Gallina
Organization: certicoq
compiler coq formal-verification gallina

creusot-rs / creusot
formal-verification,Creusot helps you prove your code is correct in an automated fashion.
Organization: creusot-rs
rust-lang verification proof formal-verification deductive-reasoning why3 rust formal-methods

cristian-mattarei / cosa
formal-verification,CoreIR Symbolic Analyzer
User: cristian-mattarei
satisfiability-modulo-theories formal-verification formal-methods model-checking hardware-verification verilog systemverilog

data61 / psl
formal-verification,
Organization: data61
proof psl isabelle proof-strategies conjecture hol machine-learning artificial-intelligence itp interactive-theorem-proving

fizzbee-io / fizzbee
formal-verification,Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
Organization: fizzbee-io
Home Page: https://fizzbee.io
formal-languages formal-methods formal-verification ltl tla tla-plus tlaplus alloy alloy-analyzer pluscal

formal-land / coq-of-rust
formal-verification,Check 100% of execution cases of Rust programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦 Formal verification
Organization: formal-land
coq formal-verification rust proof

frama-c / frama-c-snapshot
formal-verification,Release snapshots of the Frama-C platform for source code analysis
Organization: frama-c
Home Page: http://frama-c.com
c static-analysis runtime-verification ocaml formal-verification abstract-interpretation

fraunhoferfokus / acsl-by-example
formal-verification,Public snapshots of "ACSL by Example"
Organization: fraunhoferfokus
frama-c acsl wp-plugin formal-methods formal-specification formal-verification c

hacl-star / hacl-star
formal-verification,HACL*, a formally verified cryptographic library written in F*
Organization: hacl-star
cryptography verified-primitives high-performance security formal-methods formal-verification inria hacl everest verification

hacspec / hacspec
formal-verification,Please see https://github.com/hacspec/hax
Organization: hacspec
Home Page: https://hacspec.org
cryptography formal-verification specifications

hacspec / hax
formal-verification,A Rust verification tool
Organization: hacspec
Home Page: https://hacspec.org/blog
formal-verification rust

hwayne / learntla-v2
formal-verification,Learn TLA+ for free! No prior experience necessary!
User: hwayne
Home Page: https://www.learntla.com
book formal-methods formal-specification formal-verification tla tlaplus

ibm / vsrl-framework
formal-verification,The Verifiably Safe Reinforcement Learning Framework
Organization: ibm
reinforcement-learning safety-critical formal-verification formal-methods reinforcement-learning-algorithms reinforcement-learning-environments cyber-physical-systems keymaerax keymaera differential-dynamic-logic

input-output-hk / high-assurance-legacy
formal-verification,Legacy code connected to the high-assurance implementation of the Ouroboros protocol family
Organization: input-output-hk
ouroboros cardano cryptocurrency blockchain distributed-computing formal-verification formal-methods

interchainio / funding
formal-verification,Information about the Interchain Foundation Funding Program
Organization: interchainio
Home Page: https://interchain.io/funding
blockchain cosmos cryptography decentralized formal-verification funding grant open-source permaculture research tendermint

jdnklau / fm-ml
formal-verification,Collection of resources for research concerning Machine Learning and Formal Methods.
User: jdnklau
machine-learning formal-methods formal-verification

juliareach / lazysets.jl
formal-verification,Scalable symbolic-numeric set computations in Julia
Organization: juliareach
Home Page: https://juliareach.github.io/LazySets.jl/
julia convex-sets formal-verification reachability-analysis lazy-evaluation polyhedra convex-hull calculus sets geometry

juliareach / reachabilityanalysis.jl
formal-verification,Computing reachable states of dynamical systems in Julia
Organization: juliareach
Home Page: https://juliareach.github.io/ReachabilityAnalysis.jl/
numerical-analysis hybrid-systems formal-verification cyber-physical-systems reachability-analysis rigorous-numerics differential-equations interval-arithmetic dynamical-systems control-systems

kupl / verismart-public
formal-verification,a safety verifier for Solidity smart contracts
Organization: kupl
smart-contracts solidity solidity-contracts formal-verification blockchain ethereum program-analysis

leonardoalt / yools
formal-verification,Tools for Yul.
User: leonardoalt
evm yul ethereum formal-verification solidity hacktoberfest

ligurio / practical-fm
formal-verification,A gently curated list of companies using verification formal methods in industry
User: ligurio
formal-verification formal-methods tlaplus tla-specification coq software-engineering formal-verification-methods practice

magmide / magmide
formal-verification,A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Organization: magmide
formal-verification formal-methods type-safety systems-programming dependent-types verification logic coq

mesalock-linux / mesapy
formal-verification,A Fast and Safe Python based on PyPy
Organization: mesalock-linux
python memory-safety formal-verification sgx rust pypy

nethermindeth / horus-checker
formal-verification,Horus, a formal verification tool for StarkNet smart contracts.
Organization: nethermindeth
Home Page: https://nethermind.io/horus/
cairo formal-verification starknet

newca12 / awesome-rust-formalized-reasoning
formal-verification,An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
User: newca12
formal-verification prover automated-theorem-provers theorem-prover reasoning logic constructive-mathematics dependent-types theorem-proving proof-assistants

niltok / magic-in-ten-mins
formal-verification,十分钟魔法练习
User: niltok
Home Page: https://magic.huohuo.moe
adt formal-proofs formal-verification functional-programming hkt java lambda-calculus monad tutorial

p-org / p
formal-verification,The P programming language.
Organization: p-org
Home Page: https://p-org.github.io/P/
asynchronous programming-language systematic-testing event-driven robotics p distributed-systems state-machine model-checking formal-methods

princetonuniversity / vst
formal-verification,Verified Software Toolchain
Organization: princetonuniversity
Home Page: https://vst.cs.princeton.edu
coq coq-vst compcert c coq-library verification proof proof-assistant formal-methods formal-verification

project-oak / silveroak
formal-verification,Formal specification and verification of hardware, especially for security and privacy.
Organization: project-oak
coq formal-verification hardware

sarsko / creusat
formal-verification,CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
User: sarsko
sat verification rust automated-reasoning deductive-reasoning formal-methods formal-verification minisat sat-solver satisfiability

scarv / xcrypto
formal-verification,XCrypto: a cryptographic ISE for RISC-V
Organization: scarv
risc-v riscv verilog formal-verification yosys icarus-verilog hardware hardware-acceleration cryptography instruction-set-architecture

sec-bit / tokenlibs-with-proofs
formal-verification,Correctness proofs of Ethereum token contracts
Organization: sec-bit
coq erc20 formal-verification proof token

sifive / riscvspecformal
formal-verification,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.
Organization: sifive
coq hardware hardware-designs formal-verification riscv riscv-simulator

statebox / idris-ct
formal-verification,formally verified category theory library
Organization: statebox
category-theory formal-verification formal-proofs

stepchowfun / proofs
formal-verification,My personal repository of formally verified mathematics.
User: stepchowfun
coq proof-assistant formal-verification type-theory interactive-theorem-proving

tmeissner / psl_with_ghdl
formal-verification,Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)
User: tmeissner
vhdl psl ghdl yosys formal-verification assertions symbiyosys functional-coverage

tofgarion / spark-by-example
formal-verification,SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
User: tofgarion
formal-verification formal-methods formal-specification ada

troyguo / awesome-dv
formal-verification,Awesome ASIC design verification
User: troyguo
verification uvm formal-verification asic asic-verification

verivital / nnv
formal-verification,Neural Network Verification Software Tool
Organization: verivital
Home Page: http://www.verivital.com
neural-network verification autonomy cyber-physical cyber-physical-systems formal-methods formal-verification hybrid-systems neural-network-verification reachability

viperproject / prusti-dev
formal-verification,A static verifier for Rust, based on the Viper verification infrastructure.
Organization: viperproject
Home Page: http://prusti.org
rust verification viper formal-verification

workcraft / workcraft
formal-verification,Toolset to capture, simulate, synthesize and verify graph models
Organization: workcraft
Home Page: https://workcraft.org
cad eda formal-specification formal-verification logic-synthesis simulation petri-nets stg fsm circuit