A template repository with an example of using Veil verifier as a Lean library.

Reimplementing some data structures from Iris in Lean

A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.

Bindings to libclingo for the lean4 prover and programming language!

Formalisation of basic IO-Automata theory in Isabelle/HOL

Emacs Major mode for Rhombus (experimental)

A stateless trustless Starknet light client in Rust 🦀

Harmony automation tool available through program optimization (e-graphs)

Synthesis of Heap-Manipulating Programs from Separation Logic

Synthesis of Heap-Manipulating Programs from Separation Logic

WebAssembly Demo

iNaturalist iOS app

List of bugs found in distributed protocols

An overview of property-based testing functionality

A beautiful, simple, clean, and responsive Jekyll theme for academics

An IntelliJ plugin to run Infer and display its results

A library providing mechanized proofs of the LibraBFT consensus using the Coq theorem prover

QuickCheck inspired property-based testing for OCaml.

A Coq formalization of information theory and linear error-correcting codes

Monadic effects and equational reasonig in Coq

A minimalistic blockchain consensus implemented and verified in Coq

A minimalistic blockchain consensus implemented and verified in Coq

Haskell? More like not-prooved-well! Got-em!

Partial Commutative Monoids

A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems

Solving bin packing visually

Mathematical Components (the Book)