formal-verification

Here are 363 public repositories matching this topic...

hacl-star / hacl-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 30, 2022
F*

viperproject / prusti-dev

Star

A static verifier for Rust, based on the Viper verification infrastructure.

rust verification viper formal-verification

Updated Oct 28, 2022
Rust

CakeML / cakeml

Star

CakeML: A Verified Implementation of ML

programming-language compiler formal-semantics theorem-proving sml formal-verification hol

Updated Oct 30, 2022
Standard ML

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

niltok / magic-in-ten-mins

Star

十分钟魔法练习

java tutorial functional-programming lambda-calculus monad hkt adt formal-verification formal-proofs

Updated Mar 30, 2022
HTML

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 28, 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

mesalock-linux / mesapy

Star

A Fast and Safe Python based on PyPy

python rust memory-safety pypy sgx formal-verification

Updated Sep 3, 2020
Python

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 28, 2022
Coq

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 31, 2022
Common Lisp

ben-marshall / awesome-open-hardware-verification

Star

A List of Free and Open Source Hardware Verification Tools and Frameworks

python coverage awesome hardware vhdl verification verilog awesome-list formal-verification constrained-random-verification

Updated Apr 18, 2022

stepchowfun / proofs

Sponsor

Star

My personal repository of formally verified mathematics.

coq proof-assistant type-theory formal-verification interactive-theorem-proving

Updated Oct 31, 2022
Coq

statebox / idris-ct

Star

formally verified category theory library

category-theory formal-verification formal-proofs

Updated Jun 23, 2020
Idris

JuliaReach / LazySets.jl

Star

Scalable Symbolic-Numeric Set Computations

calculus geometry julia computational-geometry convex-hull lazy-evaluation polygons projections formal-verification polyhedra sets minkowski-sum reachability-analysis convex-sets geometry-algorithms zonotope set-propagation

Updated Oct 30, 2022
Julia

awesomo4000 / awesome-provable

Star

A curated set of links to formal methods involving provable code.

coq idris agda isabelle formal-verification isabelle-hol sel4 certified-programming

Updated Dec 12, 2021

JuliaReach / ReachabilityAnalysis.jl

Star

Methods to compute sets of states reachable by dynamical systems

julia verification ode simulations dynamical-systems control-systems differential-equations interval-arithmetic hybrid-systems formal-verification numerical-analysis cyber-physical-systems reachability-analysis automatic-control flowpipe rigorous-numerics set-propagation

Updated Oct 26, 2022
Julia

hacspec / hacspec

Star

A specification language for cryptography primitives.

cryptography specifications formal-verification

Updated Oct 28, 2022
Rust

Frama-C / Frama-C-snapshot

Star

Release snapshots of the Frama-C platform for source code analysis

c static-analysis ocaml formal-verification abstract-interpretation runtime-verification

Updated Oct 21, 2020
OCaml

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

Improve this page

Add a description, image, and links to the formal-verification 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-verification topic, visit your repo's landing page and select "manage topics."

Learn more

Sep	OCT	Nov
	31
2021	2022	2023