GitHub topics: formal-methods

Repositories

acl2/acl2

ACL2 System and Books as Maintained by the Community

Language: Common Lisp - Size: 1.37 GB - Last synced at: about 10 hours ago - Pushed at: about 11 hours ago - Stars: 388 - Forks: 108

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs

Language: Scala - Size: 139 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 374 - Forks: 56

shuyang-dong/stlu_quantitative_predictative_monitor

Quantitative predicative monitoring and adaptive control based on Signal Temporal Logic with uncertainty in Cyber-Physical-System

Language: Python - Size: 264 MB - Last synced at: about 4 hours ago - Pushed at: 3 days ago - Stars: 0 - Forks: 0

AeneasVerif/charon

Interface with the rustc compiler for the purpose of program verification

Language: Rust - Size: 6.33 MB - Last synced at: 2 days ago - Pushed at: 3 days ago - Stars: 138 - Forks: 19

creusot-rs/creusot

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

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

fizzbee-io/fizzbee

Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

Language: Python - Size: 1.02 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 216 - Forks: 14

hacl-star/hacl-star

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

Language: F* - Size: 569 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 1,748 - Forks: 179

will62794/spectacle

Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.

Language: JavaScript - Size: 29.1 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 117 - Forks: 9

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: 2 days ago - Pushed at: 2 months ago - Stars: 38 - Forks: 3

data61/PSL

Language: Isabelle - Size: 175 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 68 - Forks: 9

AeneasVerif/aeneas

A verification toolchain for Rust programs

Language: OCaml - Size: 8.55 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 257 - Forks: 24

spacejam/sled

the champagne of beta embedded databases

Language: Rust - Size: 9.03 MB - Last synced at: 5 days ago - Pushed at: 4 months ago - Stars: 8,435 - Forks: 395

se-buw/fm-playground

A Formal Method playground for limboole, Z3, nuXmv, Alloy, and Spectra

Language: TypeScript - Size: 103 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 11 - Forks: 3

informalsystems/quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

Language: TypeScript - Size: 65.1 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 923 - Forks: 48

sandialabs/elaenia

Automated Error Analysis of Numerical Software for High-Consequence Systems

Language: OCaml - Size: 472 KB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 6 - Forks: 1

florianschanda/miss_hit

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

Language: Python - Size: 4.06 MB - Last synced at: 4 days ago - Pushed at: 8 months ago - Stars: 182 - Forks: 20

tlaplus/vscode-tlaplus

TLA+ language support for Visual Studio Code

Language: TypeScript - Size: 25 MB - Last synced at: 7 days ago - Pushed at: 8 days ago - Stars: 375 - Forks: 39

chasenorman/CanonicalLean

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

Language: C - Size: 6.15 MB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 31 - Forks: 0

chasenorman/Canonical

Canonical is a performant sound and complete type inhabitation solver for dependent type theory.

Language: Lean - Size: 82 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 21 - Forks: 1

sarsko/CreuSAT

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

Language: Rust - Size: 169 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 637 - Forks: 12

drakedu/formalize

FORMALIZE is a lightweight framework that improves LLM-based program synthesis by automatically leveraging formal methods to enhance code generation accuracy and consistency.

Language: Python - Size: 53.5 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 0 - Forks: 0

leanprover-community/mathlib3 📦

Lean 3's obsolete mathematical components library: please use mathlib4

Language: Lean - Size: 213 MB - Last synced at: 4 days ago - Pushed at: 11 months ago - Stars: 1,664 - Forks: 294

alumkal/awesome-formal-ai

A curated list of awesome formal reasoning AI.

Size: 7.81 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 2 - Forks: 0

p-org/P

The P programming language.

Language: C# - Size: 143 MB - Last synced at: 3 days ago - Pushed at: 8 days ago - Stars: 3,281 - Forks: 194

IntersectMBO/formal-ledger-specifications

Formal specifications of the cardano ledger

Language: Agda - Size: 188 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 41 - Forks: 15

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: 8 days ago - Pushed at: 4 months ago - Stars: 27 - Forks: 2

daviddoret/punctilious

A human-friendly and developer-friendly math proof assistant

Language: Python - Size: 55.2 MB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 2 - Forks: 0

cristian-mattarei/CoSA

CoreIR Symbolic Analyzer

Language: Python - Size: 7.98 MB - Last synced at: 8 days ago - Pushed at: over 4 years ago - Stars: 72 - Forks: 17

TYehan/NuSMV-Practicals

Practical on concurrent system modeling and simulations using NuSMV. :Formal Methods and Software Verification module in University Final Year :SE

Language: Batchfile - Size: 5.86 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 0 - Forks: 0

Hifza-Khalid/FormalMethodsInSE

🔍A deep dive into Formal Methods in Software Engineering 📜—exploring automata, logic, verification, and specification techniques to ensure software correctness and reliability.

Language: Python - Size: 5.86 KB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 3 - Forks: 0

NethermindEth/formalverification.xyz

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

