hacl-star/hacl-star

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

Language: F* - Size: 567 MB - Last synced at: about 8 hours ago - Pushed at: 2 days ago - Stars: 1,732 - Forks: 177

sdthompson1/babylon

An experimental new programming language with verification features.

Language: C - Size: 1.77 MB - Last synced at: about 14 hours ago - Pushed at: about 15 hours ago - Stars: 1 - Forks: 0

AeneasVerif/aeneas

A verification toolchain for Rust programs

Language: OCaml - Size: 8.35 MB - Last synced at: about 18 hours ago - Pushed at: about 18 hours ago - Stars: 253 - Forks: 24

cryspen/hax

A Rust verification tool

Language: OCaml - Size: 55.8 MB - Last synced at: about 14 hours ago - Pushed at: 4 days ago - Stars: 249 - Forks: 22

EGmux/Sarcophagus_certora_formal-verification

Formal verification of Sarcophagus, the Autonomous and decentralized dead man's switch

Language: Solidity - Size: 594 KB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 1 - Forks: 0

Ironclad-Project/Ironclad

Mirror of codeberg's repository

Language: Ada - Size: 3.01 MB - Last synced at: 1 day ago - Pushed at: 2 days ago - Stars: 27 - Forks: 4

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.

Size: 312 KB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 330 - Forks: 11

JuliaReach/LazySets.jl

Scalable symbolic-numeric set computations in Julia

Language: Julia - Size: 44 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 246 - Forks: 36

gipsyh/rIC3

Hardware Formal Verification Tool

Language: Rust - Size: 1.88 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 45 - Forks: 9

creusot-rs/creusot

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

Language: Rust - Size: 66.1 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 1,243 - Forks: 57

pawinkler/hypra-support

Hypra Support Extension for Visual Studio Code. Adds language support for Hypra / HHL.

Language: TypeScript - Size: 55.2 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 0 - Forks: 0

acl2/acl2

ACL2 System and Books as Maintained by the Community

Language: Common Lisp - Size: 1.37 GB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 381 - Forks: 107

SSProve/ssprove

A foundational framework for modular cryptographic proofs in Coq

Language: Coq - Size: 3.28 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 64 - Forks: 13

p-org/P

The P programming language.

Language: C# - Size: 143 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 3,272 - Forks: 195

Koukyosyumei/LeanDiary

Solving Software Foundations in Lean4

Language: Lean - Size: 54.7 KB - Last synced at: 1 day ago - Pushed at: 4 days ago - Stars: 0 - Forks: 0

SKolodynski/IsarMathLib

IsarMathLib is a library of formalized mathematics for Isabelle/ZF.

Language: Isabelle - Size: 146 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 18 - Forks: 1

mgrojo/coap_spark

Formally verified implementation of the CoAP protocol in SPARK/Ada

Language: Ada - Size: 1.82 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 4 - Forks: 0

Verified-zkEVM/ZKLib

Formally Verified SNARKs in Lean

Language: Lean - Size: 2.74 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 60 - Forks: 7

KeYProject/key

KeY Theorem Prover for Deductive Java Verification

Language: Java - Size: 207 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 55 - Forks: 29

formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

Language: Coq - Size: 98.5 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 889 - Forks: 31

IBM/ACE-RISCV

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for RISC-V with focus on a formally verified and auditable security monitor.

Language: Rust - Size: 2.07 MB - Last synced at: about 7 hours ago - Pushed at: about 8 hours ago - Stars: 47 - Forks: 12

alumkal/awesome-formal-ai

A curated list of awesome formal reasoning AI.

Size: 6.84 KB - Last synced at: 2 days ago - Pushed at: about 1 month ago - Stars: 2 - Forks: 0

PacoReinaCampo/MPSoC-DV

Multi-Processor System on Chip verified with UVM/OSVVM/FV

Language: SystemVerilog - Size: 37.3 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 28 - Forks: 15

PacoReinaCampo/SoC-DV

