KSwap-VM

Initial idea was to make swap-vm as secure as possible but also give a leverage for future builders to secure their composite programs on swap-vm

First part of the project - is its numerous specs and proofs for instructions of swap-vm. These specs and proofs were good enough that we were able to find bugs which lead us to filing relevant bug reports

Second -- formal semantics that allows to reason and write proofs for new composite programs written on swap-vm, which allows us to formally verify any code written with swap-vm as base. For example, we created our own tiny app called sweeper that we formally verified.

One stack throughout: Kontrol on top of KEVM on top of K.

For the instruction proofs, specs are written as Solidity property tests and given to Kontrol. It compiles the contract, lifts the deployed bytecode into KEVM — the K semantics of the EVM — and symbolically executes it, sending side conditions to an SMT solver. Working on bytecode rather than source means what is proved is what actually gets deployed.

Most of the effort went into making proofs terminate: tuning the Booster backend's equation limits and fallback, raising depth and SMT timeouts, and building a lemma library for byte-level reasoning. The bugs surfaced here, as counterexamples with path conditions. We did not call any of them confirmed until we had replayed them as forge tests that fail.

The second part is why the stack matters. We wrote the SwapVM semantics directly in K, the same language KEVM is written in, so both levels share a prover and a way of stating claims. "This instruction's bytecode is correct" and "this composite program is correct" differ in what they quantify over, not in how they are written or checked.