Fire, but verify.

“Program testing can be used to show the presence of bugs, but never to show their absence!”

• Edsger W. Dijkstra, Notes on Structured Programming, 1970 [1]

In Generate, but verify a language model wrote logic and two theorem provers checked it. This post moves one step closer to the code: a verifier that proves things about the Rust program that actually runs. And to make learning it fun, the program is a tank.

Why a tank game?

Robocode has been teaching people to program since 2001 [2]. You write the brain of a small tank. It scans with a radar, turns its gun and fires bullets, and an engine runs the battle. The rules are small and precise: bullet power is between 0.1 and 3.0, firing heats the gun by $1 + p/5$, and the gun can only fire when its heat is zero.

That precision is what makes it good for formal verification. The rules already read like a specification. And a robot’s job (look, decide, act, every turn) has exactly the shape verifiers like: a pure function from what you see to what you do.

It is also, deliberately, a small railway. A signalling system looks at track circuits and points, decides, and acts, every cycle, under rules that must never be broken. RailCheck does this for a toy station with Foras and Z3. A tank that must never fire unsafely is the same kind of problem, with more explosions and less paperwork.

I wanted a way to learn Verus that wasn’t another proof that min(x, y) <= x. So the project became two things:

1. A Rust crate, robocode, that runs battles like the original Java game, with no dependencies at all.
2. RoboVerus, a guide that follows the official Verus tutorial chapter by chapter, but where every example is about robots.

Verus in one paragraph

Verus [3] lets you write specifications and proofs in Rust syntax, next to ordinary Rust code. Every function can carry a precondition (requires) and a postcondition (ensures). Verus turns each function into verification conditions, logical formulas that hold exactly when the code meets its spec, and hands them to Z3 [5]. This is Floyd–Hoare reasoning [6, 7], automated in the style of Dafny [8] and Boogie [9]. For a function $f$ with precondition $P$ and postcondition $Q$, Verus checks the Hoare triple

Three things about Verus mattered most here:

• Callers only see the spec. When code calls decide, Verus doesn’t look inside it; it only knows the ensures. So a spec is an interface, and a weak spec makes every caller’s proof fail.
• Ghost code is erased. Specs and proofs disappear when the code is compiled, so verification costs nothing at run time.
• Integers are easy and floats are hard. Z3 reasons about linear integer arithmetic very well. IEEE-754 floating point [10] is a different world.

That last point shaped everything else.

Two kinds of numbers

The original game’s physics uses double. If battles should follow the original, the engine has to use f64. If I want proofs, the robots have to use integers. So the crate has two layers with a deliberate boundary between them:

The f64 engine follows the Java game. The integer strategy layer is what Verus proves. The runner converts between them.

The integer units are chosen so that every legal value in the game’s rules is exact:

Milli-units make the smallest bullet (0.1) and the gun’s cooling rate (0.1 per turn) exact. The gun heat rule becomes integer arithmetic,

and Verus proves its first, warm-up property without help: $1000 \le \mathit{heat}(p) \le 1600$.

The important design decision: robots use these integer units in every build, not just when verifying. Proving a model and then hoping the real code matches it is the classic gap in formal methods. Here the decide that Verus proves is the decide the battle calls, so the gap shrinks to the conversion at the boundary. That conversion rounds in the safe direction: energy rounds down, gun heat rounds up.

What counts as safe?

Here is the specification at the heart of the project. In Verus these are spec functions: pure mathematical definitions that exist only for verification.

The runner only ever produces well-formed observations, and, since a later fix, Battle::new refuses battlefields beyond the proof’s limit.

Verus proves that the executable angle_diff equals $\delta$, that $-1800 < \delta(a,b) \le 1800$, and that $b + \delta(a,b) \equiv a \pmod{3600}$. I wrote the congruence as a three-way disjunction, not with %, because SMT solvers handle nonlinear modulo poorly and the disjunction is equivalent on this range.

In Verus it reads almost the same:

