formal-verification
There are 482 repositories under formal-verification topic.
p-org/P
The P programming language.
hacl-star/hacl-star
HACL*, a formally verified cryptographic library written in F*
viperproject/prusti-dev
A static verifier for Rust, based on the Viper verification infrastructure.
creusot-rs/creusot
Creusot helps you prove your code is correct in an automated fashion.
CakeML/cakeml
CakeML: A Verified Implementation of ML
magmide/magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
niltok/magic-in-ten-mins
十分钟魔法练习
sarsko/CreuSAT
CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
ligurio/practical-fm
A gently curated list of companies using verification formal methods in industry
ben-marshall/awesome-open-hardware-verification
A List of Free and Open Source Hardware Verification Tools and Frameworks
PrincetonUniversity/VST
Verified Software Toolchain
mesalock-linux/mesapy
A Fast and Safe Python based on PyPy
acl2/acl2
ACL2 System and Books as Maintained by the Community
formal-land/coq-of-rust
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦
stepchowfun/proofs
My personal repository of formally verified mathematics.
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.
statebox/idris-ct
formally verified category theory library
hacspec/hacspec
Please see https://github.com/hacspec/hax
JuliaReach/LazySets.jl
Scalable symbolic-numeric set computations in Julia
troyguo/awesome-dv
Awesome ASIC design verification
awesomo4000/awesome-provable
A curated set of links to formal methods involving provable code.
JuliaReach/ReachabilityAnalysis.jl
Computing reachable states of dynamical systems in Julia
hwayne/learntla-v2
Learn TLA+ for free! No prior experience necessary!
Frama-C/Frama-C-snapshot
Release snapshots of the Frama-C platform for source code analysis
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
AeneasVerif/aeneas
A verification toolchain for Rust programs
hacspec/hax
A Rust verification tool
leonardoalt/yools
Tools for Yul.
CertiCoq/certicoq
A Verified Compiler for Gallina, Written in Gallina
project-oak/silveroak
Formal specification and verification of hardware, especially for security and privacy.
AdaCore/RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
verivital/nnv
Neural Network Verification Software Tool
sec-bit/tokenlibs-with-proofs
Correctness proofs of Ethereum token contracts
fraunhoferfokus/acsl-by-example
Public snapshots of "ACSL by Example"
scarv/xcrypto
XCrypto: a cryptographic ISE for RISC-V
fizzbee-io/fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications