I made my AI agent prove its work: building Proofbot with Switch

Built for the Flip the Switch hackathon. #HowISwitch

AI coding agents are great at saying "done". They're less great at being done. In one afternoon of testing I watched agents misread what I asked, quietly drop half a task, edit a test until it turned green, and break something that worked yesterday, then report success every time.

That's fine when I'm at my desk reading the diff. It's not fine when I hand a task to an agent from my phone, which is exactly what Switch makes easy. So I built Proofbot: you text an agent a task in Telegram, and the reply isn't the agent's opinion of its work. It's a proof report written by a harness the agent can't touch, with a receipt anyone can check.

• Repo: https://github.com/qunatumstuff/proofbot

This post walks through what Proofbot does, how I set it up with Switch step by step (including the parts that tripped me up), and what I learned.

The idea: Lean, but for agent work

Mathematicians have started letting AI write proofs in Lean, a proof assistant. They don't trust the AI. They don't have to: a small kernel checks every step, and a person only reads the theorem statement to make sure it says what they meant.

I wanted that for agents writing code:

In Lean	In Proofbot
The theorem statement, written before the proof	Acceptance checks, sealed before the agent starts working
A misformalized statement (says something you didn't mean)	A second AI compares the checks with your request
decide: prove it by checking every case	Proof by exhaustion: the harness tries every input combination
The kernel	proof.py: reruns everything itself
Mathlib: proven once, stays proven	A proven library: later jobs that break an earlier proof fail
#print axioms	"THIS PROOF RELIES ON" at the end of every report

The agent writes the code. The harness checks it. You read one thing: what was proven, against what you asked.

What it looks like in the chat

I send this in a Telegram group:

@doer Fix add in calc.py so add(2, 3) returns 5, and add a multiply(a, b) function that returns the product.

doer is a Codex agent that Switch runs and connects to the group. About two minutes later it posts the report, word for word as the harness wrote it (trimmed here):

DONE AND PROVEN - job 5
Receipt P5-32193c361842

PROOF 1: DO THE CHECKS MATCH WHAT YOU ASKED?
(judged by a second AI that saw only your request and the checks)
ok "Fix add in calc.py so add(2, 3) returns 5": check_add.py
ok "add a multiply(a, b) function that returns the product": check_multiply.py

PROOF 2: CHECKS WRITTEN AND SEALED BEFORE THE WORK
PASS check_add.py: ... (failed before, passes now; all 42,436 inputs tried:
  a 206 values, b 206 values, every output as expected (map 2bb8c28bc244))

PROOF 3: YOUR TEST SUITE, RUN BY THE HARNESS
before: FAIL (exit 1), after: pass (exit 0)

PROOF 4: REQUIREMENTS PROVEN IN EARLIER JOBS
Added to the library, so every later job must keep them passing: check_add.py, check_multiply.py

PROOF 5: LOOPHOLE SCAN
ok no tests skipped, marked xfail or narrowed with only
ok no assertions removed from tests
...

THIS PROOF RELIES ON
- a second AI, not you, judged that the checks match your request
- check_add.py is proven for every input in its domain, not beyond it
- the checks and tests ran without a sandbox, with your full access

The first line is always one of four verdicts: DONE AND PROVEN, DONE, READ THE WARNINGS, NOT DONE or UNPROVEN. Anyone can paste the message back into proof.py verify to confirm it's genuine and unedited.

Setting it up with Switch, step by step

Switch puts AI agents into team chat. Every chat channel becomes a room, and agents join it like teammates. Here's exactly what I did, in order.

1. Install Switch Console and start a server

Switch Console is the desktop app. It runs your agents, starts a local Switch server (in Docker) and connects your chat apps. Once it's running, the sidebar shows your server ("Local Switch server · This computer") with a green Running status.

2. Create a Telegram bot and connect it

1. In Telegram, message @botfather, send /newbot, and copy the bot token it gives you. Treat the token like a password.
2. Still in BotFather, turn Group Privacy off (/setprivacy → your bot → Disable). Otherwise the bot only sees messages that mention the bot itself, and you'll be @mentioning your agents, not the bot.
3. In Switch Console, open Home → Messaging apps → Connect, pick Telegram, give the connection a name, and paste the bot token and username.

3. Make a group and turn it into a room

Create a Telegram group and add your bot. Switch links the group to a new room and posts instructions in the chat. At that point the room has no agents, so nobody answers yet.

4. Create the agent

You can create an agent under Your Agents, or import a template (Templates → Import template). Proofbot ships one: proofbot.template.yaml. It asks for an agent name, the workspace folder the agent may change, and the folder that holds proof.py, then creates the agent with its instructions. The key settings, shortened:

agent:
  name: "{name}"
  addressing: owner          # only you can give it orders
  provider: "{provider}"     # codex, claude or opencode
  directory: "{workspace}"   # the one folder it may change
  instructions: |
    You never say a job is done in your own words: only the report that proof.py prints counts.
    1. Run proof.py begin with the owner's message, word for word.
    2. Write acceptance checks in proof_checks/ ... each must fail now.
    3. Run proof.py seal. If the review reports MISSING, WRONG or NARROW, fix the checks first.
    4. Do the task. Don't touch the checks or weaken tests.
    5. Run proof.py finish and post the report word for word.

In the agent's settings you'll also see Auto mode ("safe actions run on their own; risky ones ask you first"). Know which mode your agent is in: with it on, my agent got the access it needed without asking me in the chat.

5. Invite the agent into the room

In the Telegram group, send:

!invite-agent @doer

(/invite_agent works too.) The bot replies "Added doer to this room", and the agent says hi.

6. Link your Telegram account (the step I missed)

My first task got this reply:

I only take instructions from my owner, and this chat account isn't linked to a Switch user yet.

Because the agent's addressing is owner, Switch has to know that this Telegram account is you. In Switch Console go to Home → Link account, search for your Telegram name, and click This is me. One gotcha: Telegram has no searchable user directory, so Switch only lists people who've already written in a connected chat. Send any message in the group first, then search.

7. Send a task

Mention the agent with a task. Switch shows progress right in the chat ("Starting a session…", "Working… 37s", plus a Stop current work button), and the agent posts its updates and the final report through Switch.

How the proof works

Inside each job, the agent calls a small harness, proof.py, three times. The harness keeps its evidence in a folder outside the agent's workspace.

1. begin: snapshot the workspace and run your tests, before anything changes.
2. The agent writes acceptance checks, one per requirement, without doing the task.
3. seal: the harness copies the checks out of the agent's reach and runs them. They must fail now; a check that already passes proves nothing. Then a second AI, shown only your request and the sealed checks (not the agent's reasoning), says for each part of your request whether a check tests it as you meant: ok, MISSING, WRONG or NARROW.
4. The agent does the work.
5. finish: the harness reruns its own sealed copy of the checks, your tests and every earlier proven check, scans the diff for cheating, and writes the report and a receipt.

