KronosSlott
  • Altcoin
  • Bitcoin
  • Blockchain
  • Ethereum
  • Litecoin
  • Gambling

Subscribe to Updates

Get the latest Crypto news from kronosslott.

What's Hot

Price Prediction: By February 9, 2023, Zilliqa (ZIL) Value Will Increase to $0.045938

February 4, 2023

Sberbank Aims To Have Own DeFi Platform Up And Running By May

February 4, 2023

Casper Price Soars To $0.04 As Bulls Stay In Check – $0.055 CSPR Incoming?

February 4, 2023
Facebook Twitter Instagram
  • Affiliate Disclosure
  • Anti Spam Policy
  • Cookie Policy
  • Privacy Policy
  • Terms & Conditions
Facebook Twitter Instagram
KronosSlott
  • Altcoin
  • Bitcoin
  • Blockchain
  • Ethereum
  • Litecoin
  • Gambling
KronosSlott
Home » Dev Update: Formal Methods | Ethereum Foundation Blog

Dev Update: Formal Methods | Ethereum Foundation Blog

adminBy adminOctober 11, 2022No Comments3 Mins Read
Facebook Twitter Pinterest LinkedIn Tumblr Reddit Telegram Email
The Devcon VI Manual | Ethereum Foundation Blog
Share
Facebook Twitter LinkedIn Pinterest Email


I’m joining Ethereum as a formal verification engineer. My reasoning: formal verification makes sense as a profession only in a rare situation where

  • the verification target follows short, simple rules (EVM);
  • the target carries lots of value (Eth and other tokens);
  • the target is tricky enough to get right (any nontrivial program);
  • and the community is aware that it’s important to get it right (maybe).

My last job as a formal verification engineer prepared me for this challenge. Besides, around Ethereum, I’ve been playing with two projects: an online service called Dr. Y’s Ethereum Contract Analyzer and a github repository containing Coq proofs. These projects are at the opposite extremes of a spectrum between an automatic analyzer and a manual proof development.

Considering the collective impact to the whole ecosystem, I’m attracted to an automatic analyzer integrated in a compiler. Many people would run it and some would notice its warnings. On the other hand, since any surprising behavior can be considered a bug, any surprise should be removed, but computers cannot sense the human expectations. For telling human expectations to the machines, some manual efforts are necessary. The contract developers need to specify the contract in a machine-readable language and give hints to the machines why the implementation matches the specification (in most cases the machine wants more and more hints until the human realizes a bug, frequently in the specification). This is labor intensive, but such manual efforts are justifiable when a contract is designed to carry multi-million dollars.

Having a person dedicated to formal methods not only gives us the ability to move faster in this important but also fruitful area, it hopefully also allows us to communicate better with academia in order to connect the various singular projects that have appeared in the past weeks.

Here are some projects we would like to tackle in the future, most of them will probably be done in cooperation with other teams.

Solidity:

  • extending the Solidity to Why3 translation to the full Solidity language (maybe switch to F*)
  • formal specification of Solidity
  • syntax and semantics of modal logics for reasoning about multiple parties

Community:

  • creating a map of formal verification projects on Ethereum
  • collecting buggy Solidity codes, for benchmarking automatic analyzers
  • analyzing deployed contracts on the blockchain for vulnerabilities (related: OYENTE tool)

Tools:

  • provide a human- and machine-readable formalization of the EVM, which can also be executed
  • developing formally verified libraries in EVM bytecode or Solidity
  • developing a formally verified compiler for a tiny language
  • explore the potential for interaction-oriented languages (“if X happens then do Y; you can only do Z if you did A”)



Source link

Share. Facebook Twitter Pinterest LinkedIn Tumblr Email
admin
  • Website

Related Posts

Grantee Roundup – Q1 2023

February 3, 2023

EF-Supported Teams: Research & Development Roundup

December 29, 2022

KZG Ceremony Grant Round | Ethereum Foundation Blog

December 15, 2022

Comments are closed.

Don't Miss

Price Prediction: By February 9, 2023, Zilliqa (ZIL) Value Will Increase to $0.045938

Blockchain February 4, 2023

Join Our Telegram channel to stay up to date on breaking news coverage Zilliqa is…

Sberbank Aims To Have Own DeFi Platform Up And Running By May

February 4, 2023

Casper Price Soars To $0.04 As Bulls Stay In Check – $0.055 CSPR Incoming?

February 4, 2023

ETC/USD Prepares for $30 Resistance

February 4, 2023
Stay In Touch
  • Facebook
  • Twitter
  • Pinterest
  • Instagram
  • YouTube
  • Vimeo
Our Picks

Price Prediction: By February 9, 2023, Zilliqa (ZIL) Value Will Increase to $0.045938

February 4, 2023

Sberbank Aims To Have Own DeFi Platform Up And Running By May

February 4, 2023

Casper Price Soars To $0.04 As Bulls Stay In Check – $0.055 CSPR Incoming?

February 4, 2023

ETC/USD Prepares for $30 Resistance

February 4, 2023

Subscribe to Updates

Get the latest Crypto news from kronosslott.

About Us
About Us

Your source for the serious news. This website is crafted specifically to for crazy and hot cryptonews. Visit our main page for more tons of news.

We're social. Connect with us:

Facebook Twitter Pinterest YouTube WhatsApp
Categories
  • Altcoin (4)
  • Bitcoin (2,020)
  • Blockchain (845)
  • Ethereum (321)
  • Gambling (2,082)
  • Litecoin (60)
  • NFTs (2)
Our Picks

Price Prediction: By February 9, 2023, Zilliqa (ZIL) Value Will Increase to $0.045938

February 4, 2023

Sberbank Aims To Have Own DeFi Platform Up And Running By May

February 4, 2023

Casper Price Soars To $0.04 As Bulls Stay In Check – $0.055 CSPR Incoming?

February 4, 2023
©2022 –Kronosslott. All Rights Reserved. Kronosslott.com is an independent i-Gaming news site and casino comparison service. Every effort is made to ensure that the bonus offers listed here are accurate and up-to-date. However, we accept no responsibility for inaccuracies or errors. It is your responsibility to confirm the terms of any promotion you choose to accept. Looking to Advertise with us? Kronosslott is always looking for new partnerships. To Inquire please email kronosslott@gmail.com

Type above and press Enter to search. Press Esc to cancel.