Category: K
K 7.0: Improving K for Ecosystem Tool Developers
April 2024 saw the release of version 7.0 of the K Framework. Previously, K was focused on the implementation of programming language semantics, and external tool support was required to expand those semantics into production tooling for a language. In K 7.0, we have merged our Python support library for K (Pyk) into the K compiler, making it the primary way for tool developers to interact with K.
Modernizing K: Enhancing Functionality and Ease of Use
With K v6 we are modernizing the K Framework. We focused on emphasizing usability and customization in the design to make it easier than ever to generate a set of tools for your programming language environment.
From 0 to K Tutorial
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification Raises $5.3 Million to Advance Blockchain Security
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
MultiversX (formerly Elrond) gets new secure dev tooling and a formal semantics
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 2)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
K-Michelson: a Case Study on Formal, Executable Language Specification (Part 1)
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Runtime Verification and Algorand announce a new engagement to build formal tools for Algorand’s smart contract ecosystem
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formal Verification Framework for Michelson
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formally Verifying Finality in Gasper: The Core of the Beacon Chain
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
KWasm and KEwasm: executable semantics and formal verification tools for Ethereum 2.0
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
Formal Verification 101 for Blockchain Systems and Smart Contracts: Formalizing Requirements
Runtime Verification Inc applies formal methods to improve the safety, reliability, and correctness of computing systems for aerospace, automotive, and the blockchain.