System on Chip verified with UVM/OSVVM/FV

Language: SystemVerilog - Size: 25.8 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 25 - Forks: 7

PacoReinaCampo/PU-DV

Processing Unit verified with UVM/OSVVM/FV

Language: SystemVerilog - Size: 16.6 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 4 - Forks: 4

wkolowski/Typonomikon

Źródła mojej książki o Coqu, programowaniu funkcyjnym, teorii typów, logice konstruktywnej i innych takich.

Language: Coq - Size: 215 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 12 - Forks: 0

CakeML/cakeml

CakeML: A Verified Implementation of ML

Language: Standard ML - Size: 117 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 1,022 - Forks: 87

AeneasVerif/charon

Interface with the rustc compiler for the purpose of program verification

Language: Rust - Size: 5.78 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 130 - Forks: 19

Ivan-Sergeyev/seymour

This project is about formally verifying Seymour's decomposition theorem for regular matroids.

Language: Lean - Size: 7.5 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 22 - Forks: 7

ciphercurve/toyni

Toyni is a new, emerging ZK proof system in Rust, developed by Ciphercurve.

Language: Rust - Size: 468 KB - Last synced at: 3 days ago - Pushed at: 8 days ago - Stars: 0 - Forks: 1

AthenaFoundation/athena

Athena is a modern, practical language for proof engineering & natural deduction.

Language: Standard ML - Size: 12.6 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 71 - Forks: 4

cryspen/libcrux

The formally verified crypto library for Rust

Language: C - Size: 48.5 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 117 - Forks: 17

troyguo/awesome-dv

Awesome ASIC design verification

Size: 18.6 KB - Last synced at: 10 days ago - Pushed at: about 3 years ago - Stars: 291 - Forks: 69

JuliaReach/ReachabilityAnalysis.jl

Computing reachable states of dynamical systems in Julia

Language: Julia - Size: 13.1 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 200 - Forks: 17

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 74.5 MB - Last synced at: about 5 hours ago - Pushed at: about 6 hours ago - Stars: 460 - Forks: 93

ldv-klever/klever

Read-only mirror of the Klever Git repository

Language: Python - Size: 162 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 21 - Forks: 14

Certora/SecurityReports

Certora's Formal Verification and Audit Portfolio – a comprehensive collection of smart contract security verification reports and audits for leading Web3 protocols on EVM-based chains, Solana, and Stellar.

Size: 43.6 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 16 - Forks: 1

Zinoex/IntervalMDPAbstractions.jl

Abstraction of stochastic systems to IMDPs and odIMDPs

Language: Julia - Size: 70.2 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 1 - Forks: 0

CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

Language: Coq - Size: 33.4 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 148 - Forks: 29

ElNiak/awesome-formal-verification

Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.

Size: 24.4 KB - Last synced at: 6 days ago - Pushed at: 3 months ago - Stars: 25 - Forks: 2

Inferara/inferara.com

Inferara official website

Language: HTML - Size: 760 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 1 - Forks: 2

adilanwar2399/ESBMC-ibmc

The ESBMC ibmc (Invariant Based Model Checking) Tool.

Language: C - Size: 327 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 6 - Forks: 1

NethermindEth/formalverification.xyz

A website listing all the best FV companies in the Crypto space.

Language: TypeScript - Size: 1.6 MB - Last synced at: 1 day ago - Pushed at: 12 days ago - Stars: 8 - Forks: 8

AllanBlanchard/tutoriel_wp

Frama-C and WP tutorial

Language: TeX - Size: 10.3 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 58 - Forks: 18

ben-marshall/awesome-open-hardware-verification

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

Size: 166 KB - Last synced at: 10 days ago - Pushed at: over 1 year ago - Stars: 519 - Forks: 51

awesomo4000/awesome-provable

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

Size: 25.4 KB - Last synced at: 10 days ago - Pushed at: over 3 years ago - Stars: 202 - Forks: 10