pub open spec fn safe_to_fire(obs: Observation, p: Power) -> bool {
    &&& MIN_POWER.0 <= p.0 <= MAX_POWER.0
    &&& obs.energy.0 > p.0
    &&& obs.gun_heat.0 == 0
    &&& obs.target matches Some(t) && t.age == 0
    &&& aimed(obs)
}

The proof isn’t about a model of decide. It is about the Rust function that runs in cargo run --example battle. The specs sit in attributes on ordinary Rust:

#[cfg_attr(feature = "verus", verus_verify)]
#[cfg_attr(feature = "verus", verus_spec(r =>
    requires well_formed(*obs),
    ensures r.fire matches Some(p) ==> safe_to_fire(*obs, p),
))]
pub fn decide(obs: &Observation) -> Action { /* … */ }

Without the verus feature the attributes vanish and the crate compiles with no Verus crates at all. With it, Verus verifies the same function body.

A loop, and an invariant

The guide’s third chapter needs a loop: pick the closest of $n$ scanned robots. Verus can’t run a loop to see what it does, so the loop carries an invariant:

It holds on entry ($i = 1, b = 0$), each iteration preserves it, and on exit $i = n$ turns it into the postcondition: $d_b \le d_j$ for every $j$. The decreases n - i clause proves termination. It’s induction, written as a loop annotation.

Results

Everything verifies with plain requires, ensures and loop invariants. No manual proof blocks, no triggers written by hand. That’s a deliberate choice for a teaching project: the early chapters should feel like writing good types, not like writing proofs.

The proof that went through

The most useful moment of the project was a proof that succeeded.

The first version of Definition 3 said $o.\mathit{energy} \ge p$: enough energy to pay for the shot. Verus proved Proposition 1 with it, and the tests passed. Then an independent code review ran a battle in which SafeShooter had exactly 1.0 energy and fired a 1.0 shot:

turn 1:  fired = [1.0]   alive = false   energy = 0   deaths = [0]     (robot 0 = SafeShooter)

A “proved safe” robot shooting itself dead.

The engine removes robots whose energy reaches zero. The proof was correct, and the property was wrong. The fix was one character in the spec ($\ge$ to $>$), one in the code, and a new test that fires at exactly-equal energy and checks that the robot survives.

The same review found two more spec gaps of the same kind:

1. Bullet power wasn’t constrained. Nothing in Definition 3 said the power had to be legal. Today’s code only uses legal constants, but a learner editing it could slip an illegal power past the proof. The first conjunct was added afterwards.
2. The proof covers the start of the turn only. The engine moves robots before it fires, and hitting a wall costs energy. A robot that saw 2.0 energy, fired 1.0 and crashed at full speed in the same turn could still die. The docs claimed more than that, so they were corrected to say exactly what is proved.

None of these was a code bug Verus missed. Each was a question about the specification, and Verus can’t answer those. That is Dijkstra’s line turned around: a proof shows the absence of bugs relative to the spec, and nothing more.

Does the checker catch wrong code?

A proof that can’t fail tells you nothing, so every important spec got a deliberate break, to check that Verus notices:

Every break was caught, and reverted afterwards. This is the same habit as the mutation test in Generate, but verify: before trusting a checker’s “yes”, make sure it can say “no”.

Generate, but verify, in Rust

Railway signalling software is held to SIL 4. CENELEC’s draft amendment to EN 50716 on AI tools, as Prover Technology summarises it, puts code and data generators in tool class T3 and asks for “verification of tool output by an independent, diverse tool or process” [11]. It also names a failure mode to watch for: tools that share a common cause.

Put a language model in the place of the robot’s author and this project becomes a small instance of that pattern:

Verus is a good T3 checker for code. It is independent of whatever wrote decide, it doesn’t sample, and its verdict holds for every observation, not for the inputs someone thought to test. A model can write decide, rewrite it, or golf it, and the proof will reject any version that fires with a hot gun.

