formal-methods
There are 369 repositories under formal-methods topic.
spacejam/sled
the champagne of beta embedded databases
p-org/P
The P programming language.
ligurio/sqa-wiki
My own notes (drafts mostly) about software quality
leanprover-community/mathlib
Lean 3's obsolete mathematical components library: please use mathlib4
hacl-star/hacl-star
HACL*, a formally verified cryptographic library written in F*
creusot-rs/creusot
Creusot helps you prove your code is correct in an automated fashion.
magmide/magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
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
PrincetonUniversity/VST
Verified Software Toolchain
johnyf/tool_lists
Links to tools by subject
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs
acl2/acl2
ACL2 System and Books as Maintained by the Community
tlaplus/vscode-tlaplus
TLA+ language support for Visual Studio Code
hwayne/learntla-v2
Learn TLA+ for free! No prior experience necessary!
AeneasVerif/aeneas
A verification toolchain for Rust programs
florianschanda/miss_hit
MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more
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
philzook58/z3_tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
mit-plv/koika
A core language for rule-based hardware design 🦑
AdaCore/RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
verivital/nnv
Neural Network Verification Software Tool
fraunhoferfokus/acsl-by-example
Public snapshots of "ACSL by Example"
Gbury/mSAT
A modular sat/smt solver with proof output.
fizzbee-io/fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
ACassimiro/TSNsched
Automated Schedule Generation for Time-Sensitive Networks (TSN).
JBakouny/Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
hwayne/tlacli
A script for running TLA+/TLC from the command line
input-output-hk/high-assurance-legacy
Legacy code connected to the high-assurance implementation of the Ouroboros protocol family
WilfredTA/symbolic-stack-machines
Library for building symbolically executable stack-based virtual machines
cristian-mattarei/CoSA
CoreIR Symbolic Analyzer
AeneasVerif/charon
Interface with the rustc compiler for the purpose of program verification
jdnklau/fm-ml
Collection of resources for research concerning Machine Learning and Formal Methods.
GaloisInc/grift
Galois RISC-V ISA Formal Tools
IBM/vsrl-framework
The Verifiably Safe Reinforcement Learning Framework