simple web service in lean4

The "batteries included" extended library for the Lean programming language and theorem prover

The Lean version manager

CakeML: A Verified Implementation of ML

Rocq plugin embedding Elpi

A project to digitalise results from physics into Lean.

A secure embedded operating system for microcontrollers

Proof assistant based on the λΠ-calculus modulo rewriting

Lean documentation authoring tool

A template for blueprint-driven formalization projects in Lean.

Repository hosting the resources for the conference "ItaLean 2025", held in Bologna, Italy, December 9–12, 2025.

An introduction to theorem proving in Lean for the impatient.

LLM verified with Monte Carlo Tree Search

Proving leftpad correct two-dozen different ways

Multiparty Session Types in OCaml

🦀 Small exercises to get you used to reading and writing Rust code!

Raiden Network Smart Contracts

Ethereum smart contract fuzzer

A Ruby implementation of Ethereum.

OCaml DSL for verifiable computation

A Lem formalization of EVM and some Isabelle/HOL proofs

A curated list of academic blockchain-related papers

📚 A curated collection of links for cryptoeconomists

A Lem formalization of EVM and some Isabelle/HOL proofs

An Analysis Tool for Smart Contracts

K Semantics of the Ethereum Virtual Machine (EVM)

Preview GitHub README.md files locally before committing them.

Elliptic curve library secp256k1 wrapper for Ocaml