Topic: "formal-methods"
spacejam/sled
the champagne of beta embedded databases
Language: Rust - Size: 8.87 MB - Last synced at: about 15 hours ago - Pushed at: 21 days ago - Stars: 8,498 - Forks: 399
p-org/P
The P programming language.
Language: C# - Size: 153 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 3,298 - Forks: 195
ligurio/sqa-wiki
My own notes (drafts mostly) about software quality
Size: 392 KB - Last synced at: 24 days ago - Pushed at: over 2 years ago - Stars: 2,285 - Forks: 409
hacl-star/hacl-star
HACL*, a formally verified cryptographic library written in F*
Language: F* - Size: 572 MB - Last synced at: 5 days ago - Pushed at: 6 days ago - Stars: 1,757 - Forks: 179
leanprover-community/mathlib3 📦
Lean 3's obsolete mathematical components library: please use mathlib4
Language: Lean - Size: 213 MB - Last synced at: about 22 hours ago - Pushed at: 11 months ago - Stars: 1,667 - Forks: 294
creusot-rs/creusot
Creusot helps you prove your code is correct in an automated fashion.
Language: Rust - Size: 67 MB - Last synced at: 5 days ago - Pushed at: 12 days ago - Stars: 1,270 - Forks: 57
informalsystems/quint
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Language: TypeScript - Size: 65.3 MB - Last synced at: about 19 hours ago - Pushed at: about 20 hours ago - Stars: 941 - Forks: 70
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: 13 days ago - Pushed at: about 1 year ago - Stars: 823 - Forks: 13
sarsko/CreuSAT
CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
Language: Rust - Size: 169 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 637 - Forks: 12
ligurio/practical-fm
A gently curated list of companies using verification formal methods in industry
Size: 122 KB - Last synced at: 15 days ago - Pushed at: 4 months ago - Stars: 537 - Forks: 42
PrincetonUniversity/VST
Verified Software Toolchain
Language: Coq - Size: 74.1 MB - Last synced at: 5 days ago - Pushed at: 6 days ago - Stars: 463 - Forks: 94
acl2/acl2
ACL2 System and Books as Maintained by the Community
Language: Common Lisp - Size: 1.38 GB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 395 - Forks: 109
tlaplus/vscode-tlaplus
TLA+ language support for Visual Studio Code
Language: TypeScript - Size: 25.1 MB - Last synced at: about 19 hours ago - Pushed at: about 20 hours ago - Stars: 381 - Forks: 42
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs
Language: Scala - Size: 139 MB - Last synced at: about 15 hours ago - Pushed at: 22 days ago - Stars: 375 - Forks: 56
johnyf/tool_lists
Links to tools by subject
Size: 63.5 KB - Last synced at: 3 months ago - Pushed at: about 1 year ago - Stars: 375 - Forks: 83
AeneasVerif/aeneas
A verification toolchain for Rust programs
Language: OCaml - Size: 8.75 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 262 - Forks: 25
fizzbee-io/fizzbee
Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications
Language: Python - Size: 1.16 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 222 - Forks: 14
hwayne/learntla-v2
Learn TLA+ for free! No prior experience necessary!
Language: TLA - Size: 2.14 MB - Last synced at: 3 months ago - Pushed at: 4 months ago - Stars: 209 - Forks: 43
florianschanda/miss_hit
MATLAB Independent, Small & Safe, High Integrity Tools - code formatter and more
Language: Python - Size: 4.06 MB - Last synced at: 13 days ago - Pushed at: 9 months ago - Stars: 183 - Forks: 20
veyselusta/programming-language-research
Research on theory of programming languages λ, compilers, interpreters, functional programming, formal methods, logic etc.
Size: 38.1 KB - Last synced at: 5 months ago - Pushed at: 9 months ago - Stars: 169 - Forks: 6
philzook58/z3_tutorial
Jupyter notebooks for tutorial on the Z3 SMT solver
Language: Jupyter Notebook - Size: 1.19 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 160 - Forks: 20
mit-plv/koika
A core language for rule-based hardware design 🦑
Language: Coq - Size: 4.81 MB - Last synced at: 20 days ago - Pushed at: 8 months ago - Stars: 153 - Forks: 12
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
Language: Ada - Size: 1.03 MB - Last synced at: 10 months ago - Pushed at: almost 3 years ago - Stars: 150 - Forks: 16
AeneasVerif/charon
Interface with the rustc compiler for the purpose of program verification
Language: Rust - Size: 6.63 MB - Last synced at: 5 days ago - Pushed at: 6 days ago - Stars: 148 - Forks: 19
will62794/spectacle
Interactive, web-based tool for exploring, visualizing, and sharing formal specifications in TLA+.
Language: JavaScript - Size: 28.6 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 125 - Forks: 9
verivital/nnv
Neural Network Verification Software Tool
Language: MATLAB - Size: 2.77 GB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 122 - Forks: 51
AdaCore/RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Language: Ada - Size: 32.4 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 115 - Forks: 8
fraunhoferfokus/acsl-by-example
Public snapshots of "ACSL by Example"
Language: TeX - Size: 20.8 MB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 109 - Forks: 21
engboris/stellogen
An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax
Language: OCaml - Size: 2.09 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 106 - Forks: 10
JetBrains-Research/coqpilot
VSCode extension that is designed to help automate writing of Coq proofs.
Language: TypeScript - Size: 19.1 MB - Last synced at: 24 days ago - Pushed at: 24 days ago - Stars: 103 - Forks: 4
Gbury/mSAT
A modular sat/smt solver with proof output.
Language: OCaml - Size: 4.92 MB - Last synced at: 6 days ago - Pushed at: over 1 year ago - Stars: 99 - Forks: 8
hwayne/tlacli
A script for running TLA+/TLC from the command line
Language: Python - Size: 2.7 MB - Last synced at: 27 days ago - Pushed at: about 4 years ago - Stars: 80 - Forks: 4
JBakouny/Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Language: Scala - Size: 17.6 MB - Last synced at: 2 months ago - Pushed at: about 3 years ago - Stars: 79 - Forks: 7
input-output-hk/high-assurance-legacy 📦
Legacy code connected to the high-assurance implementation of the Ouroboros protocol family
Language: Haskell - Size: 4.53 MB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 78 - Forks: 16
cristian-mattarei/CoSA
CoreIR Symbolic Analyzer
Language: Python - Size: 7.98 MB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 72 - Forks: 17
chasenorman/CanonicalLean
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Language: Lean - Size: 8.79 MB - Last synced at: 3 days ago - Pushed at: 4 days ago - Stars: 69 - Forks: 4
ACassimiro/TSNsched
Automated Schedule Generation for Time-Sensitive Networks (TSN).
Language: Java - Size: 260 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 69 - Forks: 29
data61/PSL
Language: Isabelle - Size: 175 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 68 - Forks: 9
WilfredTA/symbolic-stack-machines
Library for building symbolically executable stack-based virtual machines
Language: Rust - Size: 125 KB - Last synced at: over 2 years ago - Pushed at: over 2 years ago - Stars: 68 - Forks: 8
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: about 23 hours ago - Pushed at: about 24 hours ago - Stars: 61 - Forks: 34
AllanBlanchard/tutoriel_wp
Frama-C and WP tutorial
Language: TeX - Size: 10.3 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 58 - Forks: 18
GaloisInc/grift
Galois RISC-V ISA Formal Tools
Language: Haskell - Size: 7.55 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 58 - Forks: 8
IBM/vsrl-framework 📦
The Verifiably Safe Reinforcement Learning Framework
Language: Python - Size: 1.92 MB - Last synced at: about 1 month ago - Pushed at: almost 4 years ago - Stars: 56 - Forks: 12
SatyendraBanjare/plt-formal-methods-resources
Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.
Size: 3.24 MB - Last synced at: 2 months ago - Pushed at: almost 6 years ago - Stars: 55 - Forks: 1
philzook58/nand2coq
Build an educational formally verified version of the Nand 2 Tetris course using Coq (and other formal tools).
Language: Coq - Size: 823 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 54 - Forks: 3
symbolicsoft/verifpal
Cryptographic protocol analysis for real-world protocols.
Language: Go - Size: 2.34 MB - Last synced at: 5 days ago - Pushed at: 9 months ago - Stars: 53 - Forks: 6
imandra-ai/fix-engine
Imandra FIX Engine
Language: OCaml - Size: 7.86 MB - Last synced at: 2 months ago - Pushed at: 7 months ago - Stars: 52 - Forks: 3
overturetool/overture
The Overture Tool
Language: Java - Size: 210 MB - Last synced at: 2 months ago - Pushed at: 8 months ago - Stars: 50 - Forks: 24
chasenorman/Canonical
Canonical is a performant sound and complete type inhabitation solver for dependent type theory.
Language: Lean - Size: 169 KB - Last synced at: about 24 hours ago - Pushed at: 1 day ago - Stars: 47 - Forks: 4
TorXakis/TorXakis
A tool for Model Based Testing
Language: Haskell - Size: 9.17 MB - Last synced at: 2 months ago - Pushed at: about 3 years ago - Stars: 47 - Forks: 13
ElliotSwart/pragmaticformalmodeling
An instructional website with progressively worked examples of TLA+ specifications and model checking.
Language: TLA - Size: 6.79 MB - Last synced at: 6 months ago - Pushed at: almost 3 years ago - Stars: 44 - Forks: 2
IntersectMBO/formal-ledger-specifications
Formal specifications of the cardano ledger
Language: Agda - Size: 197 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 41 - Forks: 15
davidlazar/llvm-semantics
Formal semantics of LLVM IR in K
Language: LLVM - Size: 14.4 MB - Last synced at: over 1 year ago - Pushed at: almost 10 years ago - Stars: 41 - Forks: 9
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: 17 days ago - Pushed at: 6 months ago - Stars: 40 - Forks: 18
c-cube/mc2
[research] A modular SMT solver in OCaml, based on mcSAT
Language: SMT - Size: 9.08 MB - Last synced at: 6 days ago - Pushed at: over 1 year ago - Stars: 39 - Forks: 5
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: 5 days ago - Pushed at: 6 days ago - Stars: 38 - Forks: 3
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: about 1 month ago - Pushed at: about 1 year ago - Stars: 34 - Forks: 6
robkorn/plutus-experimental-smart-contracts
Experimental Smart Contracts In Plutus.
Language: Haskell - Size: 68.4 KB - Last synced at: about 2 years ago - Pushed at: about 6 years ago - Stars: 34 - Forks: 8
zenprotocol/zen-wallet
Node and GUI for the Zen Protocol.
Language: C# - Size: 119 MB - Last synced at: over 2 years ago - Pushed at: over 7 years ago - Stars: 33 - Forks: 13
y-taka-23/ddsv-go
A toy deadlock detector written in Go. 🔍
Language: Go - Size: 428 KB - Last synced at: about 2 months ago - Pushed at: about 5 years ago - Stars: 30 - Forks: 2
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: 5 days ago - Pushed at: 5 months ago - Stars: 29 - Forks: 2
CakeML/hardware
Verilog development and verification project for HOL4
Language: Standard ML - Size: 4.85 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 26 - Forks: 5
c-cube/sidekick
A modular library for CDCL(T) SMT solvers, with [wip] proof generation.
Language: SMT - Size: 15.4 MB - Last synced at: 6 days ago - Pushed at: 4 months ago - Stars: 24 - Forks: 15
arandilopez/z-eves
Z-EVES for linux. Probably the only place you can find it
Language: Python - Size: 18.1 MB - Last synced at: about 1 month ago - Pushed at: about 4 years ago - Stars: 24 - Forks: 10
fadoss/maude-bindings
Language bindings for Maude
Language: SWIG - Size: 444 KB - Last synced at: 23 days ago - Pushed at: 5 months ago - Stars: 23 - Forks: 0
c-cube/smbc
Experimental model finder/SMT solver for functional programming.
Language: OCaml - Size: 1.07 MB - Last synced at: 6 days ago - Pushed at: almost 3 years ago - Stars: 23 - Forks: 0
Componolit/gneiss 📦
Framework for platform-independent SPARK components
Language: Ada - Size: 1.48 MB - Last synced at: 5 months ago - Pushed at: almost 5 years ago - Stars: 22 - Forks: 2
ldv-klever/klever
Read-only mirror of the Klever Git repository
Language: Python - Size: 162 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 21 - Forks: 14
Componolit/SXML
Formally verified, bounded-stack XML library
Language: Ada - Size: 69.3 MB - Last synced at: 10 months ago - Pushed at: about 5 years ago - Stars: 21 - Forks: 2
mgrabovsky/fm-notes
Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on
Language: Coq - Size: 218 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 20 - Forks: 2
cits5501/cits5501.github.io
CITS5501 website. Visit https://cits5501.github.io/ to view the website.
Language: HTML - Size: 47.6 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 19 - Forks: 4
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: 29 days ago - Pushed at: 10 months ago - Stars: 19 - Forks: 3
imandra-ai/reasonml-tic-tac-toe
Language: Reason - Size: 2.92 MB - Last synced at: 10 days ago - Pushed at: over 2 years ago - Stars: 19 - Forks: 1
will62794/snapshot-isolation-spec
A formal specification of snapshot isolation.
Language: TLA - Size: 78.1 KB - Last synced at: 2 months ago - Pushed at: 7 months ago - Stars: 18 - Forks: 2
Vanille-N/tree-borrows
Overview of the Tree Borrows rules for detecting violations of the aliasing discipline in Rust
Language: TeX - Size: 3.44 MB - Last synced at: about 1 year ago - Pushed at: about 1 year ago - Stars: 18 - Forks: 0
PROGNOSISTool/main
Code and resources for model learning of network protocol implementations
Language: Shell - Size: 59.3 MB - Last synced at: 7 months ago - Pushed at: over 1 year ago - Stars: 18 - Forks: 3
appliedfm/vstyle
A style guide for Coq
Size: 646 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 0
formalmethods/intrepid
Intrepyd Model Checker
Language: Python - Size: 147 MB - Last synced at: 17 days ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 1
black-sat/black
BLACK (Bounded Lᴛʟ sAtisfiability ChecKer)
Language: C++ - Size: 188 MB - Last synced at: 29 days ago - Pushed at: 29 days ago - Stars: 17 - Forks: 5
CuriousCI/software-engineering
Software Engineering course @ Sapienza Università di Roma
Language: Typst - Size: 6.68 MB - Last synced at: about 2 months ago - Pushed at: 3 months ago - Stars: 17 - 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: 3 months ago - Pushed at: over 1 year ago - Stars: 17 - Forks: 1
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: 29 days ago - Pushed at: 5 months ago - Stars: 15 - Forks: 1
tomooda/ViennaTalk
ViennaTalk, a LIVE IDE for VDM-SL based on Pharo Smalltalk
Language: Smalltalk - Size: 48.8 MB - Last synced at: 14 days ago - Pushed at: 14 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: about 1 month ago - Pushed at: about 2 months ago - Stars: 14 - Forks: 7
iwilare/formal-methods
Operational semantics, Type-based information flow security, Hoare logic, Verification conditions, and Separation logic in Agda for the IMP language
Language: Agda - Size: 32.2 KB - Last synced at: 10 months ago - Pushed at: almost 3 years ago - Stars: 14 - Forks: 1
jdnklau/fm-ml
Collection of resources for research concerning Machine Learning and Formal Methods.
Language: TeX - Size: 54.7 KB - Last synced at: over 2 years ago - Pushed at: over 3 years ago - Stars: 14 - Forks: 3
grayswandyr/electrod
Formal analysis for the Electrod formal specification language
Language: OCaml - Size: 2.51 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 13 - Forks: 4
symbolicsoft/noiseexplorer
Online engine for reasoning about the Noise Protocol Framework.
Language: Rust - Size: 49.7 MB - Last synced at: 10 days ago - Pushed at: 7 months ago - Stars: 13 - Forks: 6
Sophietje/Verification-Tool-Overview
Information about verification tools. Browse the data at https://slebok.github.io/proverb/
Language: Python - Size: 1.06 MB - Last synced at: almost 2 years ago - Pushed at: almost 2 years ago - Stars: 13 - Forks: 2
imandra-ai/cme-mdp
Imandra Modelling Language CME MDP Model
Language: Jupyter Notebook - Size: 2.17 MB - Last synced at: 2 months ago - Pushed at: about 5 years ago - Stars: 13 - Forks: 3
hengxin/tlaps-examples
Examples for TLAPS (TLA+ Proof System)
Language: TeX - Size: 4.76 MB - Last synced at: 3 months ago - Pushed at: about 5 years ago - Stars: 13 - Forks: 6
lean-machines-central/lean-machines
a Lean4 framework for the modeling and refinement of stateful systems
Language: Lean - Size: 738 KB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 12 - Forks: 2
se-buw/fm-playground
A Formal Method playground for limboole, Z3, nuXmv, Alloy, and Spectra
Language: TypeScript - Size: 104 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 12 - Forks: 2
maxvonhippel/AttackerSynthesis
🤖KORG: Tool, Models, and Supplementary Materials for Attacker Synthesis
Language: Python - Size: 1.65 MB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 12 - Forks: 1
vasilisp/inez
A Constraint Solver
Language: OCaml - Size: 519 KB - Last synced at: 25 days ago - Pushed at: over 9 years ago - Stars: 12 - Forks: 3
Kiguli/IMPaCT
IMPaCT: Interval MDP Parallel Construction for Controller Synthesis of Large-Scale Stochastic Systems. IMPaCT is an open-source software tool for the parallelized verification and controller synthesis of large-scale stochastic systems using interval Markov chains (IMCs) and interval Markov decision processes (IMDPs).
Language: C++ - Size: 21.9 MB - Last synced at: about 2 months ago - Pushed at: 6 months ago - Stars: 11 - Forks: 0
imandra-ai/ipl-examples
Imandra Protocol Language example models
Size: 117 KB - Last synced at: 3 months ago - Pushed at: 10 months ago - Stars: 11 - Forks: 1
timewinder-dev/timewinder-prototype
Temporal Logic of Actions Modeling for Python
Language: Python - Size: 176 KB - Last synced at: over 1 year ago - Pushed at: about 4 years ago - Stars: 11 - 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: 22 days ago - Pushed at: about 2 months ago - Stars: 10 - Forks: 8
tobias-rothmann/Polynomial-Commitment-Schemes
Formalizing Polynomial Commitment Schemes in the Interactive Theorem Prover Isabelle.
Language: Isabelle - Size: 4.16 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 10 - Forks: 0
