Category: K
![Kontrol Integrated Verification of the Optimism Pausability Mechanism](/_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)
Kontrol Integrated Verification of the Optimism Pausability Mechanism
by Runtime Verification
May 16th, 2024![Runtime Verification Hosts EthCluj Workshop on Formal Methods](/_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](/_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![Modernizing K: Enhancing Functionality and Ease of Use](/_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)
![Runtime Verification Raises $5.3 Million to Advance Blockchain Security](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
Runtime Verification Raises $5.3 Million to Advance Blockchain Security
by Runtime Verification
June 18th, 2021![MultiversX (formerly Elrond) gets new secure dev tooling and a formal semantics](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fmultiversx_dark_f750dab64b.png&w=640&q=75)
MultiversX (formerly Elrond) gets new secure dev tooling and a formal semantics
by Rikard Hjort
January 5th, 2021![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 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![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 3 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 2 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)
![RV Inc. & FSL @ UIUC Release First Formal Viper Tools](/_next/image?url=%2Fassets%2Fimg%2Frv-logo.png&w=640&q=75)
![New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)](/_next/image?url=https%3A%2F%2Fstrapi-rv-bucket-01.s3.us-east-2.amazonaws.com%2Fiohk_logo_a5d01aea3f.png&w=640&q=75)
New Technologies for the Blockchain: IELE (virtual machine) and K (universal language framework)
by Grigore Roșu
October 25th, 2017