ldv-klever/klever

Read-only mirror of the Klever Git repository

Language: Python - Size: 162 MB - Last synced at: about 3 hours ago - Pushed at: about 4 hours ago - Stars: 22 - Forks: 14

ultimate-pa/ultimate

The Ultimate program analysis framework.

Language: Java - Size: 876 MB - Last synced at: about 12 hours ago - Pushed at: about 12 hours ago - Stars: 221 - Forks: 46

tlaplus/vscode-tlaplus

TLA+ language support for Visual Studio Code

Language: TypeScript - Size: 22.7 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 382 - Forks: 42

lip6/ITSTools

A multi-formalism, multi-solution model-checker centered on the language GAL

Language: Python - Size: 506 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 25 - Forks: 12

harmonylang/harmony

A Python-like programming language for testing and experimenting with concurrent programs.

Language: Python - Size: 87 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 18 - Forks: 6

apalache-mc/apalache

APALACHE: symbolic model checker for TLA+ and Quint

Language: Scala - Size: 62.3 MB - Last synced at: about 22 hours ago - Pushed at: about 1 month ago - Stars: 468 - Forks: 44

nas120r/tla-ai-amplifier

Explore the TLA+ AI Amplifier repository to see how AI tools can enhance formal specification development and verification. 🛠️ Discover examples like a race condition counter and a producer-consumer queue, complete with TLA+ specs and Python implementations. 💻

Language: TLA - Size: 27.3 KB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 0 - Forks: 0

mCRL2org/mCRL2

The Git repository for the mCRL2 toolset.

Language: C++ - Size: 102 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 98 - Forks: 42

tlaplus/tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

Language: Java - Size: 139 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 2,449 - Forks: 216

model-checking/kani

Kani Rust Verifier

Language: Rust - Size: 32.6 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 2,570 - Forks: 118

gipsyh/rIC3

Hardware Formal Verification Tool

Language: Rust - Size: 1.94 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 52 - Forks: 11

p-org/P

The P programming language.

Language: C# - Size: 153 MB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 3,367 - Forks: 197

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: 769 KB - Last synced at: 6 days ago - Pushed at: 7 days ago - Stars: 4 - Forks: 0

moves-rwth/storm

A Modern Probabilistic Model Checker

Language: C++ - Size: 195 MB - Last synced at: 7 days ago - Pushed at: 7 days ago - Stars: 147 - Forks: 81

aygp-dr/tla-ai-amplifier

TLA+ examples demonstrating AI-assisted formal specification development, model checking, and verification processes

Language: TLA - Size: 25.4 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 0 - Forks: 0

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

aygp-dr/tla-etaps-2025

Resources and materials for the TLA+ Community Event at ETAPS 2025

Language: Makefile - Size: 9.77 KB - Last synced at: 8 days ago - Pushed at: 8 days ago - Stars: 0 - Forks: 0

spacejam/tla-rust

writing correct lock-free and distributed stateful systems in Rust, assisted by TLA+

Language: TLA - Size: 728 KB - Last synced at: 5 days ago - Pushed at: about 8 years ago - Stars: 1,054 - Forks: 27

ftsrg/theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms

Language: Java - Size: 547 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 52 - Forks: 45

informalsystems/modelator

Model-based testing tool

Language: Python - Size: 334 MB - Last synced at: 5 days ago - Pushed at: 3 months ago - Stars: 59 - Forks: 5

hlisdero/cargo-check-deadlock

Find deadlocks in Rust code with Petri net model checking

Language: Rust - Size: 1.82 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 29 - Forks: 0

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,286 - Forks: 407

Calvin-L/ezpsl

The easy parallel algorithm specification language

Language: Haskell - Size: 344 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 4 - Forks: 1

cristian-mattarei/CoSA

CoreIR Symbolic Analyzer

Language: Python - Size: 7.98 MB - Last synced at: about 20 hours ago - Pushed at: over 4 years ago - Stars: 73 - Forks: 18

nicolasAmat/SMPT

SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).

