the champagne of beta embedded databases
The P programming language.
My own notes (drafts mostly) about software quality
HACL*, a formally verified cryptographic library written in F*
Creusot helps you prove your Rust code is correct.
Lean 3's obsolete mathematical components library: please use mathlib4
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
A verification toolchain for Rust programs
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
A gently curated list of companies using verification formal methods in industry
Verified Software Toolchain
The specification language that talks back
ACL2 System and Books as Maintained by the Community
TLA+ language support for Visual Studio Code
Analyze Rust crates without touching compiler internals
Verification framework and tool for higher-order Scala programs. https://gitlab.epfl.ch/lara/stainless
Links to tools by subject
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
Research on theory of programming languages λ, compilers, interpreters, functional programming, formal methods, logic etc.
To associate your repository with the formal-methods topic, visit your repo's landing page and select "manage topics."