formal-land/coq-of-solidity Fork of ethereum/solidity

Formal verification for Solidity smart contracts with Coq 🐓 Verify arbitrary properties on your smart contracts and make no bugs!

Language: Coq - Size: 101 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 30 - Forks: 1

LAVA-LAB/lava-lab.github.io

Language: JavaScript - Size: 176 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 2 - Forks: 2

ariadne-cps/ariadne

C++ framework for rigorous computation on cyber-physical systems

Language: C++ - Size: 20 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 29 - Forks: 9

magmide/magmide

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

Language: Coq - Size: 38.5 MB - Last synced at: 9 days ago - Pushed at: about 1 year ago - Stars: 823 - Forks: 13

Certora/CertoraProver

The Certora Prover is the state-of-the-art security tool for automated formal verification of smart contracts running on EVM-based chains, Solana and Stellar

Language: Kotlin - Size: 12.2 MB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 160 - Forks: 15

Ivan-Klikovac/symexec

A symbolic execution engine that works on GCC's SSA GIMPLE

Language: C++ - Size: 20.5 KB - Last synced at: 14 days ago - Pushed at: 14 days ago - Stars: 0 - Forks: 0

allisterb/Silver

Static analyzer and formal verifier for Stratis smart contracts

Language: Jupyter Notebook - Size: 2.99 MB - Last synced at: 10 days ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 2

stepchowfun/proofs

My personal repository of formally verified mathematics.

Language: Coq - Size: 1.28 MB - Last synced at: 9 days ago - Pushed at: about 1 month ago - Stars: 297 - Forks: 13

ligurio/practical-fm

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

Size: 122 KB - Last synced at: 7 days ago - Pushed at: 2 months ago - Stars: 526 - Forks: 42

rbeauchamp/industrial-haskell-template

Industrial-grade Haskell project template for mission-critical systems. Features formal verification (LiquidHaskell), robust error handling, hexagonal architecture, TDD, and AI-assistant rules (Cursor)

Language: Haskell - Size: 122 KB - Last synced at: 5 days ago - Pushed at: 17 days ago - Stars: 0 - Forks: 0

NASA-SW-VnV/fret

A framework for the elicitation, specification, formalization and analysis of requirements.

Language: JavaScript - Size: 136 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 335 - Forks: 56

reilabs/proven-zk

A support library for working with zero knowledge cryptography in Lean 4.

Language: Lean - Size: 160 KB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 36 - Forks: 4

symbolicsoft/verifpal

Cryptographic protocol analysis for real-world protocols.

Language: Go - Size: 2.34 MB - Last synced at: 7 days ago - Pushed at: 8 months ago - Stars: 48 - Forks: 4

awslabs/aws-lc-verification

This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of the correctness and security of the library.

Language: Coq - Size: 633 KB - Last synced at: 9 days ago - Pushed at: 4 months ago - Stars: 40 - Forks: 18

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.

Language: Haskell - Size: 26.8 MB - Last synced at: 13 days ago - Pushed at: almost 5 years ago - Stars: 77 - Forks: 7

unl-nimbus-lab/pymavswarm

Python library used to safely control drone swarms and drone fleets with MAVLink

Language: Python - Size: 343 KB - Last synced at: 17 days ago - Pushed at: about 2 years ago - Stars: 20 - Forks: 5

AdaCore/RecordFlux

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

Language: Ada - Size: 32.2 MB - Last synced at: 3 days ago - Pushed at: 22 days ago - Stars: 112 - Forks: 8

ElNiak/PANTHER

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.

Language: C - Size: 1.2 GB - Last synced at: 6 days ago - Pushed at: about 2 months ago - Stars: 36 - Forks: 3

aai-institute/USFlows

Normalizing flows for neuro-symbolic AI

Language: Python - Size: 2.68 MB - Last synced at: about 17 hours ago - Pushed at: about 17 hours ago - Stars: 13 - Forks: 2

UQ-Trust-Lab/WraLU

