#

formal-verification

Here are 317 public repositories matching this topic...

project-everest / 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 Apr 11, 2022
F*

CakeML / cakeml

Open

Formalise DEFLATE and add implementation to examples

5

myreen commented Nov 16, 2020

Deflate is a lossless data compression file format that zip and gzip are based on.

The deflate algorithm would be a nice formalisation and verification exercise in HOL. The result of the formalisation effort could be used to con

Read more

enhancement good first issue medium effort

Open

Platform for unverified assembly-level experiments

1

Open

The encoders are _big_

1

Find more good first issues

viperproject / prusti-dev

Open

Call vergen instead of git

fpoli commented Dec 21, 2021

The vergen crate seems a better alternative than manually calling git

https://github.com/viperproject/prusti-dev/blob/69325d35ec51a45118ec93ed4e46957e1d08f903/prusti/build.rs#L12-L16
https://github.com/viperproject/prusti-dev/blob/69325d35ec51a45118ec93ed4e46957e1d08f903/prusti/build.rs#L21-L25

Read more

enhancement good first issue

Open

Use FxHashSet/FxHashMap

2

Open

Build and publish Docker images via GitHub actions

1

Find more good first issues

niltok / magic-in-ten-mins

十分钟魔法练习

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

Updated Mar 30, 2022
HTML

mesalock-linux / mesapy

A Fast and Safe Python based on PyPy

python rust memory-safety pypy sgx formal-verification

Updated Sep 3, 2020
Python

ligurio / practical-fm

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 Dec 14, 2021

PrincetonUniversity / VST

Verified Software Toolchain

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

Updated Apr 4, 2022
Coq

magmide / magmide

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 Apr 8, 2022
Coq

creusot

xldenis / creusot

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 Apr 9, 2022
Rust

acl2 / acl2

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

statebox / idris-ct

formally verified category theory library

category-theory formal-verification formal-proofs

Updated Jun 23, 2020
Idris

JuliaReach / LazySets.jl

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 Apr 11, 2022
Julia

ben-marshall / awesome-open-hardware-verification

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 Nov 10, 2021

stepchowfun / proofs

Sponsor

A selection of formal proofs in Coq.

coq proof-assistant type-theory formal-verification

Updated Apr 9, 2022
Coq

awesomo4000 / awesome-provable

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

Frama-C / Frama-C-snapshot

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

JuliaReach / ReachabilityAnalysis.jl

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 Mar 5, 2022
Julia

tofgarion / 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

formal-methods ada formal-verification formal-specification

Updated Jul 2, 2021
Ada

hacspec / hacspec

A specification language for cryptography primitives.

cryptography specifications formal-verification

Updated Apr 5, 2022
Rust

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.

hardware coq formal-verification

Updated Feb 26, 2022
Coq

sec-bit / tokenlibs-with-proofs

Correctness proofs of Ethereum token contracts

coq proof token formal-verification erc20

Updated Jun 5, 2019
Coq

CertiCoq / certicoq

A Verified Compiler for Gallina, Written in Gallina

compiler coq formal-verification gallina

Updated Apr 11, 2022
Coq

input-output-hk / high-assurance-legacy

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

fraunhoferfokus / acsl-by-example

Public snapshots of "ACSL by Example"

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

Updated Jun 17, 2021
TeX

troyguo / awesome-dv

Awesome ASIC design verification

asic verification uvm formal-verification asic-verification

Updated Feb 9, 2022

Componolit / RecordFlux

Formal message specification and generation of verifiable binary parsers and message generators

parser spark formal-methods ada binary-parser formal-verification formal-specification

Updated Apr 11, 2022
Ada

scarv / xcrypto

XCrypto: a cryptographic ISE for RISC-V

open-source cryptography cpu crypto hardware riscv verilog research-project mit-license ise icarus-verilog hardware-acceleration formal-verification yosys instruction-set-architecture risc-v xcrypto

Updated Mar 31, 2021
Verilog

sifive / RiscvSpecFormal

The RiscvSpecKami package provides SiFive's RISC-V processor model. Built using Coq, this processor model can be used for simulation, model checking, and semantics analysis. The RISC-V processor model can be output as Verilog and simulated/synthesized using standard Verilog tools.

hardware coq riscv hardware-designs formal-verification riscv-simulator

Updated Apr 24, 2020
Haskell

newca12 / awesome-rust-formalized-reasoning

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

rust dependent-types logic theorem-proving formal-verification prover automated-theorem-provers reasoning theorem-prover constructive-mathematics proof-assistants

Updated Mar 26, 2022

interchainio / funding

Information about the Interchain Foundation Funding Program

open-source funding cryptography research decentralized blockchain cosmos permaculture tendermint formal-verification grant

Updated Mar 15, 2022

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."