Runtime Verification proved Algorand can't fork — its KAVM tool has been idle since 2023

2026-08-19

formal-verification · security · audits · consensus · kavm · discovery · web · updated

A machine-checked safety theorem

In 2019 the Algorand team handed its consensus protocol to a small Champaign-Urbana startup and asked for something few blockchains had ever commissioned: a machine-checked proof that the protocol could never split. Runtime Verification, then best known for applying formal methods to aerospace and automotive code, delivered it using Coq, an interactive proof assistant.

Formal verification works differently from testing. Instead of running code against sample inputs and hoping the cases cover the dangerous paths, the engineer writes the system as mathematical definitions and then proves properties about it the way a mathematician proves a theorem, with every inference step checked by software. Human intuition can skip a step or miscount an edge case; the proof assistant cannot.

The property RV proved was asynchronous safety: no two honest nodes can ever certify different blocks for the same round, even when the network partitions so badly that groups of nodes cannot reach each other. That guarantee is the mathematical basis of Algorand's [single-block finality](/glossary/single-block-finality "A feature of some blockchains where transactions are confirmed and made irreversible in a single block, eliminating the need for multiple confirmation") — the property that a confirmed block is permanent, with no probabilistic waiting period for extra confirmations. Algorand's own announcement at the time called the chain 'the first blockchain to provide immediate transaction finality.'

The model, published in June 2019 by RV researchers Musab Alturki, Brandon Moore, Karl Palmskog and Lucas Pena, broke the safety theorem into about 170 lemmas and pinned down the assumptions the guarantee rests on, including that a supermajority of stake is held by honest users. The algorand-verification repository remains public, with maintenance releases through 2022. Algorand's protocol experts Jing Chen, Nickolai Zeldovich and Victor Luchangco worked alongside the RV team on the engagement.

From protocol theorems to a DeFi audit bench

The 2019 engagement became a standing relationship. In July 2020 the Algorand Foundation awarded RV a grant under its 250 million ALGO Ecosystem Grants Program to build a formal semantic framework for Algorand smart contracts using the K Framework, RV's 'programming language for programming languages' — a system that lets engineers define a language's behavior once and automatically derive interpreters, debuggers and verification tools from that definition. The original proposal anticipated formalizing a high-level language adapted from Blockstack's Clarity; by the time a public beta shipped in 2023, the work had settled on the Algorand Virtual Machine ([AVM](/glossary/avm "Algorand Virtual Machine, the software environment that executes smart contracts on the Algorand blockchain.")), the execution engine for Algorand smart contracts, and [TEAL](/glossary/teal "A low-level, stack-based programming language used to write smart contracts on the Algorand blockchain. It requires manual stack management and lacks "), the assembly-like language the AVM interprets, which Algorand had launched in the meantime.

In December 2021 RV announced it had become the Foundation's security partner. 'We look forward to our partnership and welcome Runtime Verification Inc as our security partner,' said Addie Wagenknecht, then the Foundation's Head of Global Ecosystems and Technical Operations. Audit work followed at scale: between July 2021 and December 2022 RV published thirteen audit engagements spanning the ecosystem's first wave of decentralized finance (DeFi) applications — automated market makers (AMMs), the smart-contract pools that price trades by formula instead of an order book, alongside lending, [liquid staking](/glossary/liquid-staking "A DeFi mechanism where a user locks up a proof-of-stake cryptocurrency (like ALGO) and receives a tradable derivative token (such as xALGO) representi") and stablecoins.