An algorithm to calculate the convex hull of ReLU function for neural network verification.

Language: Python - Size: 2.99 MB - Last synced at: 25 days ago - Pushed at: 25 days ago - Stars: 3 - Forks: 1

maksym-bortin/a_framework

A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs

Language: Isabelle - Size: 227 KB - Last synced at: 25 days ago - Pushed at: 25 days ago - Stars: 0 - Forks: 0

verivital/nnv

Neural Network Verification Software Tool

Language: MATLAB - Size: 2.77 GB - Last synced at: 25 days ago - Pushed at: 25 days ago - Stars: 122 - Forks: 51

baselkhouri/edusat-bva

Implementing and integrating Simple Bounded Variable Addition (BVA) preprocessing technique in EDUSAT SAT solver

Language: C++ - Size: 8.39 MB - Last synced at: 28 days ago - Pushed at: 28 days ago - Stars: 0 - Forks: 0

BDSM-hardware/lock_handler

Manages multi points bondage locks, for self or collective bondage.

Language: PostScript - Size: 2.85 MB - Last synced at: 28 days ago - Pushed at: 28 days ago - Stars: 3 - Forks: 0

NethermindEth/horus-checker

Horus, a formal verification tool for StarkNet smart contracts.

Language: Haskell - Size: 1 MB - Last synced at: 16 days ago - Pushed at: about 2 years ago - Stars: 74 - Forks: 9

julianmendez/market

Multi-agent prototype of a market modeled in Soda that uses formal verification.

Language: Scala - Size: 279 KB - Last synced at: 18 days ago - Pushed at: about 1 month ago - Stars: 1 - Forks: 0

niltok/magic-in-ten-mins

十分钟魔法练习

Language: HTML - Size: 31.5 MB - Last synced at: 27 days ago - Pushed at: over 1 year ago - Stars: 800 - Forks: 38

runtimeverification/evm-equivalence

Equivalence proofs of EVM models

Language: Lean - Size: 102 KB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 2 - Forks: 0

tmeissner/libvhdl

Library of reusable VHDL components

Language: VHDL - Size: 263 KB - Last synced at: 3 days ago - Pushed at: about 1 year ago - Stars: 28 - Forks: 5

CASTLE-Benchmark/CASTLE-Source

The source code for the CASTLE Benchmark Tests, Wrappers, Evaluator, Diagrams and more

Language: C - Size: 196 KB - Last synced at: 7 days ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

Isaac-DeFrain/TLAplusFun

TLA+ questions, answers, and experiments

Language: TLA - Size: 3.39 MB - Last synced at: 20 days ago - Pushed at: over 2 years ago - Stars: 23 - Forks: 0

huynhtrankhanh/AlternateFace

New theorem prover based on set theory. Focuses on performance and usability, not theoretical concerns.

Language: TypeScript - Size: 412 KB - Last synced at: 9 days ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

djokovic55/packet_processing_crc8

Formal verification of the Packet Processing System. Application of the SST method.

Language: VHDL - Size: 9.09 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 1 - Forks: 0

hacspec/hacspec 📦

Please see https://github.com/hacspec/hax

Language: Coq - Size: 131 MB - Last synced at: 12 days ago - Pushed at: about 1 year ago - Stars: 243 - Forks: 42

mmhristov/Erlaplus

Erla+ is a compiler that transpiles PlusCal specs into Erlang implementations

Language: Java - Size: 29 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 3 - Forks: 0

tmeissner/psl_with_ghdl

Examples of using PSL for functional and formal verification of VHDL with GHDL (and SymbiYosys)

Language: VHDL - Size: 92.8 KB - Last synced at: 3 days ago - Pushed at: 3 months ago - Stars: 66 - Forks: 5

JepMik/GCL-Build-Analyse-Tool

Program Parser, Compiler & Analyzer

Language: F# - Size: 6.92 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 1 - Forks: 1

symbolicsoft/noiseexplorer

