Disclaimer: grammar fixed by AI

On a stormy day, I, the philosopher, was looking at a protocol. I could smell something weird with it, but after reading it a dozen times, I still had not found what I was looking for. Let me pull out the big gun: formal verification! Let the magic wand tell me what is going on.

The choice is between Certora prover and Kontrol. TLA+ requires you to compile the code into temporal logic manually, which could be error prone. Theorem provers like Isabelle and Coq seem like a bad fit for Solidity. Considering how crappy my laptop is, the only viable choice is basically Certora prover. It has great optimizations and is very easy to use. However, when I tried to learn it last time, there was something weird. It is a different mindset—like a Python developer trying to learn Haskell for the first time.

Enough worrying! Let's simply get our hands dirty! Now, let's summon the great power of formal verification to unveil all hidden dirty technical secrets of my poor target protocol! WA-HAHAHAHA! But still, baby steps:

pragma solidity >=0.8.0;
import {ERC20} from "./ERC20.sol";  // standard ERC20

contract Factory {
    function createToken() public returns (address) {
        return address(new ERC20("name", "symbol", 18));
    }
    
    function transferToken(ERC20 token, uint256 amount) public {
        token.transfer(msg.sender, amount);
    }
}

With this straightforward CVL rule:

using ERC20 as token;

rule transferWorks(env e) {
    uint256 amount;
    uint256 bal0;
    uint256 bal1;
    
    require bal0 == token.balanceOf(e, currentContract);
    transferToken(e, token, amount);
    require bal1 == token.balanceOf(e, currentContract);
    
    assert bal0 == bal1 + amount;
}

**Havoc Hell:**
After I fluently ran the prover with my shiny virtual lab experiment, the keyboard started freezing. I realized, no, the devil is near! I rushed to the final report HTML page and found the prover in high fever and talking nonsense.

What? It said the rule fails, but with bullshit reasons. Is the prover infected with Corona-virus? It was like the numbers came to life and changed themselves with no programming logic at all! I didn't understand this failure.

I read the protocol code again and again, and was certain that the prover and I were not on the same channel. Then I realized, yes, it must be "[havoc](https://docs.certora.com/en/latest/docs/user-guide/glossary.html#term-havoc)" coming back to life! That does exactly this: lobbying the lawful numbers into freedom fighters and changing themselves randomly!

But no way. The only possible "unresolved external call" that could betray me to introduce "havoc" is `transfer`, but I deliberately told the prover that the token is `ERC20`. It should not be unresolved.

Confused, but the final report said nothing about whether it was using havoc. After pondering for 5 seconds, I think the best way to confirm a havoc invasion is to use the cloud verification tool, which has more information. Right now I am running the prover locally.

Time to try the cloud version with its fancy UI—except I couldn't find how to enable it.

After scouring docs in vain, I tried:
- Modifying `certoraRun.py` scripts → failed
- Reinstalling the CLI in a new Python virtual environment → still local
- Wondering how it even found my local prover

Looks like the CLI and I spoke different languages and failed to communicate. If you insist on running locally, how about I hide the local prover path? What would you do then? I guess that is what you call hacker intuition.

`unset CERTORA` nuked the environment variable, which I think is how CLI finds the local prover. Bingo! Cloud UI unlocked. There I saw the smoking gun: when `token` entered `transferToken`, the prover went "default havoc"—treating it as an abstract entity and changing values arbitrarily.

Of course! All my self-doubt about my Solidity and CVL skills was gone. For a moment, I thought I was crazy! The devil is indeed here!

**Dispatcher Fix:**
I switched to the dispatcher pattern and added a self-transfer guard:

using ERC20 as token;

methods {
    function _.transfer(address,uint256) external => DISPATCHER(true);
}

rule transferWorks(env e) {
    uint256 amount;
    uint256 bal0;
    uint256 bal1;
    
    require e.msg.sender != currentContract; // Prevent factory self-transfers
    require bal0 == token.balanceOf(e, currentContract);
    transferToken(e, token, amount);
    require bal1 == token.balanceOf(e, currentContract);
    
    assert bal0 == bal1 + amount; // Finally passed!
}

This will let the prover know for sure where to resolve the "unresolved external call". This looks like a duct-tape solution to me, but let's get it running and prettify it later. Since Certora prover is still in beta, it could be a bug as well.

**Vacuity Vortex:**
Confident again, I added a new rule:

rule createTokenWorks(env e) {
    require token == createToken(e); // vacuous!
    token.balanceOf(e, currentContract);
    assert false;
}

Except the prover decided to quit its job for good this time. It did not believe my rule was even worth verifying, since it was vacuous.

What the actual hell? This is the simplest test! This is as common as breathing for EVM—how is the prover rejecting it? At first, I had more CVL statements than shown above, so I was not certain about the source of vacuity. I thought some of my requirements were somehow not playing well with each other—contradiction in requirements is supposed to be the main reason for vacuity.

