Yoichi Hirai

awesome-ethereum-virtual-machine. Ethereum Virtual Machine Awesome List

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

ethereum-formal-verification-overview. The start page about my efforts around smart contract verification

eth-isabelle. A Lem formalization of EVM and some Isabelle/HOL proofs

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

fp-ethereum. Functional Programming for Ethereum: Intro and Resources

evmverif. An EVM code verification framework in Coq

dry-analyzer. Dr. Y's Ethereum Contract Analyzer

vmtrace_visualizer. A program that annotates a vm trace with dataflow information

ethereum-word-list. Words are Hard: Defining Common Terms in the Ethereum / Crypto Space

gohantabeyo. 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.

cbc_casper. Isabelle formalization of binary consensus

record.

patchwork. social writing tool

neta. neta notes

rlp-ocaml. RLP serialization for OCaml

reasonable-manifesto. Reasonable Engineering Manifest

practice. JavaScript

sql2lisp. Verilog

kissdb-rust. kissdb ported to rust

verbose-code-reading. Verboselly Logged Code Reading

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

pieces_old. pieces: a fork from instiki.

kietter. kietter

surreal. surreal numbers in Coq

token_why3. A Why3 modelling of a token contract

proofmarket.

gitit. A wiki using HAppS, pandoc, and git

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

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

llrbtree. Left-leaning red-black trees

waitfree. A combinator library for asynchronous waitfree computation among forkIO threads.

smart-contract. slock smart contract written in solidity

bamboo-tests. Little prost to test bamboo contracts with mocha and web3js

bst. Binary search tree based on a logarithmic method

ethereum-formal-list. A list of formal method applications on smart contracts

CLTT. Verilog

htodo. a todo manager

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

taocp_in_coq. taocp_in_coq

yellowpaper. The "Yellow Paper": Ethereum's formal specification

notes. Some random notes

ConcurrentSet. Haskell

go-ethereum. Official golang implementation of the Ethereum protocol

thesis.

salary-nego. Salary negotiation app on the Nexus zkVM

game. combinatorial game

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

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