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

Subscribe to Updates

Get the latest Crypto news from kronosslott.

What's Hot

Avalanche Drops, Litecoin Faces Resistance, Borroe.Finance Passes $1.1 Million

September 23, 2023

BTC to $30K? Glassnode Founders Think So; XRP, LINK, and QUBE Poised for Monumental Rise

September 23, 2023

ImmutableX spiked 34% after major crypto exchange lists IMX

September 22, 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

Devconnect Istanbul Updates! | Ethereum Foundation Blog

September 18, 2023

Ethereum Execution Layer Specification | Ethereum Foundation Blog

August 29, 2023

Allocation Update: Q2 2023 | Ethereum Foundation Blog

August 15, 2023

Comments are closed.

Don't Miss

Avalanche Drops, Litecoin Faces Resistance, Borroe.Finance Passes $1.1 Million

Altcoin September 23, 2023

Avalanche’s ($AVAX) market performance succumbs to bearish pressure, leaving its holders in panic. Elsewhere, Litecoin’s…

BTC to $30K? Glassnode Founders Think So; XRP, LINK, and QUBE Poised for Monumental Rise

September 23, 2023

ImmutableX spiked 34% after major crypto exchange lists IMX

September 22, 2023

What next after 9% ARB this past week?

September 22, 2023
Stay In Touch
  • Facebook
  • Twitter
  • Pinterest
  • Instagram
  • YouTube
  • Vimeo
Our Picks

Avalanche Drops, Litecoin Faces Resistance, Borroe.Finance Passes $1.1 Million

September 23, 2023

BTC to $30K? Glassnode Founders Think So; XRP, LINK, and QUBE Poised for Monumental Rise

September 23, 2023

ImmutableX spiked 34% after major crypto exchange lists IMX

September 22, 2023

What next after 9% ARB this past week?

September 22, 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 (171)
  • Bitcoin (2,020)
  • Blockchain (1,713)
  • Ethereum (346)
  • Gambling (2,082)
  • Litecoin (221)
  • NFTs (2)
Our Picks

Avalanche Drops, Litecoin Faces Resistance, Borroe.Finance Passes $1.1 Million

September 23, 2023

BTC to $30K? Glassnode Founders Think So; XRP, LINK, and QUBE Poised for Monumental Rise

September 23, 2023

ImmutableX spiked 34% after major crypto exchange lists IMX

September 22, 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.