Language: TypeScript - Size: 1.6 MB - Last synced at: 8 days ago - Pushed at: about 1 month ago - Stars: 9 - Forks: 8

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 74.7 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 463 - Forks: 93

ligurio/sqa-wiki

My own notes (drafts mostly) about software quality

Size: 392 KB - Last synced at: 5 days ago - Pushed at: over 2 years ago - Stars: 2,285 - Forks: 409

engboris/stellogen

An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax

Language: OCaml - Size: 2.06 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 101 - Forks: 9

sillydan1/graphedit

The extendable graph editor

Language: Java - Size: 8.24 MB - Last synced at: 18 days ago - Pushed at: 19 days ago - Stars: 7 - Forks: 0

input-output-hk/iog-agda-prelude

Supplementary types and functions for the Agda prelude

Language: Agda - Size: 47.9 KB - Last synced at: 2 days ago - Pushed at: 27 days ago - Stars: 3 - Forks: 0

tomooda/ViennaTalk

ViennaTalk, a LIVE IDE for VDM-SL based on Pharo Smalltalk

Language: Smalltalk - Size: 48.7 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 14 - Forks: 0

objectionary/news.eolang.org

Our Official Blog: we write about the development of EOLANG and 𝜑-calculus

Language: HTML - Size: 306 KB - Last synced at: 9 days ago - Pushed at: 24 days ago - Stars: 14 - Forks: 7

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: 49 - Forks: 5

Koukyosyumei/LeanDiary

Solving Software Foundations in Lean4

Language: Lean - Size: 54.7 KB - Last synced at: 3 days ago - Pushed at: 23 days ago - Stars: 0 - Forks: 0

JetBrains-Research/coqpilot

VSCode extension that is designed to help automate writing of Coq proofs.

Language: TypeScript - Size: 18.8 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 100 - Forks: 4

MixedMatched/juniper

A toy formally-specified Computer Algebra library written in Rust and formalized in Lean 4

Language: Rust - Size: 110 KB - Last synced at: 2 days ago - Pushed at: 4 months ago - Stars: 15 - Forks: 1

sandialabs/xstack-klokkos

Language: C++ - Size: 3.18 MB - Last synced at: 5 days ago - Pushed at: 29 days ago - Stars: 8 - Forks: 0

ldv-klever/klever

Read-only mirror of the Klever Git repository

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

Inferara/inferara.com

Inferara official website

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

AllanBlanchard/tutoriel_wp

Frama-C and WP tutorial

Language: TeX - Size: 10.3 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 58 - Forks: 18

LAVA-LAB/lava-lab.github.io

Language: JavaScript - Size: 176 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 2 - Forks: 2

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: 28 days ago - Pushed at: about 1 year ago - Stars: 823 - Forks: 13

lisa-analyzer/lisa

📚 a modular easy to use Library for Static Analysis aiming at multi-language analysis

Language: Java - Size: 8.68 MB - Last synced at: 23 days ago - Pushed at: 24 days ago - Stars: 57 - Forks: 35

sigp/verified-consensus

Formalisation of Ethereum consensus in Isabelle/HOL

Language: Isabelle - Size: 1010 KB - Last synced at: about 15 hours ago - Pushed at: 6 days ago - Stars: 3 - Forks: 1

rljacobson/mod2

Independent implementation of the pattern matching algorithms in Maude.

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

hwayne/tlacli

A script for running TLA+/TLC from the command line

Language: Python - Size: 2.7 MB - Last synced at: about 13 hours ago - Pushed at: about 4 years ago - Stars: 80 - Forks: 4

ligurio/practical-fm

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

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

CakeML/hardware

Verilog development and verification project for HOL4

Language: Standard ML - Size: 4.85 MB - Last synced at: 15 days ago - Pushed at: 16 days ago - Stars: 26 - Forks: 5

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: 1 day ago - Pushed at: 5 months ago - Stars: 40 - Forks: 18

onera/pml-analyzer

The PML analyzer is an open source API providing a simple DSL to build a description of the architecture of your chip based on the PHYLOG Modelling Language (PML).

Language: Scala - Size: 2.25 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 7 - Forks: 0

pkoerner/lisb

Language: Clojure - Size: 919 KB - Last synced at: 29 days ago - Pushed at: about 1 month ago - Stars: 5 - Forks: 2

urbanophile/awesome-sat-solvers

A curated collection of resources for the Boolean Satisfiability Problem (SAT).

Size: 144 KB - Last synced at: 2 days ago - Pushed at: 4 months ago - Stars: 5 - Forks: 0

CuriousCI/software-engineering

Software Engineering course @ Sapienza Università di Roma

Language: Typst - Size: 6.68 MB - Last synced at: about 1 month ago - Pushed at: 2 months ago - Stars: 17 - Forks: 0

GaloisInc/grift

Galois RISC-V ISA Formal Tools

Language: Haskell - Size: 7.55 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 58 - Forks: 8

mit-plv/koika

