JoranHonig

👷 What I work on

• tree-sitter-solidity
• Vertigo
• Mythril

⬅ Shift Left

• IBM Research - Relative cost of fixing defects
• BCM - What is shift left?

🔧 Early & Mid Stage | Analysis Tools

JoranHonig

pragma solidity ^0.6.0;

///#invariant unchecked_sum(_balances) == _totalSupply;
///#if_succeeds unchecked_sum(_balances) == old(unchecked_sum(_balances)) || msg.sig == bytes4(0x00000000);
contract AnnotatedToken {
  uint256 private _totalSupply;
  mapping (address => uint256) private _balances;
  mapping (address => mapping (address => uint256)) private _allowances;

  constructor() public {