![About Runtime Verification logo](/assets/img/logos/publications.png)
We Love Formal Methods
![About Runtime Verification logo](/assets/img/logos/publications.png)
![Runtime Verification website hero](/assets/img/body-left-light.png)
![Runtime Verification website hero](/assets/img/body-right-light.png)
![Runtime Verification website hero](/assets/img/mobile-header.png)
Welcome to the Runtime Verification blog. We have been working in the web3 security space since 2018 and we love to share what we have learned. Our blog posts are a great way to learn about our audits and formal verification engagements with web3 protocols for readers that may find the audit reports too long or technical.
Our authors write about progress on our tooling - ERCx, Kontrol and Simbolik, all of which are designed and maintain with the goal of helping developers and users interact with blockchains more securely. Dive in and learn with us, and if you have any questions contact us.
![How We Build Formal Verification and Fuzzing Tools: Bridging the Gap Between Developers and Advanced Security Tooling with the K Framework](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fruntime_verification_logo_black_957e882be7.png&w=640&q=75)
How We Build Formal Verification and Fuzzing Tools: Bridging the Gap Between Developers and Advanced Security Tooling with the K Framework
by Gregory Makodzeba
December 10th, 2024![With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
With $33B TVL on the Line, Lido Turns to Runtime Verification for a Design Review
by Runtime Verification
September 4th, 2024![External Computation with Kontrol: Leveraging Foundry Execution for Formal Verification](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2FBFA_832_D7_AB_77_42_A8_A88_E_E395_B9_B9_CFA_6_273641f95d.png&w=640&q=75)
External Computation with Kontrol: Leveraging Foundry Execution for Formal Verification
by Juan Conejero
August 28th, 2024![Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2FBFA_832_D7_AB_77_42_A8_A88_E_E395_B9_B9_CFA_6_273641f95d.png&w=640&q=75)
Using Kontrol to Tackle Complexities Caused by Dynamically-Sized Constructs
by Petar Maksimović
August 19th, 2024![Formal Verification Lore Intuitive Intro to Why We Can Prove Programs Correct](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fruntime_verification_logo_black_957e882be7.png&w=640&q=75)
Formal Verification Lore Intuitive Intro to Why We Can Prove Programs Correct
by Juan Conejero
April 2nd, 2024![Introducing KMIR: concrete and symbolic execution of Rust MIR](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fruntime_verification_logo_black_957e882be7.png&w=640&q=75)
![Using Foundry to Explore Upgradeable Contracts (Part 1)](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
![K-Michelson: a Case Study on Formal, Executable Language Specification (Part 2)](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Ftezos_a4b3164e7a.png&w=640&q=75)
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 2)
by Stephen Skeirik
December 11th, 2020![K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Ftezos_a4b3164e7a.png&w=640&q=75)
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)
by Stephen Skeirik
November 2nd, 2020![Runtime Verification completes another successful engagement with PlatON Networks](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2FPlat_ON_logo_3ad945c0fa.png&w=640&q=75)
Runtime Verification completes another successful engagement with PlatON Networks
by Bogdan Stanciu
October 26th, 2020![Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Falgorand_60718be2e8.png&w=640&q=75)
Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem
by Musab Alturki
July 28th, 2020![Formally Verifying Finality in Gasper: The Core of the Beacon Chain](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fethereum_logo_landscape_purple_d0e9145e6f.png&w=640&q=75)
![KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fgitcoin_logo_horizontal_light_815f7a6f61.png&w=640&q=75)
KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0
by Rikard Hjort
March 26th, 2020![Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements
by Stephen Skeirik
March 10th, 2020![Runtime Verification enters a protocol verification agreement with PlatON](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2FPlat_ON_logo_3ad945c0fa.png&w=640&q=75)
Runtime Verification enters a protocol verification agreement with PlatON
by Bogdan Stanciu
March 9th, 2020![Formal Verification 101 for Blockchain Systems and Smart Contracts](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
Formal Verification 101 for Blockchain Systems and Smart Contracts
by Stephen Skeirik
February 18th, 2020![End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fethereum_logo_landscape_purple_d0e9145e6f.png&w=640&q=75)
End-to-End Formal Verification of Ethereum 2.0 Deposit Smart Contract
by Daejun Park
January 20th, 2020![K vs. Coq as Language Verification Frameworks (Part 2 of 3)](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
![K vs. Coq as Language Verification Frameworks (Part 1 of 3)](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
![K vs. Coq as Language Verification Frameworks (Part 3 of 3)](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
![A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fethereum_logo_landscape_purple_d0e9145e6f.png&w=640&q=75)
A Formal Model in K of the Beacon Chain: Ethereum 2.0’s Primary Proof-of-Stake Blockchain
by Musab Alturki
October 22nd, 2019![The RV Bounded Model Checker - A lightweight semantics-based tool](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
![Formally Verifying Algorand: Reinforcing a Chain of Steel (Modeling and Safety)](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Falgorand_60718be2e8.png&w=640&q=75)
Formally Verifying Algorand: Reinforcing a Chain of Steel (Modeling and Safety)
by Musab Alturki
June 18th, 2019![Runtime Verification goes multinational by opening Bucharest based subsidiary](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
Runtime Verification goes multinational by opening Bucharest based subsidiary
by Patrick MacKay
November 27th, 2018