How to debug vacuity? Comment out all of the statements and figure out which ones are the criminals. I did not expect the innocent-looking lawful citizen, `require token == createToken(e);`, to rob me. I asked it why, but it refused to answer.

I don't understand, but I respect that. Maybe you think `token` is already created, and therefore a newly created contract cannot have the same address. OK, I will play your game.

rule createTokenWorks(env e) {
    address token2;
    require token2 == createToken(e);
    token2.balanceOf(e, currentContract); // vacuous!
    assert false;
}

The keyboard froze again, and froze off my toes. Yeah, getting used to it. This was vacuous again!

Right after I pulled all of my hair out, I finally realized that all method calls to `token2` would revert (probably)! But it should not! The prover treated new contract addresses like ghost objects.

Very unexpected! Then how do I do this? There are some factory functions that need to create new contracts, and I want to test the new contracts in the same rule. Am I just too weird trying to test this?

My breakthrough came when I shifted verification logic to Solidity:

function createTokenAndBalance(uint256 bal) public returns (address) {
    ERC20 ret = new ERC20("name", "symbol", 18);
    assert(bal == ret.balanceOf(msg.sender)); // Anchor in reality
    return address(ret);
}

rule createTokenAndBalanceWorks(env e) {
    address token2;
    uint256 bal;
    require token2 == createTokenAndBalance(e, bal);
    satisfy true; // Partial victory
}

But this only checks happy paths since Certora ignores reverts. But probably we can change this rule to check meaningful properties as well.

Anyways, we have conquered another obstacle and stepped on it. Let's keep marching forward!

**Dispatcher Revenge:**
Just when I thought I'd won, adding a dispatcher for `balanceOf` reintroduced vacuity:

methods {
    function _.balanceOf(address) external => DISPATCHER(true); // Vacuity returns!
}

Why did I add the dispatcher? You guessed it: to stop it from havoc. How would that rule be meaningful if it simply returned meaningless values?

I had no reason to suspect the dispatcher rule leading to vacuity. What I tried was to change different functions to call while punching the wall. Through brutal trial-and-error, I discovered:
- Change the method code to make sure it never reverts → no effect
- Renaming method → works
- Commenting out dispatcher → rule works
- Adding dispatcher → VACUITY

Then it is really a catch-22.

Honestly, with this much trouble, right now I feel like I prefer Kontrol, the other symbolic execution tool. But of course, the second I actually use Kontrol, I will miss the days with Certora. Both are just hard.

**Diagnostic tools:**
I was desperate, toe-less, hairless, meaninglessly clicking around, tongue swinging. Is this where my Certora journey ends? Me? The philosopher?

Then somehow I noticed there were more HTMLs under the `Reports` folder. I tried to open one of them and found that it was the diagnostic tools UI that I wanted before! Let's not go home yet!

Look out! The stubborn researcher is coming back to life!

I stared at the "tac" code. The one on the left is without dispatcher. I could see the difference from the call trace.

I swept through the vacuous rule and did not see where it was reverting the dispatched method. I was very confused, but maybe try something nasty like this:

rule createTokenWorks(env e) {
    address token2;
    // require token2 == createToken(e);

    token2.balanceOf(e, currentContract);

    assert false;
}

Of course it was not vacuous. This was expected. But did it resolve or havoc? Yes. However, even with the dispatcher commented out! So weird! I guess I spoke a different language than Certora after all.

To test out its temper a bit more, I tried to call a function that did not exist from CVL. In this case, even the Certora compiler threw an error. It was dispatched at compile time and then hardcoded into TAC!

Maybe it did not revert, but something else made it vacuous? Let's try the most basic vacuous example with requirements. Let's go crazy:

rule basicVacuity() {
    uint256 x;
    require x > 0 && x < 0;

    assert false;
}

And I couldn't believe my eyes. TAC had nothing!

Compiled TAC:

TACSymbolTable {
	UserDefined {
		UninterpSort skey
	}
	BuiltinFunctions {
	}
	UninterpretedFunctions {
	}
}
Program {
	Block 0_0_0_0_0_0 Succ [] {
		NopCmd
	}
}
Axioms {
}
Metas {
}

I can only take it as some kind of Certora TAC compiler optimization.

I was clueless and hopeless. Wait, is someone knocking on my door? Oh, it's Kontrol.

**Kontrol time**
Now I have to try Kontrol, jokes aside. I did light experiments with Kontrol before but never noticed anything about vacuity. I wonder how it handles it.

I installed Kontrol on my brand new home server and was ready to go. First, I had a simple test like this:

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.13;

import {Test, console} from "forge-std/Test.sol";
import {Factory} from "../src/Factory.sol";
import {ERC20} from "../src/ERC20.sol";
import {KontrolCheats} from "kontrol-cheatcodes/KontrolCheats.sol";