Concept	Real-World Implication
Tinyman [AMM](/glossary/automated-market-maker "The underlying algorithm used by most Algorand DEXs. Instead of matching buyers and sellers via an order book, AMMs use smart contracts and mathematic") V2 (Dec 2022)	The largest Algorand AMM got a five-week review before shipping flash swaps, flash loans and configurable pool fees
Pact, Pact Router and Pact Stableswap (Feb–Aug 2022)	The AMM's core pools, its multi-pool routing contract and its stableswap mathematical invariant were each audited separately
Algofi Lending v2 (Aug 2022)	Lending markets for ALGO and ASAs, the STBL2 [stablecoin](/glossary/stablecoin "A cryptocurrency whose value is designed to stay stable, usually by being pegged 1:1 to a traditional currency like the US dollar (e.g. USDC) or, in H") and a governance-collateral vault reviewed in one engagement
xBacked (Sep 2022)	An over-collateralized stablecoin's master vaults and stability pool, audited in Reach, a specialized smart-contract language
Hone Liquid Staking (Sep 2022)	Governance-rewards staking that mints the liquid dALGO token; the audit pushed a two-contract design down to one
EXA Finance Baskets (May 2022)	Peer-to-peer trading of baskets of up to four assets across four exchange models
Folks Finance, Yieldly, XET and the governance Rewards Contracts (2021–22)	Lending, multi-token staking, token deployment and the community governance machinery from the first wave

The methodology was consistent across the bench: auditors reconstructed the invariants — the properties that must hold for a system to be safe — from protocol documentation, reviewed the [on-chain](/glossary/on-chain "Describes transactions that are recorded and permanently stored on a blockchain ledger, making them publicly visible and tamper-resistant.") source line by line, then simulated large numbers of adversarial behaviors with in-house tooling such as pyteal_eval and tstmodel. Where contracts were written in Tealish, RV also reviewed the TEAL output of the transpiler so the audit did not have to trust the compiler. Under the partnership RV additionally reviewed StakerDAO and AlgoDex in 2021. The sharpest result of the batch: xBacked's first-round review surfaced five high-severity findings, one medium and one informative, with a second round adding two medium findings and another informative. In every 2022 engagement the audited team addressed the issues before launch.

KAVM: the prover that caught a rounding bug

The grant's product went public in March 2023 as KAVM — the formal semantics of the Algorand Virtual Machine, built on K — pitched as a way to formally verify Algorand smart contracts 'without necessarily having a PhD in Computer Science.' KAVM integrated with PyTeal, Algorand's Python framework for writing smart contracts, and with py-algorand-sdk; its launch tutorial walked through a K Coin Vault contract to show what the tool could do.

The demo is the clearest illustration of why formal verification earns its keep on-chain. Smart contracts compute with fixed-point integers, not floating-point numbers, so the order of operations in an arithmetic expression changes the result: X multiplied by Y then divided by Z is not the same as X divided by Z then multiplied by Y, once rounding cuts in. The vault's burn method divided by the exchange rate before scaling — correct-looking code that silently returned zero for small burn amounts. KAVM's prover flagged the method because the symbolic expression of its output did not match the postcondition the developer had specified; a conventional test suite using round numbers passed the same code. It is precisely the class of bug — loss of user funds through arithmetic — that RV's audit methodology lists among its standard checks.

Concept	Real-World Implication
@router.precondition and @router.postcondition decorators on PyTeal ABI methods	A developer states assumptions and expected outputs directly in the contract code; the prover checks the implementation against them
kavm.[algod](/glossary/algod "The core Algorand node daemon ('algo daemon') and its REST API: the live source of truth for the current state of the chain — latest round, account ba") integration with py-algorand-sdk	Existing deployment and testing scripts can run against KAVM as a stand-in for a live node, not just against a sandbox
Planned AlgoKit integration	Would have made KAVM a drop-in replacement for Algorand's Sandbox, bringing verification to any AlgoKit project

Then development stopped. KAVM's README still carries the 'Work in progress' banner, lists symbolic proving ('kavm prove') as 'Not yet implemented', and warns that the specification proofs 'have not yet been fully ported to the current semantics and are failing'. Not all TEAL opcodes are supported and contract-to-contract calls are absent. The repository's last commit is a routine dependency bump from August 2, 2023; the demo repository was last touched in January 2024. KAVM demonstrated the approach on one contract and never became the maintained, documented developer tool its launch post promised — a beta that shipped and then went quiet.

