Pinned Repositories
erc4626-tests
ERC4626 Property Tests
halmos
A symbolic testing tool for EVM smart contracts
beacon-chain-spec
Formalization of the Beacon Chain Phase 0 Specification in K
evm-disassembler
EVM ByteCode To Opcode Disassembler
jsaf
Forked from http://safe.kaist.ac.kr
verified-smart-contracts
Smart contracts which are formally verified
javascript-semantics
KJS: A Complete Formal Semantics of JavaScript
vyper-semantics
KVyper: Semantics of Vyper in K
deposit-contract-verification
verified-smart-contracts
Smart contracts which are formally verified
daejunpark's Repositories
daejunpark/evm-disassembler
EVM ByteCode To Opcode Disassembler
daejunpark/jsaf
Forked from http://safe.kaist.ac.kr
daejunpark/verified-smart-contracts
Smart contracts which are formally verified
daejunpark/beacon-chain-spec
Formalization of the Beacon Chain Phase 0 Specification in K
daejunpark/beacon-chain-verification
daejunpark/c-semantics
Semantics of C in K
daejunpark/daejunpark.github.io
https://daejunpark.github.io
daejunpark/deposit-contract-verification
daejunpark/ERC721A
https://ERC721A.org
daejunpark/erc777-semantics
daejunpark/halmos-solady
Formally verifying consistency between Solmate and Solady using Halmos
daejunpark/helios
A fast, secure, and portable light client for Ethereum
daejunpark/java-semantics
The semantics of Java in K
daejunpark/javascript-semantics
KJS: A Complete Formal Semantics of JavaScript
daejunpark/jsaf-bin
Binary distribution of https://github.com/daejunpark/jsaf.git
daejunpark/michelson-semantics
A K semantics of Tezos' Michelson language.
daejunpark/morpho-data-structures
Data structures tested and used by the Morpho Protocol.
daejunpark/multicaller
Efficient multicaller contracts
daejunpark/npi
Artifact for the paper "Invariant Synthesis for Incomplete Verification Engines" in TACAS'18
daejunpark/openzeppelin-contracts
OpenZeppelin Contracts is a library for secure smart contract development.
daejunpark/revenue-distribution-token
Token to distribute aggregated vested earnings of any underlying token using the ERC-4626 standard.
daejunpark/rv-publications
Publications of Runtime Verification, Inc.
daejunpark/SecureML
daejunpark/solmate
Modern, opinionated, and gas optimized building blocks for smart contract development.
daejunpark/sound-protocol
daejunpark/VCDryad
VCDryad description
daejunpark/verisol
A formal verifier and analysis tool for Solidity Smart Contracts
daejunpark/vyper-semantics
KVyper: Semantics of Vyper in K
daejunpark/yield-daddy
ERC-4626 wrappers for common yield-generating platforms