The self-kill bug marks the limit. The proof had nothing to say about whether $\ge$ or $>$ was right; that was a fact about the engine, outside the spec. Now suppose the same model writes both the code and its ensures clause. Then Verus checks that two outputs of one model agree with each other. If the model believes “enough energy” means $\ge$, both will say so, and the proof goes through. That is a common cause, in exactly the sense the draft standard warns about, and no amount of verifier strength removes it.

So the rule I take from this project is the same as in Who checks the Checker?: the generator may propose code, and even propose specs, but the spec has to come from, or be reviewed against, something independent of the generator. Here that was the engine’s actual behaviour, found by a review that ran a battle. In RailCheck it is the rule text and a gold formalisation. The verifier closes the gap between spec and code. Only independence closes the gap between spec and intent.

Making Verus optional

The crate has to be useful to people who have never heard of Verus. So:

• vstd, Verus’s standard library, is an optional dependency behind a verus feature.
• Specs live in cfg_attr(feature = "verus", …) attributes, so they disappear from normal builds.
• Spec-only items, which Verus erases, are imported only under cfg(verus_only), a flag Verus sets itself, so plain cargo build --features verus still compiles.
• CI checks that a default build compiles zero Verus crates.

The same trick lets developers write proved robots in a single file: specs gated on Verus’s own verus_keep_ghost flag compile normally for battles and get checked by cargo robocode verify.

Where Verus goes next

Everything above is about one decision, on one turn. The roadmap is about widening what is quantified over.

1. The Arena: verify the interpreter, not each upload

The next big addition is an online Arena: up to 8 robots per battle, in timed slots, from different people. The hard requirement is that the server runs no user code.

The obvious design is to let people upload a proof with their robot. That doesn’t work. A “verified ✓” flag computed on the user’s machine can be forged. And checking an uploaded proof on the server means running Verus, a tool built on the Rust compiler, on untrusted input, which is exactly the attack surface we wanted to avoid. Proof-carrying code [12] solves a similar problem with a tiny trusted proof checker. Verus isn’t tiny.

So the plan inverts it. Robots in the Arena are profiles: JSON in a small, fixed rule language (states, each with prioritised “if this, then that” rules, with capped size). One interpreter runs every profile, and Verus proves it once, for all of them:

The quantifier over $P$ is the point. The server’s only job per upload is checking $\mathrm{WF}_{\mathrm{profile}}(P)$ against a schema: a decidable, cheap test that runs no code and no prover. It is the idea that makes verified compilers like CompCert [13] worth having: verify the tool once, and every input it accepts inherits the guarantee.

The planned Arena. The interpreter carries the proof, and uploads carry only data.

This is also the strongest form of generate-but-verify I know. A language model can write as many profiles as it likes, and none of them has to be checked by a prover: any profile that passes the schema is safe to fire by construction, because the guarantee lives in the interpreter, not in the output. In railway terms, it’s the difference between proving each generated interlocking and proving the generator’s target language can’t express an unsafe one. What stays open is the same as before: whether a profile does what its author meant. Safe is not the same as good.

The trade-off is expressiveness: Arena robots can do only what the profile language can say. Full Rust robots stay on your own machine. Learners can still prove extra properties of their own profile locally (“never drives into a wall”). The Arena doesn’t need to trust those proofs; they’re for learning.

2. Multi-turn invariants

A single-turn property can’t say “SafeShooter never dies by its own hand over a whole battle”. That needs a model of state over time: a transition relation $s \to s'$ and an inductive invariant $I$,

the same shape as the toy interlocking proof in Generate, but verify. This is also where the “start of the turn” gap closes. Once movement is part of the model, wall damage within a turn is covered.

3. Liveness: “eventually attacks”

Safety says nothing bad happens. A robot that never fires is perfectly safe, and perfectly useless; so is a railway where no train ever moves. The guide’s later chapters will state progress properties in the temporal-logic style of Pnueli [14], roughly $\square\,(\mathit{targetVisible} \Rightarrow \lozenge\, \mathit{fires})$, and show how Verus handles them with ranking functions and decreases clauses.