A relay node for real-time monitoring

Three weeks after KAVM's last commit, RV announced a different kind of Algorand contribution: a registered relay node. Relays are the network's backbone — [archival nodes](/glossary/archival-nodes "An archival node is a blockchain node that stores the complete historical record of all transactions and blocks, unlike regular nodes that may delete ") that keep full copies of the ledger, validate and rebroadcast transactions, and appear in Algorand's DNS SRV records so that [participation nodes](/glossary/participation-nodes "Nodes run by ALGO holders to validate transactions and earn staking rewards; in Algorand, all token holders can run them with a minimum stake.") can discover and connect to them. At the time there were about 110 registered relays, RV's among them.

The relay served a monitoring agenda. RV's plan was to turn the invariants proven during audits into runtime monitors that watch deployed contracts and can trigger recovery transactions when a property breaks — for example, flagging an undercollateralized loan before it damages a lending protocol. Most indexing services are too slow for that job, so running a relay gave RV direct, low-latency observation of the network's transaction flow. Whether that relay is still registered today could not be verified: its documentation moved behind a GitBook login, the Wayback Machine holds no snapshot of it, and the current SRV record set does not clearly identify RV's hostname.

The AI-age company — and the idle Algorand toolchain

Runtime Verification today leads its homepage with 'Software Assurance for the AI Age' and has reorganized its services around three lines.

Concept	Real-World Implication
Software Quality Assurance	The core audit business — modeling, property identification, fuzzing and formal verification — for teams that 'can’t afford software failure'
Data Partnerships	RV offers its years of modeling and verification work as training data for LLMs learning high-quality engineering practice
Agentic Guardrails	Security policy enforcement for AI agents: knowing what an agent may do, proving it stays in bounds, and catching violations

The company is real and busy. Founded in 2010 out of the University of Illinois at Urbana-Champaign, it lists 25+ senior engineers, an average tenure of 4 years, and heritage with NASA (three consecutive SBIR grants) and Boeing. Its current showcase work is cross-chain: a pre-launch review of Monad, audits of Espresso's staking contracts and Stellar's Soroban VM, hardening of the WASMI interpreter, and formal verification of Solana's token standard programs. CEO Everett Hildenbrandt describes the engagement standard plainly: 'A Runtime Verification audit report is a stamp of approval from our team.' Its actively developed smart-contract verification product is Ethereum-focused: Kontrol, built on the KEVM semantics, had commits as recently as August 2026.

The Algorand side tells a different story. No Algorand-tagged post has appeared on RV's blog since August 2023, and the dedicated Algorand partnership page that archived the full engagement timeline now resolves to the homepage. The Algorand community has not forgotten the relationship — forum threads since 2019 have repeatedly cited the safety proof against criticisms of the protocol, and a June 2026 governance post recommending a third-party audit named Runtime Verification — but the appetite for AVM formal verification outlived KAVM's development. In May 2023 a community proposal ([xGov](/glossary/xgov "Algorand's community grant-funding program: ALGO holders lock tokens into term pools to earn voting power, and the resulting votes decide which ecosys")-18) requested 250,000 ALGO to finish a Coq-based AVM version 8 library, explicitly framed as an 'alternative to the AVM semantic library of the K Framework'; the proposal's pull request was merged into the xGov repository, and the library at the time supported stepping through 25 AVM opcodes.

What endures for Algorand is that 2019 theorem: the machine-checked proof remains public and unrevoked, and the audit reports from the DeFi wave are still in RV's public repository. But a developer shipping a serious Algorand contract today should know that KAVM is not a maintained verification option — the practical assurance path is a conventional audit, or the semi-formal invariant reasoning Algorand's own developer guidelines describe. The gap between what the 2019 engagement proved and what the tooling track ultimately delivered is the honest measure of the relationship: a foundational proof, a strong audit bench, and a flagship tool that never reached production.

Source

Source: https://runtimeverification.com/