formal-methods

Here are 280 public repositories matching this topic...

spacejam / sled

Sponsor

the champagne of beta embedded databases

rust tree orm database high-performance persistence fuzzing formal-methods concurrent lock-free log-structured kv b-tree sled b-plus-tree incredibly-spicy embedded-kv crash-testing

Updated Oct 6, 2022
Rust

ligurio / software-quality-wiki

Star

Software Quality Wiki

testing learning verification courses model-checking formal-methods quality-assurance ebooks software-testing tla

Updated Feb 9, 2021

hacl-star / hacl-star

Star

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

security cryptography high-performance verification formal-methods verified-primitives formal-verification everest inria hacl

Updated Oct 21, 2022
F*

leanprover-community / mathlib

Star

Lean mathematical components library

theorem-proving lean formal-methods formal-mathematics proof-automation formal-proofs

Updated Oct 21, 2022
Lean

magmide / magmide

Star

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

dependent-types coq logic verification formal-methods type-safety formal-verification systems-programming

Updated Sep 4, 2022
Coq

xldenis / creusot

Star

deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!

rust proof verification rust-lang formal-methods formal-verification deductive-reasoning why3

Updated Oct 20, 2022
Rust

sarsko / CreuSAT

Star

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

rust proof verification rust-lang formal-methods sat-solver minisat formal-verification sat automated-reasoning satisfiability deductive-reasoning

Updated Aug 4, 2022
Rust

ligurio / practical-fm

Star

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

practice coq software-engineering formal-methods formal-verification tlaplus tla-specification formal-verification-methods

Updated Oct 17, 2022

PrincetonUniversity / VST

Star

Verified Software Toolchain

c coq proof verification proof-assistant formal-methods compcert formal-verification coq-library formal-specification coq-vst

Updated Oct 20, 2022
Coq

johnyf / tool_lists

Star

Links to tools by subject

tools static-analysis theorem-proving verification proof-assistant smtlib synthesis satisfiability-solver binary-decision-diagrams model-checking satisfiability-modulo-theories formal-methods theorem-prover

Updated Jan 8, 2022

epfl-lara / stainless

Star

Verification framework and tool for higher-order Scala programs

scala verification z3 formal-methods inox smt leon cvc4

Updated Oct 15, 2022
HTML

acl2 / acl2

Star

ACL2 System and Books as Maintained by the Community

common-lisp logic theorem-proving first-order-logic formal-methods formal-verification theorem-prover rewriting acl2

Updated Oct 21, 2022
Common Lisp

tlaplus / vscode-tlaplus

Star

TLA+ language support for Visual Studio Code

verification specification vscode-extension model-checking formal-methods tla tlc pluscal

Updated Oct 18, 2022
TypeScript

tofgarion / spark-by-example

Star

SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada

formal-methods ada formal-verification formal-specification

Updated Aug 16, 2022
Ada

philzook58 / z3_tutorial

Sponsor

Star

Jupyter notebooks for tutorial on the Z3 SMT solver

tutorial jupyter z3 formal-methods smt smt-solver

Updated Sep 13, 2022
Jupyter Notebook

mit-plv / koika

Star

A core language for rule-based hardware design 🦑

semantics coq programming-languages formal-methods compilation hardware-description-language

Updated Mar 7, 2022
Coq

Gbury / mSAT

Star

A modular sat/smt solver with proof output.

formula modular ocaml solver formal-methods sat-solver smt-solver clause

Updated Oct 14, 2021
OCaml

Componolit / RecordFlux

Star

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

python parser spark communication-protocol formal-methods ada protocol-parser binary-parser formal-verification protocol-specification formal-specification

Updated Oct 19, 2022
Ada

fraunhoferfokus / acsl-by-example

Star

Public snapshots of "ACSL by Example"

c formal-methods wp-plugin formal-verification acsl frama-c formal-specification

Updated Jun 17, 2021
TeX

input-output-hk / high-assurance-legacy

Star

Legacy code connected to the high-assurance implementation of the Ouroboros protocol family

blockchain distributed-computing cryptocurrency formal-methods formal-verification cardano ouroboros

Updated Feb 4, 2022
Haskell

Improve this page

Add a description, image, and links to the formal-methods topic page so that developers can more easily learn about it.

Curate this topic

Add this topic to your repo

To associate your repository with the formal-methods topic, visit your repo's landing page and select "manage topics."

Learn more