A core language for rule-based hardware design 🦑

Language: Coq - Size: 4.81 MB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 148 - Forks: 12

jinminhao/PANTS

[Usenix Security '25] Robustifying ML-powered Network Classifiers with PANTS

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

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: 22 days ago - Pushed at: about 1 month ago - Stars: 112 - Forks: 8

lean-machines-central/lean-machines

a Lean4 framework for the modeling and refinement of stateful systems

Language: Lean - Size: 705 KB - Last synced at: 3 days ago - Pushed at: 4 days ago - Stars: 11 - Forks: 2

verivital/nnv

Neural Network Verification Software Tool

Language: MATLAB - Size: 2.77 GB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 122 - Forks: 51

vasilisp/inez

A Constraint Solver

Language: OCaml - Size: 519 KB - Last synced at: about 1 month ago - Pushed at: over 9 years ago - Stars: 12 - Forks: 3

vasilisp/pub

My academic publications

Size: 3.32 MB - Last synced at: about 1 month ago - Pushed at: over 6 years ago - Stars: 1 - Forks: 0

marlowe-lang/marlowe-agda

Marlowe language specification

Language: Nix - Size: 373 KB - Last synced at: 4 days ago - Pushed at: 3 months ago - Stars: 9 - Forks: 4

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 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

systerel/RodinCore

Open tool platform for the cost effective rigorous development of dependable complex software systems services. This platform is based on the Event-B formal method and provides natural support for refinement and mathematical proof.

Language: Java - Size: 52.7 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 5 - Forks: 1

hengxin/sat-smt-satisfying

SAT and SMT

Language: Jupyter Notebook - Size: 86.2 MB - Last synced at: 16 days ago - Pushed at: almost 2 years ago - Stars: 6 - Forks: 2

JepMik/GCL-Build-Analyse-Tool

Program Parser, Compiler & Analyzer

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

johnyf/tool_lists

Links to tools by subject

Size: 63.5 KB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 375 - Forks: 83

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: 6 months ago - Stars: 13 - Forks: 6

koehlma/momba

A toolbox for dealing with formal models from construction to analysis based on the JANI-model interchange format.

Language: PDDL - Size: 32 MB - Last synced at: 2 days ago - Pushed at: 9 months ago - Stars: 19 - Forks: 3

overturetool/overture

The Overture Tool

Language: Java - Size: 210 MB - Last synced at: about 1 month ago - Pushed at: 7 months ago - Stars: 50 - Forks: 24

black-sat/black

BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)

Language: C++ - Size: 188 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 17 - Forks: 5

philzook58/z3_tutorial

Jupyter notebooks for tutorial on the Z3 SMT solver

Language: Jupyter Notebook - Size: 1.19 MB - Last synced at: 15 days ago - Pushed at: over 1 year ago - Stars: 160 - Forks: 20

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: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

doganulus/reelay

A header-only C++ library for system-level verification and declarative testing of real-time systems with Python bindings.

Language: C++ - Size: 2.98 MB - Last synced at: 5 days ago - Pushed at: about 1 year ago - Stars: 34 - Forks: 6

mkhaled87/pFaces-OmegaThreads

OmegaThreads constructs automatically correct-bu-construction controllers for dynamical systems to satisfy Omega-regular specifications given as discrete parity automata (DPA) or linear temporal logic (LTL) formulae. It constructs a symbolic model of the system and combine it with the specification into a parity game. Winning the parity game results into a closed-loop controller that enforces the specification on the system. The controller is generated as a Mealy machine. A Python interface and a 2d simulator are provided.

Language: C++ - Size: 70.4 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 9 - Forks: 2

mkhaled87/pFaces-PIRK Fork of alexdevonport/pfaces-pirk

A tool for parallel computation of interval over-approximations to reachable sets of nonlinear control systems, powered by the pFaces acceleration ecosystem; more briefly, a Parallel Interval Reachability Kernel.

Language: C++ - Size: 15.7 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 6 - Forks: 0

GabrielCellammare/Formal-Methods-for-Optimized-and-Verified-Drone-Delivery-Systems

This project combines Answer Set Programming for optimal drone delivery route planning with temporal logic verification of flight maneuvers. It balances distance and energy costs while formally verifying safety properties, providing mathematical guarantees for autonomous drone operations

Size: 0 Bytes - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

LeonardoSaccotelli/Formal-Methods-For-Computer-Science

Language: Jupyter Notebook - Size: 83.4 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

fadoss/maude-bindings

Language bindings for Maude

Language: SWIG - Size: 444 KB - Last synced at: 29 days ago - Pushed at: 4 months ago - Stars: 21 - Forks: 0

FlorianCassayre/master-project

Master Thesis Project at LARA (EPFL)

Language: Scala - Size: 940 KB - Last synced at: 4 days ago - Pushed at: almost 3 years ago - Stars: 3 - Forks: 0

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: 2 months ago - Pushed at: about 1 year ago - Stars: 17 - Forks: 1