Language: Python - Size: 8.98 MB - Last synced at: 14 days ago - Pushed at: 15 days ago - Stars: 27 - Forks: 5

will62794/spectacle

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

Language: JavaScript - Size: 28.6 MB - Last synced at: 17 days ago - Pushed at: 17 days ago - Stars: 125 - Forks: 9

vtramo/rtl-mc

Model Checking Linear Temporal Properties on Polyhedral Systems - Master's Thesis in Computer Science

Language: C++ - Size: 40 MB - Last synced at: 11 days ago - Pushed at: 18 days ago - Stars: 0 - Forks: 0

johnyf/tool_lists

Links to tools by subject

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

seahorn/seahorn

SeaHorn Verification Framework

Language: C - Size: 7.46 MB - Last synced at: 19 days ago - Pushed at: 21 days ago - Stars: 451 - Forks: 131

sp-muramutsa/knights

A knowledge-based system solving Knights and Knaves puzzles using propositional logic and model checking to demonstrate AI concepts like symbolic reasoning and knowledge representation.

Language: Python - Size: 10.7 KB - Last synced at: 19 days ago - Pushed at: 19 days ago - Stars: 0 - Forks: 0

sybila/biodivine-hctl-model-checker

Symbolic HCTL model checker for Boolean networks

Language: Rust - Size: 860 KB - Last synced at: 26 days ago - Pushed at: 26 days ago - Stars: 0 - Forks: 0

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs

Language: Scala - Size: 139 MB - Last synced at: 11 days ago - Pushed at: about 1 month ago - Stars: 375 - Forks: 56

Metroidzeta/Model-Checker-CTL

Model Checker CTL (simple) en Java, que j'ai réalisé en M2 Informatique parcours Programmation et Logiciels Sûrs

Language: Java - Size: 76.2 KB - Last synced at: 26 days ago - Pushed at: 26 days ago - Stars: 0 - Forks: 0

AliveToolkit/alive2

Automatic verification of LLVM optimizations

Language: C++ - Size: 6.32 MB - Last synced at: 26 days ago - Pushed at: about 1 month ago - Stars: 905 - Forks: 116

bigraph-toolkit-suite/bigraphs.bigraph-framework

A framework written in Java for the creation and simulation of bigraphs.

Language: Java - Size: 64.5 MB - Last synced at: 18 days ago - Pushed at: 18 days ago - Stars: 2 - Forks: 0

benkeks/equivalence-fiddle

Tool for finding the best ways of equating / preordering / distinguishing finite process models.

Language: Scala - Size: 11.5 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 4 - Forks: 1

florentdelgrange/synthesis_from_drl

Composing reinforcement learning policies, with formal guarantees

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

firmai/datagene

DataGene - Identify How Similar TS Datasets Are to One Another (by @firmai)

Language: Jupyter Notebook - Size: 1.12 MB - Last synced at: 7 days ago - Pushed at: over 3 years ago - Stars: 204 - Forks: 24

vincenzoml/VoxLogicA

VoxLogicA: the "Voxel-based Logical Analyser", is an interpreter of a declarative language, inspired by spatial logics, to analyse images in a simple way. See also http://www.voxlogica.org .

Size: 256 MB - Last synced at: 28 days ago - Pushed at: 28 days ago - Stars: 15 - Forks: 4

kelvich/tlaplus_jupyter

Jupyter kernel for TLA⁺

Language: Python - Size: 78.1 KB - Last synced at: 8 days ago - Pushed at: almost 3 years ago - Stars: 120 - Forks: 8

probing-lab/HyperPAYNT

Synthesizing controllers for Probabilistic HyperProperties on MDPs.

Language: C++ - Size: 144 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

ticktac-project/tchecker

TChecker is an open-source verification tool for timed automata

Language: C++ - Size: 24.5 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 21 - Forks: 20

moves-rwth/prophesy 📦

Parameter Synthesis in Markov Models

Language: Python - Size: 71.1 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 3

SmnTin/lincheck

A linearizability checker for concurrent data structures

