We love formal methods

$EGLD gets formal verification tools from @rv_inc With otherwise expensive & complex testing tools available in the Elrond devkit the overall security of our DeFi ecosystem raises to meet institutional-grade requirements.

Elrond eGold @ElrondNetwork

The work been done by @rv_inc, it’s incredible. I only have good things to say and the more I learn about K-Framework, the more ideas I get to bring even more innovation to @Cardano 💪 #cardano

Nico Arqueros @NicoArqueros

The first ever ERC20 formal verification spec was done by @rv_inc they now made one for ERC777 as well! The next token standard. Now we need automated gen. proofs and checkers to run those!

Fabian Vogelsteller @feindura

@ercwl @rv_inc Yeah, the KEVM is amazing. We also built https://github.com/dapphub/klab to be able to explore the complete space of execution paths for an ethereum contract. Browser version in the pipeline!

Martin Lundfall @MartinLundfall

This report on @rv_inc's verification of RANDAO's possible randomness bias under worst-case adversarial conditions using statistical model checking is one of the most underrated new papers in cryptocurrency security/modeling, IMO.
rdao-analysis.pdf

Philip Daian @phildaian

To make the Gnosis Safe one of the most secure multisigs on the market, we worked with formal verification pros @rv_inc and updated our smart contracts. Check out the full report here 👉
GnosisSafe_RuntimeVerification.pdf

Gnosis Safe @gnosisSafe

Another major achievement is the Meta VM Elrond brings by building a GO backend to K framework. Through this we will support 3 VMs at the same time for max flexibility: EVM, WASM, IELE + formal verification

Beniamin Mincu ⚡ @beniaminmincu

Warming up to proposing the Jello Paper as the canonical EVM spec, and would love everyone's thoughts. IMO the Jello Paper way clearer and complete versus the current Yellow Paper. Kudos to the KEVM folks 🎉 https://ethereum-magicians.org/t/jello-paper-as-canonical-evm-spec/2389

Brooklyn Zelenka 🏳️‍🌈 @expede

Just released v0.11.3 with critical bug fix to the eth2 state transition spec. Special thanks to @daejunpark for finding the bug while doing formal verification on the eth2 spec for @rv_inc! https://github.com/ethereum/eth2.0-specs/releases/tag/v0.11.3

Danny Ryan @dannyryan

@rv_inc! completes the formal verification of the eth2 deposit contract bytecode! https://github.com/runtimeverification/verified-smart-contracts/blob/master/deposit/bytecode-verification/deposit-spec.ini

Danny Ryan @dannyryan

Honestly, @rv_inc was incredible to work with. They were incredibly thorough, thoughtful and dilligent in the entire process. We're looking forward to continuing work with them and a special callout to @daejunpark.

Will Villanueva @wjvill

Giskard Protocol (CBFT) was formally verified by @rv_inc. It should be a technical requirement for the industrial adoption of any innovative public ledger.

Chen Li @ChenLLII