formal-methods

Here are 301 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 Dec 8, 2022
Rust

p-org / P

Star

The P programming language.

programming-language distributed-systems state-machine robotics asynchronous systematic-testing event-driven model-checking formal-methods p formal-verification

Updated Mar 10, 2023
C#

ligurio / sqa-wiki

Star

My own notes (draft mostly) about software quality

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

Updated Feb 1, 2023

leanprover-community / mathlib

Star

Lean mathematical components library

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

Updated Mar 21, 2023
Lean

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 Mar 20, 2023
F*

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 Mar 17, 2023
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 Mar 20, 2023
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 Mar 6, 2023
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 Feb 3, 2023

PrincetonUniversity / VST

Star

Verified Software Toolchain

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

Updated Mar 19, 2023
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 Mar 20, 2023
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 Mar 20, 2023
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 Jan 17, 2023
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

florianschanda / miss_hit

Star

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

parser metrics matlab linter python3 octave lexer formal-methods simulink static-analyzer style-checker code-formatter

Updated Nov 24, 2022
Python

AdaCore / 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 Mar 20, 2023
Ada

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

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

Feb	MAR	Apr
	21
2022	2023	2024