Formal Methods

Open-source projects categorized as Formal Methods
Edit details
Language: + Rust + Haskell + Coq + Ada + Python + C# + Lean + F* + HTML + TypeScript + Jupyter Notebook + TeX + Standard ML
Topics: Formal Verification Verification Math tla Rust
The modern identity platform for B2B SaaS
The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
workos.com
Sponsored

Top 23 Formal Method Open-Source Projects

  • sled

    the champagne of beta embedded databases

    • Project mention: SableDb – a key/value store that uses RocksDB and Redis API (written in Rust) | news.ycombinator.com | 2024-04-04

    a few times, seems interesting. The author's also built a lot of other cool concurrency primitives for Rust as well.

    [0] https://github.com/spacejam/sled

  • P

    The P programming language.

    • Project mention: Property-based testing in practice [pdf] | news.ycombinator.com | 2024-04-02

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo

  • sqa-wiki

    My own notes (drafts mostly) about software quality

    • Project mention: 10 Github Repositories for Software Testers | dev.to | 2023-10-21

    4. SQA wiki

  • mathlib

    Lean 3's obsolete mathematical components library: please use mathlib4

    • Project mention: An Easy-Sounding Problem Yields Numbers Too Big for Our Universe | news.ycombinator.com | 2023-12-04

  • hacl-star

    HACL*, a formally verified cryptographic library written in F*

  • creusot

    Creusot helps you prove your code is correct in an automated fashion.

    • Project mention: Creusot, a deductive verifier for Rust code | news.ycombinator.com | 2024-02-29

  • magmide

    A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.

    • Project mention: Languages on the rise like Rust and Go are being quite vocal against inheritance and many engineers seem to agree. Is this the end of inheritance? What do you think? | /r/rust | 2023-07-04

    https://github.com/magmide/magmide when

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

    WorkOS logo

  • CreuSAT

    CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.

  • practical-fm

    A gently curated list of companies using verification formal methods in industry

  • stainless

    Verification framework and tool for higher-order Scala programs (by epfl-lara)

  • vscode-tlaplus

    TLA+ language support for Visual Studio Code

  • 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

  • z3_tutorial

    Jupyter notebooks for tutorial on the Z3 SMT solver

  • what4

    Symbolic formula representation and solver interaction library

  • miss_hit

    MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more

  • koika

    A core language for rule-based hardware design 🦑

  • RecordFlux

    Formal specification and generation of verifiable binary parsers, message generators and protocol state machines

  • acsl-by-example

    Public snapshots of "ACSL by Example"

  • fizzbee

    Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

    • Project mention: FizzBee: Open-source formal methods tool that's not hard | news.ycombinator.com | 2024-04-01

  • hermit

    Haskell Equational Reasoning Model-to-Implementation Tunnel (by ku-fpg)

  • sbvPlugin

    Formally prove properties of Haskell programs using SBV/SMT.

  • hardware

    Verilog development and verification project for HOL4 (by CakeML)

  • PFV

    This tool presents a novel approach to bolstering network protocol verification by integrating the Shadow network simulator with the Ivy formal verification tool to check time properties. Furthermore, it extends Ivy’s capabilities with a dedicated time module, enabling the verification of complex quantitative-time properties.

    • Project mention: Show HN: PFV (Protocols Formal Verification) | news.ycombinator.com | 2024-03-04

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020).

Formal Methods related posts

Index

What are some of the best open-source Formal Method projects? This list will help you:

Project Stars
1 sled 7,736
2 P 2,911
3 sqa-wiki 2,200
4 mathlib 1,625
5 hacl-star 1,583
6 creusot 968
7 magmide 804
8 CreuSAT 581
9 practical-fm 460
10 stainless 347
11 vscode-tlaplus 329
12 spark-by-example 150
13 z3_tutorial 147
14 what4 146
15 miss_hit 143
16 koika 128
17 RecordFlux 100
18 acsl-by-example 94
19 fizzbee 63
20 hermit 49
21 sbvPlugin 44
22 hardware 23
23 PFV 17

Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com