---
title: "Proving the promises"
description: "Evil Engine's design promises now live in Lean, so a decision that breaks one fails the check. Here's how it's set up, what it caught, and what it can't do."
url: "https://evil-engine.com/devlogs/proving-the-promises"
published: "2026-11-01T04:30:00.000Z"
modified: "2026-11-01T04:30:00.000Z"
---

Devlogs

2026-10-31 21:30 MST

# Proving the promises

Evil Engine's design promises now live in Lean, so a decision that breaks one fails the check. Here's how it's set up, what it caught, and what it can't do.

---

Evil Engine makes a lot of promises. Every playermodel from every mount shows up in the picker. Two players with the same game can join the same server, whatever else they’ve installed. Nothing a server sends can touch your files. Plugins only ever add, they never take away.

Each of those gets written down in a scope before any code exists, which I went over in [Starting over on purpose](https://evil-engine.com/devlogs/starting-over-on-purpose). There are a few dozen scopes now though, and a decision in one can quietly break a promise made in another. Rereading all of them after every change doesn’t scale, and I don’t trust myself to catch everything anyway, so the promises live in Lean now too.

## Lean

Lean is a programming language you can also write proofs in. You state something, like “after any sequence of patches, everything that was listed is still listed”, then prove it, and if the proof has a hole it doesn’t build. It’s a bit like a compiler refusing code with a type error, except what it refuses is an argument that doesn’t hold up.

It started on October 31 as a small test of three of the laws, about 200 lines, to see if it was worth doing at all. Against the design as it stood, all three came back broken. Two of those had already come up in a review of the scopes, which was a good sign the model was reading the design right, and the third was one I’d missed completely.

## How it’s set up

The Lean lives beside the docs rather than replacing them, so the docs are still what I read and edit. Each law is a definition of what has to hold for every game, every machine and every Plugin. Each scope’s design is its own module, written straight from what the scope says. A theorem then either proves the design keeps the law, or proves it doesn’t by producing the case that breaks it. Every time a scope changes, everything gets rechecked against every law.

Here’s law 10, “everything is listed”:

```
def Law10 (apply : Op → List Record → List Record) : Prop :=
  ∀ base (ops : List Op), ∀ e ∈ listings base,
    e ∈ listings (ops.foldl (fun reg o => apply o reg) base)
```

Start from any records, apply any sequence of patches, and anything that was in a menu before is still in a menu after.

Games don’t get proofs of their own. The laws are stated for every game, so a game is just one more value they already cover, and a new mount only grows the model if it brings a kind of rule the records store hasn’t seen yet.

Some decisions don’t need a theorem at all. A converter is typed so it only ever sees its own game’s files, so the old design where it peeked at your other mounts can’t even be written.

It’s 123 theorems in about 2,500 lines so far, across 17 scope modules, with no unfinished proofs and no extra libraries.

## What a broken design looks like

When a design breaks a law, the proof is an example of it breaking. Here’s Kleiner the way Garry’s Mod’s records describe him, a person with a `player` table, which is what puts someone in the playermodel picker:

```
def kleiner : Record :=
  ⟨"gmod:kleiner", .person, [⟨"player", "table", "lua/includes/modules/player_manager.lua"⟩], []⟩

theorem removePlayer_breaks_law10 : ¬ Law10 Patch.applyUnguarded := by
  intro h
  have := h [kleiner] [.removeKey "gmod:kleiner" "player"] ("gmod:kleiner", .playermodels)
    (by simp [listings, menusOf, kleiner, Record.hasKey])
  simp [listings, menusOf, kleiner, Record.hasKey, Patch.applyUnguarded, edit, dropKey] at this
```

The `¬` means “not”, so this says patches as I first designed them don’t keep law 10\. The proof assumes they do, applies one patch that removes Kleiner’s `player` key, and looks in the picker, where he isn’t anymore. That contradicts the assumption, so the theorem holds.

Some of them are a lot smaller. The movement scope had Garry’s Mod’s player hull as 0.81 m wide, and in tenths of a millimeter that’s checked like this:

```
theorem roundedHull_misses_the_oracle : ¬ (32 * 254 - 8100 ≤ 10) := by decide
```

32 units is 812.8 mm, and the test the scope is held to only allows 1 mm of slack, so the rounding didn’t fit. `decide` just means Lean works the arithmetic out itself.

## What it caught

A good chunk of the design proved as written. A Plugin running its own 60 Hz step inside a 66-tick server steps exactly 60 times every 66 ticks and never drifts, as long as its clock counts in whole units of time instead of floats. Every Plugin listening for an event hears it whatever the others answer, where the first version’s events stopped at the first handler that returned anything, so a shield Plugin could hide damage from an armour Plugin after it.

The rest didn’t hold up:

- Patches could remove a mount’s record outright, so `remove = true` on Charple took it out of every menu. Hiding is its own key now, and only folds an entry away
- Even after that, `remove = ["player"]` took Kleiner out of the playermodel picker, as above. Patches can’t remove a key that decides which list a record is in anymore
- Hashing one registry of everything you’d mounted meant a single extra Workshop addon gave you a different session key than the server, which is why there are two registries now
- “Every skinned, animated model is a person” turned Garry’s Mod’s ragdoll Kleiner into a person. Now only what a game lists as a body gets sorted
- Joining on a game’s build fingerprint meant a player who updated Garry’s Mod between sessions couldn’t join. Joining compares the files the server actually needs instead
- Two Plugins that each need the other’s API could load with one running before the other’s API existed. Cycles get refused now, except for two Plugins that only want each other, which both load
- Lean only accepts a function it can see will finish, so events raised inside events needed a depth limit before they could be modelled at all. That raised the question of what happens at the limit, and as written they got dropped silently. They’re still dropped, but with a note naming the Plugin that raised them
- A client-only Plugin sending inputs shifted the command numbering on just that one machine, so only Plugins on both sides send inputs now
- The player hull rounding above, which the scope now gives exactly as 0.8128 m
- Animation clips with no ground speed would’ve had feet sliding, so in-place clips measure it from their planted feet now
- A map’s own sounds were laid over the shared registry, so changing maps could change the session’s hash. Maps keep their records in a layer of their own now, which goes away with the map

All of those got fixed in the docs, and the fixes got proved. The broken versions stay in as theorems too, so I can’t wander back into one later. It does mean the list of theorem names reads a bit like a list of my mistakes XD

## Keeping the docs honest

A proof is only worth something if it proves what the docs actually say. A second step builds a page that puts each law, quoted word for word from the docs, beside the Lean that states it and the theorem that proves it. It covers the twelve laws plus nine promises from the scopes that the laws lean on, like load order, trust and events, and under each one go the earlier designs it caught. If a quoted line changes without its proof changing too, the check fails.

## What it can’t do

This proves the design, and not the C# code, so the code can still get the design wrong. A theorem is also only as good as how it’s stated, so if I write a law down wrong, Lean will happily prove the wrong thing. It can’t check anything about one game’s files either, like whether a converter reads a model correctly, which stays in regular tests over real installs. It also can’t catch problems that aren’t logic, like a missing scope or a legal question, so I still read everything myself.

## What’s next

The plan is for the spec to write out test cases (registries, patch sequences, join attempts) that the engine’s own tests replay, so the C# gets checked against the same design the proofs cover. That needs a records store to test against first, so it’ll come once the store is built. Until then, any change to a scope has to get past the proofs before it goes in.

Older

### [Starting over on purpose](https://evil-engine.com/devlogs/starting-over-on-purpose)

## Details

- **Written**: 2026-10-31 21:30 MST
- **Edited**: 2026-10-31 21:30 MST

## Contents

- [Lean](https://evil-engine.com/devlogs/proving-the-promises#lean)
- [How it’s set up](https://evil-engine.com/devlogs/proving-the-promises#how-its-set-up)
- [What a broken design looks like](https://evil-engine.com/devlogs/proving-the-promises#what-a-broken-design-looks-like)
- [What it caught](https://evil-engine.com/devlogs/proving-the-promises#what-it-caught)
- [Keeping the docs honest](https://evil-engine.com/devlogs/proving-the-promises#keeping-the-docs-honest)
- [What it can’t do](https://evil-engine.com/devlogs/proving-the-promises#what-it-cant-do)
- [What’s next](https://evil-engine.com/devlogs/proving-the-promises#whats-next)

## Stay up-to-date

- [RSS](https://evil-engine.com/rss.xml)
- Mailing list
- [Steam](https://store.steampowered.com/app/3731310/Evil_Engine)