Language: Rust - Size: 67.4 KB - Last synced at: 7 days ago - Pushed at: almost 2 years ago - Stars: 12 - Forks: 1

mrigankpawagi/LeanearTemporalLogic

Formalization of Linear Temporal Logic (LTL) in Lean 4.

Language: Lean - Size: 167 KB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

model-checking/cbmc-starter-kit

The CBMC starter kit makes it easy to add CBMC verification to a software project.

Language: Python - Size: 1.42 MB - Last synced at: 13 days ago - Pushed at: 4 months ago - Stars: 46 - Forks: 22

parapluu/Concuerror

Concuerror is a stateless model checking tool for Erlang programs.

Language: Erlang - Size: 10.5 MB - Last synced at: 26 days ago - Pushed at: about 2 months ago - Stars: 338 - Forks: 43

mryndzionek/tlaplus_specs

Different TLA+ specifications, mostly for learning purposes

Language: TLA - Size: 161 MB - Last synced at: 18 days ago - Pushed at: about 1 year ago - Stars: 32 - Forks: 1

lip6/libITS

Core Guarded Action Language and Instantiable Transition System semantics using libDDD.

Language: C++ - Size: 180 MB - Last synced at: about 2 months ago - Pushed at: 2 months ago - Stars: 8 - Forks: 5

Smattr/rumur

yet another model checker

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

lemmy/BlockingQueue

Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history!

Language: TLA - Size: 18.3 MB - Last synced at: 16 days ago - Pushed at: 8 months ago - Stars: 492 - Forks: 23

jens-classen/vergo

Vergo: A Verification System for GOLOG Programs

Language: Prolog - Size: 805 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 4 - Forks: 1

JJWRoeloffs/minictl

A small model checker for Computational Tree Logic

Language: Rust - Size: 128 KB - Last synced at: about 21 hours ago - Pushed at: 2 months ago - Stars: 1 - Forks: 1

informalsystems/modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.

Language: Python - Size: 68.7 MB - Last synced at: 12 days ago - Pushed at: over 2 years ago - Stars: 28 - Forks: 3

marcusm117/mctk

Python Package Model Checking Toolkit

Language: Python - Size: 2.74 MB - Last synced at: 11 days ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 0

thomasp85/lime

Local Interpretable Model-Agnostic Explanations (R port of original Python package)

Language: R - Size: 10.6 MB - Last synced at: 18 days ago - Pushed at: almost 3 years ago - Stars: 484 - Forks: 109

jrclogic/SMCDEL

A symbolic model checker for Dynamic Epistemic Logic.

Language: Haskell - Size: 14.2 MB - Last synced at: about 1 month ago - Pushed at: 4 months ago - Stars: 46 - Forks: 9

s12f/tlads

TLA+ and Distributed/Discrete Systems.

Language: TLA - Size: 82 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 3 - Forks: 0

sbu-fsl/Metis

