47 Open source projects that are alternatives of or similar to tutoriel_wp

Read-only mirror of the Klever Git repository

Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on

Legacy code connected to the high-assurance implementation of the Ouroboros protocol family

www.imandra.ai

Fully proved small C functions (examples for verification course).

The Verifiably Safe Reinforcement Learning Framework

Intrepyd Model Checker

The Overture Tool

A framework for implementing and certifying impure computations in Coq

Jupyter notebooks for tutorial on the Z3 SMT solver

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.

TLA+ specs and models for the TezEdge node's p2p overlay network, shell, and consensus

Synthesis of Heap-Manipulating Programs from Separation Logic

Reads a state transition system and performs property checking

Trying to verify Verilog/VHDL designs with formal methods and tools

Formal semantics of LLVM IR in K

Automated Schedule Generation for Time-Sensitive Networks (TSN).

A tool for Model Based Testing

An Eclipse-based modeling framework for the component-based design and analysis of reactive systems

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

Source code for the equivalence checker presented in the PLDI 2019 paper, "Semantic Program Alignment for Equivalence Checking"

generative programming & verification

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

Formalization of Tendermint proposer election properties

A core language for rule-based hardware design 🦑

Algebraic proof discovery in Agda

A modular sat/smt solver with proof output.

Experimental Smart Contracts In Plutus.

Verification framework and tool for higher-order Scala programs

ACL2 System and Books as Maintained by the Community

Software Quality Wiki

TLA+ language support for Visual Studio Code

SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada

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

High-assurance implementation of the Ouroboros protocol family

A Coq-based synthesis of Scala programs which are correct-by-construction

CoreIR Symbolic Analyzer

Lean mathematical components library

Meaningful control of data in distributed systems.

the champagne of beta embedded databases

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

Links to tools by subject

Z-EVES for linux. Probably the only place you can find it

TLA+ language support for Visual Studio Code

Awesome ASIC design verification

A cryptographic library in SPARK 2014

Example implementation of Arm's Architecture Specification Language (ASL)