contract FactoryTest is Test, KontrolCheats {
    Factory public f;

    function setUp() public {
	    f = new Factory();
    }

    function testCreate(address u) public {
        address token = f.createToken();

        assert(ERC20(token).balanceOf(u) == 0);
    }

}

After I was done proving and looking at the CFG, somehow whenever I clicked on something, it gave me error `MarkupError: Expected markup value` and quits. Why? Why would God do this to me? This was supposed to just work!

I found no relevant issues on GitHub or Discord. Luckily AI realized that the markup content was not escaping some special characters, causing bad syntax. The quick fix was to change `/nix/store/nm58p2h35klbfy8s8y4a80q7yvl5spx6-kontrol-pyk-env/lib/python3.10/site-packages/pyk/kcfg/tui.py`:

class NavWidget(ScrollableContainer, can_focus=True):
    text: reactive[str] = reactive('', init=False)

    class Selected(Message):
        def __init__(self) -> None:
            super().__init__()

    BINDINGS = [
        ('g', 'scroll_home', 'Go to vert start'),
        ('G', 'scroll_end', 'Go to vert end'),
    ]

    def __init__(self, id: str):
        super().__init__(id=id)

    def update(self, text: str) -> None:
        self.text = text

    def compose(self) -> ComposeResult:
        yield Static(self.text)

    def watch_text(self) -> None:
        ################ Changed this ##################
        def escape_kterm(s: str) -> str:
            return s.replace("[", "\[")#.replace("]", "\]")

        self.query_one(Static).update(escape_kterm(self.text))
        ##############################################

Now, Kontrol is happy with the proof:

server@server:~/lab/kontrolexample$ kontrol prove --match-test FactoryTest.testCreate --reinit
🏃 Running Kontrol proofs 🏃 
 Add `--verbose` to `kontrol prove` for more details!
Selected functions: test%FactoryTest.testCreate(address)
Running setup functions in parallel: test%FactoryTest.setUp()
  0:00:14 test%FactoryTest.setUp():1 Finished PASSED: 4 nodes: 0 pending|1 passed|0 failing|0 vacuous|0 refuted|0 stuck
Running test functions in parallel: test%FactoryTest.testCreate(address)
  0:00:33 test%FactoryTest.testCreate(address):1 Finished PASSED: 16 nodes: 0 pending|1 passed|0 failing|0 vacuous|0 refuted|0 stuck
✨ PROOF PASSED ✨ test%FactoryTest.testCreate(address):1
⏳ Time: 34s ⏳

I deliberately made a vacuous test and found it showed something like this:

server@server:~/lab/kontrolexample$ kontrol build --regen --rekompile
🔨 Building Kontrol project 🔨 
 Add `--verbose` to `kontrol build` for more details!
✅ Success! Kontrol project built 💪
server@server:~/lab/kontrolexample$ kontrol prove --match-test CounterTest.testVacuity
🏃 Running Kontrol proofs 🏃 
 Add `--verbose` to `kontrol prove` for more details!
Selected functions: test%CounterTest.testVacuity(uint256)
Running setup functions in parallel: test%CounterTest.setUp()
  0:00:16 test%CounterTest.setUp():2 Finished PASSED: 6 nodes: 0 pending|1 passed|0 failing|0 vacuous|0 refuted|0 stuck
Running test functions in parallel: test%CounterTest.testVacuity(uint256)
⠋ 0:00:12 test%CounterTest.testVacuity(uint256):0 Running proof PENDING: 4 nodes: 1 pending|0 passed|0 failing|0 vacuous|0 refuted|0 stuckWARNING 2025-07-10 01:14:03,092 pyk.kcfg.kcfg - Extending KCFG with: vacuous node: 9
  0:00:12 test%CounterTest.testVacuity(uint256):0 Finished PASSED: 5 nodes: 0 pending|0 passed|0 failing|1 vacuous|0 refuted|0 stuck
✨ PROOF PASSED ✨ test%CounterTest.testVacuity(uint256):0
⏳ Time: 13s ⏳

Vacuity problem solved? Let's call it a day.

One more thing. See if we should contribute to the `pyk` project and help fix the problem, just in case someone else gets this bug.

server@server:~/lab/kontrolexample$ . /nix/store/nm58p2h35klbfy8s8y4a80q7yvl5spx6-kontrol-pyk-env/bin/activate
(kontrol-pyk-env) server@server:~/lab/kontrolexample$ python
Python 3.10.14 (main, Mar 19 2024, 21:46:16) [GCC 13.2.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> import pyk
>>> pyk.__version__
'7.1.273'

Could be a new bug from the newest release? It would explain why no one else is posting it.

Let's submit a new [issue](https://github.com/runtimeverification/k/issues/4839).