Metis: File System Model Checking via Versatile Input and State Exploration (FAST '24)

Language: C - Size: 5.03 MB - Last synced at: about 2 months ago - Pushed at: 3 months ago - Stars: 12 - Forks: 3

Benestar/rust-model-checker

A Model Checker in Rust

Language: Rust - Size: 43.9 KB - Last synced at: 3 months ago - Pushed at: 4 months ago - Stars: 4 - 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: 4 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

ArtZaragozaGitHub/ML--P2_Predicting_Loan_Purchases

Anticipating Loan-Eligible Bank Customers with a High Probability of Successfully Purchasing a Bank Loan.

Language: Jupyter Notebook - Size: 1.49 MB - Last synced at: 4 days ago - Pushed at: 4 months 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: 4 months ago - Pushed at: 4 months ago - Stars: 76 - Forks: 20

Gy-Hu/pyBMC

Implementation of bounded model checking with Z3py. (AIGER1.0 support)

Language: Python - Size: 104 MB - Last synced at: 6 days ago - Pushed at: almost 2 years ago - Stars: 9 - Forks: 0

johnwickerson/memalloy

Memory consistency modelling using Alloy

Language: OCaml - Size: 4.99 MB - Last synced at: 6 days ago - Pushed at: over 4 years ago - Stars: 29 - Forks: 6

montao/formal-verification

🌍 The SMV models

Language: Matlab - Size: 22.5 KB - Last synced at: 14 days ago - Pushed at: about 8 years ago - Stars: 1 - Forks: 0

jayhorn/jayhorn

Static checker for Java

Language: Java - Size: 180 MB - Last synced at: 4 months ago - Pushed at: 5 months ago - Stars: 85 - Forks: 23

huffyhenry/ltl24

An experimental verification and querying language for F24 football data

Language: Haskell - Size: 74.2 KB - Last synced at: about 3 hours ago - Pushed at: over 8 years ago - Stars: 7 - Forks: 0

imitator-model-checker/imitator

IMITATOR is a parametric timed model checker taking as input extensions of parametric timed automata, and synthesizing parameter valuations for safety properties and more.

Language: OCaml - Size: 50.6 MB - Last synced at: about 24 hours ago - Pushed at: 21 days ago - Stars: 28 - Forks: 14

tlaplus/azure-cosmos-tla Fork of Azure/azure-cosmos-tla

Azure Cosmos TLA+ specifications

Language: TLA - Size: 1.28 MB - Last synced at: 3 months ago - Pushed at: 5 months ago - Stars: 21 - Forks: 5

systems-group/anysystem

A framework for deterministic simulation and testing of distributed systems

Language: Rust - Size: 315 KB - Last synced at: 17 days ago - Pushed at: 8 months ago - Stars: 5 - Forks: 0

FedericoPonzi/tlaplus-wiki 📦

Moved to dokuwiki: https://docs.tlapl.us

Language: CSS - Size: 852 KB - Last synced at: 3 months ago - Pushed at: 9 months ago - Stars: 1 - Forks: 0

andreamanini98/TABEC

Tool for creating Timed Automata and checking their language emptiness.

Language: C++ - Size: 6.05 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

eLyKseeR/modelling

modelling effort

Language: Coq - Size: 988 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

fadoss/umaudemc

Unified Maude model-checking tool

Language: Python - Size: 273 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 9 - Forks: 1

will62794/tlaplus_repl

A simple REPL for TLA+.

Language: Python - Size: 21.5 KB - Last synced at: 3 months ago - Pushed at: over 1 year ago - Stars: 40 - Forks: 2

Rapfff/jajapy

Baum-Welch for all kind of Markov models

Language: Python - Size: 8.23 MB - Last synced at: 2 months ago - Pushed at: about 1 year ago - Stars: 21 - Forks: 2

github/deli 📦

Language: Haskell - Size: 48.8 KB - Last synced at: 5 months ago - Pushed at: over 4 years ago - Stars: 167 - Forks: 9

lou1306/pyxmv

(Unofficial) Python interface to nuXmv

Language: Python - Size: 121 KB - Last synced at: about 2 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

mell-o-tron/DEL-Model-Checker

DEL Model Checker

Language: JavaScript - Size: 19.7 MB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 0 - Forks: 0

formalmethods/intrepid

Intrepyd Model Checker

Language: Python - Size: 147 MB - Last synced at: 28 days ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 1

vincent-hugot/nfalib

NFA framework for INSA-CVL 4A class on Verification / Model-Checking

Language: Python - Size: 367 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 5 - Forks: 5

nclarius/pyPL

Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions

Language: Python - Size: 6.22 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 19 - Forks: 2

florentdelgrange/vae_mdp

Implementation of Variational Markov Decision Processes, a framework allowing to (i) distill policies learned through (deep) reinforcement learning and (ii) learn discrete abstractions of continuous environments, the two with bisimulation guarantees.

Language: Jupyter Notebook - Size: 236 MB - Last synced at: about 19 hours ago - Pushed at: almost 3 years ago - Stars: 5 - Forks: 2

dalzilio/mcc

High-Level Nets Blaster for the Model-Checking Contest

Language: Go - Size: 1.18 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 10 - Forks: 1

AliAtaollahi/Solidity2mCRL2-Compiler-Project

A compiler developed using ANTLR in Java that translates Solidity smart contracts into mCRL2 models

Language: Java - Size: 18.7 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 11 - Forks: 0

y-taka-23/ddsv-go

A toy deadlock detector written in Go. 🔍

Language: Go - Size: 428 KB - Last synced at: 2 months ago - Pushed at: about 5 years ago - Stars: 30 - Forks: 2

DrHAMDANE/TransformationAADL2timedAutomata

We propose in this work an approach for the verification of the AADL (Architecture and Analysis Design Language) description. This approach is based in Model Driven Engineering (MDE) and assisted by a toolchain. Indeed, we define a source meta-model for AADL and a target meta-model for the timed automata formalism; we define a transformation process in two steps : the first is aModel2Model transformation which takes an AADLModel and produces the corresponding timed automata model. The second transformation is a Model2Text transformation which takes a timed automata model and generates a text in ta-format code. This code is accepted by the Uppaal toolbox. The goal of this effort is to insure some properties of AADL models using the Uppaal model checker. A case study has been developed to show the feasibility and validity of the proposed approach.

Language: Assembly - Size: 292 KB - Last synced at: 24 days ago - Pushed at: almost 4 years ago - Stars: 8 - Forks: 0

paultristanwagner/model-checking

Command line tool for model checking using LTL, CTL and CTL* formulas

Language: Java - Size: 562 KB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 10 - Forks: 0

Blacksujit/Suraksha

Welcome to the **SURAKSHA -- Secure Document Query Application**! This powerful tool allows you to securely upload, search, and analyze documents with ease. Built using Streamlit, this app offers an intuitive interface and various features for managing your document queries efficiently.

Language: Python - Size: 14.9 MB - Last synced at: 3 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 0

labs-lang/sliver

The SLiVER LAbS VERifier

Language: Python - Size: 40.7 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 0 - Forks: 0

xlauko/lart

LLVM Abstraction & Refinement Tool. The goal of this tool is to provide LLVM-to-LLVM transformations that implement various program abstractions. In terms of the instruction set, the resulting programs are normal, concrete LLVM programs that can be executed and analyzed.

Language: C++ - Size: 1.06 MB - Last synced at: 2 months ago - Pushed at: over 2 years ago - Stars: 19 - Forks: 2

janislley/LSVerifier

LSVerifier - Large Systems Verifier

Language: Python - Size: 22.4 MB - Last synced at: 3 days ago - Pushed at: about 1 year ago - Stars: 11 - Forks: 3

fluentverification/stamina-storm

STAMINA - the STochiastic Approximate Model-checker for INfinite-state Analysis, integrated with the Storm model checking engine.

Language: C++ - Size: 2.1 MB - Last synced at: 6 months ago - Pushed at: 8 months ago - Stars: 5 - Forks: 2

m4lvin/mchlpe

🕵️🤥 A Model Checker for the Hardest Logic Puzzle Ever

Language: Haskell - Size: 370 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 5 - Forks: 0

draeger-lab/ModelPolisher

ModelPolisher accesses the BiGG Models knowledgebase to annotate SBML models.

Language: Java - Size: 63.8 MB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 23 - Forks: 7

utwente-fmt/ltsmin

The LTSmin model checking toolset

Language: C - Size: 7.43 MB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 52 - Forks: 30

inbo/inlatools

An R package with useful functions to diagnose INLA models

Language: R - Size: 7.65 MB - Last synced at: about 2 months ago - Pushed at: 9 months ago - Stars: 4 - Forks: 2

fadoss/maudesmc

Model checker for Maude systems controlled by strategies

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

amamory-verification/hw-formal-verif

Hardware Formal Verification

Language: Verilog - Size: 3.74 MB - Last synced at: about 21 hours ago - Pushed at: almost 5 years ago - Stars: 15 - Forks: 3