formal-methods
There are 406 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/mathlib3
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.
informalsystems/quint
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
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
acl2/acl2
ACL2 System and Books as Maintained by the Community
johnyf/tool_lists
Links to tools by subject
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs
tlaplus/vscode-tlaplus
TLA+ language support for Visual Studio Code
AeneasVerif/aeneas
A verification toolchain for Rust programs
hwayne/learntla-v2
Learn TLA+ for free! No prior experience necessary!
veyselusta/programming-language-research
Research on theory of programming languages λ, compilers, interpreters, functional programming, formal methods, logic etc.
fizzbee-io/fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
florianschanda/miss_hit
MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more
philzook58/z3_tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
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
mit-plv/koika
A core language for rule-based hardware design 🦑
verivital/nnv
Neural Network Verification Software Tool
AeneasVerif/charon
Interface with the rustc compiler for the purpose of program verification
AdaCore/RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
fraunhoferfokus/acsl-by-example
Public snapshots of "ACSL by Example"
Gbury/mSAT
A modular sat/smt solver with proof output.
will62794/spectacle
Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.
ACassimiro/TSNsched
Automated Schedule Generation for Time-Sensitive Networks (TSN).
engboris/stellogen
An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax
JetBrains-Research/coqpilot
VSCode extension that is designed to help automate writing of Coq proofs.
jdnklau/fm-ml
Collection of resources for research concerning Machine Learning and Formal Methods.
hwayne/tlacli
A script for running TLA+/TLC from the command line
JBakouny/Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
input-output-hk/high-assurance-legacy
Legacy code connected to the high-assurance implementation of the Ouroboros protocol family