anvacaru

INTRO
------
Hi, everyone, I am Andrei Vacaru, I am a K developer at Runtime Verification Inc, and today I will talk about how to do Smart Contract Verification. I will be using KEVM which is a K implementation of the EVM, fully faithfull with other implementations and it is also a K formal semantics, which means that we can use it to do formal verification of ethereum programs. 

 Real quick, We are RV, we are a formal methods company, we have serviced automotive and aerospace companies in the past with our services, now we are focused mostly on blockchain clients, our general mission is to improve basically the state of security and correctes n code across the board.

K - is a mathematical modelling language.
  you build mathematical models in K, and one of the key features of K is that those models are executable. So, for example you can ake your test suite and execute it against KEVM which is the mathematical model of the ethereum virtual machine in K, or you can make proofs

  So, if you were to say, wan

anvacaru

{
  "contractName": "ERC20EXT",
  "abi": [
    {
      "inputs": [
        {
          "internalType": "string",
          "name": "name",
          "type": "string"
        },

anvacaru

   > {
   >   "jsonrpc": "2.0",
   >   "id": 1,
   >   "method": "net_version",
   >   "params": []
   > }
 <   {
 <     "id": 1,
 <     "jsonrpc": "2.0",
 <     "result": "1553001029840"