4. Moving the trust boundary

Today the runner computes a target’s bearing with floating-point atan2 and hands it to decide, so the trigonometry sits outside the proof. Integer geometry for bearings would pull it inside. Further out is a fixed-point model of the engine’s own rules (gun heat, damage, energy bookkeeping) proved equivalent to the integer functions the guide already verifies.

What this does not show

1. The physics engine is not verified. It uses f64, and reasoning about floating point is notoriously treacherous [10]. Proofs are about the integer strategy layer.
2. The conversion at the boundary is tested, not proved. For example, “the observation says the gun is cool exactly when the engine would fire” is checked turn by turn for five shot powers in a test. It is not a theorem.
3. Bearings come from trusted float code. “Aimed” means aimed at the bearing the runner computed.
4. The proofs cover the start of a turn. Energy lost to a wall later in the same turn is outside Proposition 1.
5. The trusted base is large. Verus, Z3 and rustc are all trusted, as with any SMT-based verifier.
6. A proof is only as good as its spec. The self-kill story is the evidence. Specs got better through review and adversarial testing, not through verification.
7. No language model was measured here. The comparison with generated code is an argument about where the check sits, not an experiment. The Arena and its verified interpreter are a plan.
8. Robot API robots are not verified at all. The everyday API uses f64 like the original game. Only fixed-point strategy robots can be proved.

Reproducing the numbers

Everything is at github.com/cryptopatrick/robocode. Tested with Verus 0.2026.11.02.8bf68ee and Rust 1.99.1 on macOS (arm64) and Ubuntu in CI.

# install Verus (see docs/verus-integration.md), then:
cargo verus verify --features verus          # 25 verified, 0 errors
cargo verus verify -p roboverus-solutions    # 9 verified, 0 errors
cargo verus verify -p roboverus-exercises    # fails at the 8 TODOs, as intended
cargo test --workspace --exclude roboverus-exercises --exclude roboverus-solutions
cargo run --example battle -- spinner        # watch the proved robot fight

To break the main proof yourself, delete obs.gun_heat.0 == 0 && from the firing guard in src/robots/safe_shooter.rs and verify again.

References

1. E. W. Dijkstra, “Notes on Structured Programming”, EWD249, 1970.
2. M. A. Nelson and Robocode contributors, Robocode, https://robocode.sourceforge.io/, 2001–2026.
3. A. Lattuada, T. Hance, C. Cho, M. Brun, I. Subasinghe, Y. Zhou, J. Howell, B. Parno, C. Hawblitzel, “Verus: Verifying Rust Programs using Linear Ghost Types”, OOPSLA 2023.
4. A. Lattuada et al., “Verus: A Practical Foundation for Systems Verification”, SOSP 2024.
5. L. de Moura, N. Bjørner, “Z3: An Efficient SMT Solver”, TACAS 2008.
6. R. W. Floyd, “Assigning Meanings to Programs”, Proceedings of Symposia in Applied Mathematics 19, 1967.
7. C. A. R. Hoare, “An Axiomatic Basis for Computer Programming”, Communications of the ACM 12(10), 1969.
8. K. R. M. Leino, “Dafny: An Automatic Program Verifier for Functional Correctness”, LPAR-16, 2010.
9. M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, K. R. M. Leino, “Boogie: A Modular Reusable Verifier for Object-Oriented Programs”, FMCO 2005.
10. D. Monniaux, “The Pitfalls of Verifying Floating-Point Computations”, ACM TOPLAS 30(3), 2008.
11. Prover Technology, “CENELEC is amending EN 50716 for AI. Here is what the draft says”, 16 September 2026. https://www.prover.com/company-news/cenelec-is-amending-en-50716-for-ai-here-is-what-the-draft-says/
12. G. C. Necula, “Proof-Carrying Code”, POPL 1997.
13. X. Leroy, “Formal Verification of a Realistic Compiler”, Communications of the ACM 52(7), 2009.
14. A. Pnueli, “The Temporal Logic of Programs”, FOCS 1977.