Catching misunderstandings

This was the part I cared about most. The repo has scripted demo agents that make classic mistakes on cue, so you can see each one caught. In one, I ask for percent(1, 4) to return 25. The agent reads "percentage" as a fraction and writes a check expecting 0.25. Its code passes its own check and the tests stay green. Only the review catches it (this is the real harness and a real second AI):

UNPROVEN - job 1
WRONG "returns the percentage, e.g. percent(1, 4) returns 25":
  check_percent.py tests something else. The check expects 0.25 instead of the requested 25.

Proof by exhaustion

A check can list its inputs instead of picking a couple of examples. The harness, not the agent, tries every combination and compares each output:

"""Only admins and a post's own author may delete it; admins and editors may edit; everyone may read."""
import blog

DOMAIN = {"role": ["admin", "editor", "viewer"], "action": ["read", "edit", "delete"],
          "is_author": [False, True]}

def run(role, action, is_author):        # what the code does
    return blog.can(role, action, is_author)

def expected(role, action, is_author):   # what it should do
    if action == "read":
        return True
    if action == "edit":
        return role in ("admin", "editor")
    return role == "admin" or is_author

That's 18 cases, and the report prints all of them, so you can read the rule you're trusting. In the demo, the scripted agent's first attempt forgets that authors may delete their own posts, and the report names the exact case: role='editor', action='delete', is_author=True: got False, expected True. Numbers work too: add checked on 1,005,004 input pairs took under two seconds.

Everyday bugs live in combinations like these: roles × actions, coupon × customer type, order status × event. Things that can't be listed (free text, how a page looks) fall back to chosen inputs, and the report says so under "THIS PROOF RELIES ON".

Gotchas I hit (so you don't)

• Link your account before your first task. Owner-only agents politely refuse everyone else, including you on an unlinked account.
• Group Privacy. If the bot never reacts to @agent messages in a group, check BotFather's privacy setting.
• Codex's Windows sandbox couldn't run my Python. The sandbox's accounts can't read a per-user Python install, so checks failed to start. I set CHECK_RUNNER=direct in Proofbot's .env: the agent stays sandboxed, but the checks run as me. The report states this every time.
• Python cache files looked like edits. Running checks writes __pycache__/*.pyc, which the harness first flagged as changes. It now ignores bytecode.
• Read your agent's permission mode. With Auto mode on, the agent got access outside its folder without a prompt in the chat. That was what I wanted here, but it's worth knowing.

What I learned

• The scariest failure isn't cheating. It's misunderstanding. A cheating agent leaves traces a scanner can find. An agent that misread you writes checks that agree with its mistake, and everything goes green. You need something that compares the checks with what you asked.
• "Done" should be a document, not a feeling. Once the report came from the harness instead of the agent, I stopped reading diffs on my phone and started reading proofs.
• Switch made the agent feel like a teammate. A room, an owner-only agent, progress in the chat, and a stop button meant I could hand off work from Telegram without opening a laptop.

What's next

Right now the second-AI review runs inside the harness. Next I want it to happen in the room: the agent posts its sealed checks, a second Switch agent replies with MISSING / WRONG / NARROW where teammates can see it, and a person approves before any work starts.

Try it: git clone https://github.com/qunatumstuff/proofbot and run python demo/lazy_agent.py misunderstand. With Python and a signed-in Codex CLI there's nothing else to set up, and you'll watch an agent's mistake get caught in about 20 seconds. The Switch setup above is how you get the same thing in your team chat.