Firefly
Firefly is a set of quality assurance tools for Ethereum smart contracts aimed to help developers before the audit and formal verification stages
ERC20 Token Verifier
Check your token’s full functional compliance with the ERC20 standard (the approve, transfer and transferFrom functions), before deploying it on mainnet
Blockchain Advisory Services
Receive targeted advice from an RV senior engineer on the verification topic of your choice: smart contracts, tokens, protocols, or virtual machines
Smart Contract Verification
Prove the correctness of smart contracts compiled for the Ethereum and Cardano virtual machines
Protocol Verification
Increase confidence in the correctness and security of the decentralized system powered by your protocol
IELE
IELE is a virtual machine (VM) for smart contracts, an evolutionary step beyond the Ethereum Virtual Machine (EVM)
K lets you design the formal semantics of your programming language in a modular and intuitive way, then uses the semantics to generate a suite of language tools including a parser, execution engine, symbolic execution engine, state-space explorer, and even a program verifier.
Read moreThe K Team was started in 2003. K has been continuously developed since then, with the center of the community being the FSL research group at the University of Illinois in Urbana-Champaign, USA.
Visit the community