Yoichi Hirai

Reasonable Engineering Manifest

Ethereum Virtual Machine Awesome List

Bamboo see https://github.com/cornellblockchain/bamboo

The start page about my efforts around smart contract verification

A Lem formalization of EVM and some Isabelle/HOL proofs

Coq to Rust program extraction. The whole tree is on the original Coq code base.

Functional Programming for Ethereum: Intro and Resources

An EVM code verification framework in Coq

Dr. Y's Ethereum Contract Analyzer

A program that annotates a vm trace with dataflow information

Words are Hard: Defining Common Terms in the Ethereum / Crypto Space

Gohantabeyo is a web site where people can make a wish whom they want to eat out with. If the other makes a similar wish, their wishes are told to both.

Isabelle formalization of binary consensus

social writing tool

No description.

neta notes

RLP serialization for OCaml

No description.

kissdb ported to rust

No description.

Verboselly Logged Code Reading

An auth module to provide drop-in session capability with Happstack.

A wiki using HAppS, pandoc, and git

script.aculo.us is an open-source JavaScript framework for visual effects and interface behaviours.

pieces: a fork from instiki.

surreal numbers in Coq

A Why3 modelling of a token contract

No description.

kietter

a fork of http://js-graph-it.sourceforge.net/

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

TODO waits for TODO on Tracks, a GTD(TM) web application, built with Ruby on Rails

Salary negotiation app on the Nexus zkVM

No description.

Little prost to test bamboo contracts with mocha and web3js

Official golang implementation of the Ethereum protocol

Main public package repository for OPAM, the source package manager of OCaml.

A list of formal method applications on smart contracts

The "Yellow Paper": Ethereum's formal specification

Some random notes

slock smart contract written in solidity

A combinator library for asynchronous waitfree computation among forkIO threads.

a todo manager

undecidability club's web page

No description.

No description.

combinatorial game

taocp_in_coq

No description.

Specification for the Execution Layer. Tracking network upgrades.

No description.

🐤 Less permission fatigue, more momentum. Dippy knows what’s safe to run and keeps Claude on track when plans change.

Rust language proof-carrying data framework

A computable model of Polynomials in Lean.

No description.

Lean 4 programming language and theorem prover

The math library of Lean 4

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

Lean 4 port of Iris, a higher-order concurrent separation logic framework

A minimal development of SSA theory

No description.

Make your zero-knowledge circuits safe with formal verification! 🍀

Formalization of C++ for verification purposes.

A randomized activity picker for your 5 minites

The Truffle Framework Website

The Solidity Contract-Oriented Programming Language

Lean circuit DSL

Modern and minimalistic blog theme.

No description.

No description.

Standard library for OCaml

No description.

Taskwarrior - Commandline Task Management

No description.

A simple ERC-20 compatible token contract written in Rust compiled into WebAssembly

pwasm-test is a set of tools to make it easy to test internal logic of contracts written using pwasm-std

WASM contracts standard library for Rust

Parity WASM Abi (Legacy and new)

Parity deployment script.

Fast, light, robust Ethereum implementation

K Framework Tools 5.0

New experimental programming language

No description.

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

A formal verifier and analysis tool for Solidity Smart Contracts

A collection of scripts used to bootstrap a test raiden envirnoment. (gist is harder to update)

Raiden Network Smart Contracts

Development of the Raiden Monitoring and Pathfinding Services

Ethereum fuzz testing framework

Spec of the Raiden Network protocol

Raiden Network

Useful tools for Raiden and Auxiliary services

Raiden monitoring service

Repo for the Raiden Pathfinding Service

a sample for checking github features

Ethereum end-to-end test harness

Bitcoin Core integration/staging tree

A bin for all the contracts we do

Certifier Website

An ACL2 formalization of the Ethereum VM, aiming to be both executable and suitable for proving interesting properties of EVM contracts.

Implementations for registrars and local resolvers for the Ethereum Name Service

No description.

The Ethereum Improvement Proposal

OCaml DSL for verifiable computation

K Semantics of the Ethereum Virtual Machine (EVM)

One consensus test generator

No description.

No description.

No description.

Optimized C library for EC operations on curve secp256k1

A skeleton dapp

A Dutch auction crowdsale dapp

simple bridge between ethereum foundation and kovan networks

A dapp for the operations proxy contract

Homebrew tap for ethcore

Test dapp

Rust JSON-RPC implementation

No description.

Pre-compiled JS files for the Parity UI. Automatically populated from CI.

JS interface definitions for all rpc methods supported by parity

JS interface library for the Ledger

JS interface to the ShapeShift APIs

The Reactive Bond API

Bond API for use with Parity

WebAssembly serialization/deserialization in rust

The Bond API.

No description.

Ethereum transaction scheduler service.

Parity Chrome Extension

The Bond-based Parity Reactive UI library

JS library for interfacing to etherscan.io

JS shared non-ui components for the Parity wallet and dapps

Shared UI components for the Parity wallet & dapps

Signer plugin for Parity accounts

Signer plugin for hardware devices

Default Signer plugin, keyfile handling

Signer plugin to handle QR codes

Dapp to manage Parity Vaults

Dapp for the Parity default addressbook view

Dapp for Parity default address info view

Dapp for interacting with a contract

Dapp for viewing a list of available contracts

Dapp for managing the accounts visible to dapps

Dapp to manage the methods/permissions available to all dapps

Dapp to select the visible dapps (available from the network) in Parity

Dapp for contract development

A dapp for loading other dapps via embedded frame

JS Parity ABI library, part of parity.js

Dapp for an overview page for Parity

Dapp for managing Parity settings

Dapp for viewing the Parity node status

Dapp for interacting with multisig wallets

Dapp for doing a simple base contract deployment to a new chain

A JavaScript console Dapp

Dapp for registering Dapps with the registry

Dapp for interfacing with the GitHub Hint registry

Dapp for viewing the local transaction queue

Dapp for interfacing with the Registry contract

Dapp for interacting with the method signature registry

A basic token deployment dapp

The Parity Bitcoin client

Dapp for interacting with the Token registry

JS Promise-based API library for interfacing with Ethereum over RPC, part of parity.js

No description.

Rust bindings for the libusb library.

SMS verification for Parity.

No description.

Elliptic curve library secp256k1 wrapper for Ocaml

Light library to deal with RPCs in OCaml

No description.

No description.

Common tests for all Ethereum implementations

A library of cryptographic primitives (ciphers, hashes, etc) for OCaml

The Ethereum Wiki -

Casper contract, daemon and related software and tests

No description.

Ethereum Foundation website

Refu language

A Solidity subset with random program generator

Luck -- A Language for Property-Based Generators

truffle practice

No description.

swarm documentation

Generates a random Solidity code that should compile

No description.

Formalization of EVM in Coq

Ethereum C++ client

Mist browser

THE CONSTITUTION OF JAPAN (by Japanese)

The DAO smart contracts

Main-Website

No description.

a repository just for wiki

Learn Rust with practical examples

A Yesod application that shows the current price of one hash in bitcoin mining.

diary

ATS言語に関する文書の日本語訳置き場

A simple pair of rust programs that writes to and read from a file.

PIrapira port management daemon.

Exercises with crowd-sourced code reviews. The gem repo is at http://github.com/kytrinyx/exercism