Zinc+ is a performance-oriented SNARK framework designed to handle computations across multiple mathematical domains without the "witness inflation" overhead typical of traditional arithmetization.

Implementation of the Clap language for ZK Circuits in the Lean proof-assistant

A lattice-based non-interactive folding scheme written in Rust

Epson Printer Configuration tool and waste ink counter resetter

articles, codes and tools all about zero-knowledge proofs

This is the repository for the Lean master program in Lyon for 2024-25

A resource for anyone interested in understanding and unlocking the potential of zk-SNARKs, from beginners to experts.

Executable formal model of the EVM and Yul in Lean 4.

Interactive formal verification tool for Yul programs

LLM101n: Let's build a Storyteller

Formal verification of zkSync's on-chain verifier using EasyCrypt.

Files associated with the course Interactive Theorem Proving at LMU SoSe 2024

Learn neovim

📜 Haskell course info, plan, video lectures, slides

Personal research notes

Game development blog.

A guide to build a simple Roguelike game with Godot engine.

Horus, a formal verification tool for StarkNet smart contracts.

Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024

Cairo compiler plugin extending language with annotations

Materials for the course "theorem prover lab: applications in programming languages" at KIT, SS2022 edition

Logic and Mechanized Reasoning

A web page with resources for teaching with formal methods and tools.

The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…