Online engine for reasoning about the Noise Protocol Framework.

Language: Rust - Size: 49.7 MB - Last synced at: 7 days ago - Pushed at: 5 months ago - Stars: 13 - Forks: 6

reilabs/gnark-lean-extractor

A tool to extract gnark circuits defined in Go to Lean for formal verification.

Language: Go - Size: 132 KB - Last synced at: 12 days ago - Pushed at: 17 days ago - Stars: 12 - Forks: 2

ThalesGroup/frama-c-lsp

This repository contains both the server and client software that implement the Language Server Protocol (LSP) for C/ACSL language. The server part is a novel Frama-C plugin called "lsp". The client part is a VsCode extension.

Language: OCaml - Size: 426 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

aerkiaga/nacre

A programming language for verified software.

Language: Rust - Size: 326 KB - Last synced at: 22 days ago - Pushed at: about 2 months ago - Stars: 0 - Forks: 0

ivanMilin/RISCV_multicore_cache_controller

This project is a final project in my master studies and it's done in a team of 2 people, Petar Stamenkovic and myself.

Language: SystemVerilog - Size: 14.8 MB - Last synced at: 15 days ago - Pushed at: 4 months ago - Stars: 4 - Forks: 1

gabrielrovesti/SystemFX

Framework di stream processing in F# con garanzie formali per costruire pipeline di elaborazione dati robuste e componibili

Language: F# - Size: 2.96 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

fvcrusher/fvcrusher.github.io

Formal Verification simplifier

Language: HTML - Size: 124 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

aman-goel/avr

Reads a state transition system and performs property checking

Language: C++ - Size: 910 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 76 - Forks: 20

meowesque/catk

C Analysis Toolkit

Language: Rust - Size: 58.6 KB - Last synced at: 1 day ago - Pushed at: about 2 months ago - Stars: 4 - Forks: 1

tudo-aqua/stars-auna-experiments

This repository analyzes driving data recorded with model race cars in a platooning scenario using the STARS framework.

Language: Kotlin - Size: 25.4 MB - Last synced at: about 1 month ago - Pushed at: 3 months ago - Stars: 2 - Forks: 0

Ghonimo/Formal-Verification-of-an-AHB2APB-Bridge

Assertion-Based Formal Verification of an AHB2APB bridge, featuring SystemVerilog assertions, RTL designs, and detailed documentation including a final report and project progression presentation.

Language: SystemVerilog - Size: 14.2 MB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 10 - Forks: 4

bor0/dafny-tutorial

Exercises for the Dafny Tutorial

Language: PHP - Size: 8.79 KB - Last synced at: 11 days ago - Pushed at: almost 7 years ago - Stars: 11 - Forks: 8

Ghonimo/Formal-Verification-With-VC-Formal--Tutorials-and-Examples

This repository is dedicated to providing a comprehensive guide and practical examples for using VC Formal for formal verification. Our goal is to help both beginners and experienced users understand the principles of formal verification and how to apply them effectively using VC Formal.

Size: 96.8 MB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 17 - Forks: 1

aionescu/lean-wasm

An intrinsically-typed interpreter for WebAssembly

Language: Lean - Size: 26.4 KB - Last synced at: 28 days ago - Pushed at: about 1 month ago - Stars: 2 - Forks: 0

trackoor/AwesomePL

A Collection of Papers & Notes in Programming Language & Formal Verification

Size: 10.3 MB - Last synced at: 3 days ago - Pushed at: almost 3 years ago - Stars: 17 - Forks: 1

modality-org/modality

verifiable contracts using temporal modal logic

Language: JavaScript - Size: 2.26 MB - Last synced at: 20 days ago - Pushed at: about 2 months ago - Stars: 4 - Forks: 0

hwayne/learntla-v2

Learn TLA+ for free! No prior experience necessary!

Language: TLA - Size: 2.14 MB - Last synced at: about 2 months ago - Pushed at: 2 months ago - Stars: 209 - Forks: 43