SP1 is a zero‑knowledge virtual machine that proves the correct execution of programs compiled for the RISC-V architecture.

A Web3Signer-compatible Ethereum consensus remote signer in Bend 2, with proved slashing-protection laws

Quick Merkle Database

Bend 2: a fast language that blocks AI mistakes via proof. Install: curl -fsSL https://bend-lang.com/install.sh | sh

Minimal zkVM for Ethereum.

Reference implementation of Ethereum SSZ serialization and Merkleization

Age of Sigmar 4th

An external lean checker with a proof of consistency

Your gateway to the ethPandaOps ecosystem

Agent skill: make LLMs write docs in ASD-STE100 Simplified Technical

Minimal-allocation delta encoding for Ethereum beacon state. ~900KB for 32 epochs of mainnet history.

A verified nftables bytecode compiler

A static verifier for Rust, based on the Viper verification infrastructure.

Analyze Rust crates without touching compiler internals

A Lean 4 implementation of the Ethereum consensus specification for the Fulu, Gloas, Heze forks.

Standalone Rust toolkit for Ethereum ERA files — read, write, verify, and convert historical chain archives across clients.

Python CLI tool for CPU and memory profiling of the Lighthouse consensus client

Verification infrastructure for the Isabelle/HOL interactive proof assistant

a simple, fast memory allocator

A simple in memory tui for analyzing traces locally

Free and open-source iOS device manager for macOS. Browse backups, export messages, extract photos, manage apps - no subscriptions, no iCloud lock-in.

Prove functional correctness of Ethereum smart contracts in higher-order logic

consensus client

Verified Optimizing Compiler for Cryptographic Primitives