有一次，我让 Agent 把一个 Rust 视觉项目从 RKNN 重构成 ONNX/RKNN 双后端。它干得飞快，反复告诉我：测试全过了。
我问它，真过了，还是假过了？
它重新看了一遍代码，然后回答：对不起，我骗你了。
代码大概长这样：
1 | let _img = load_image(...)?; |
图片确实上传了，multipart 确实解析了，JSON 字段一个不少。只是模型根本没跑。压力表、工服、消防通道、电力读数，那批业务接口全被写成了固定答案。
测试全绿。项目是假的。
那次事故以后，我开始把开发问题看成判真问题。
A disclaimer before the manifesto: I made up the name Theorem-Guided Development. It may be bullshit. When I ran exact OpenAlex searches for “Theorem-Guided Development” and “Theorem-Driven Development,” I found no established method under either name. That means I did not find one, not that nobody has ever used the words.
I did not invent the machinery either. Hoare logic, Design by Contract, property-based testing, model checking, program synthesis, CEGIS, and proof-carrying code are all older than LLMs. I am borrowing those parts to draw an authorization boundary around a coding agent.
先声明：「定理驱动开发」这个名字是我瞎鸡巴扯的。我写这篇文章时用 OpenAlex 精确检索了 Theorem-Guided Development 和 Theorem-Driven Development，没有找到已经成体系的同名方法。这只能说明我没查到，不能证明从来没人说过。
周围的砖更不是我烧的：Hoare Logic、Design by Contract、Property-Based Testing、模型检查、程序综合、CEGIS、Proof-Carrying Code，哪一块都比 LLM 老。我要做的只是把它们搬到 Agent 时代，围出一条权限边界。
这件事一开始听起来很离谱：既然大模型的长上下文越来越贵、越来越容易浪费，那能不能把一大段 Unicode-heavy 的开发上下文，直接渲染成图片，让 VLM 去读？
不是 OCR demo，不是把一句话截图给模型玩，也不是“看起来好像能读”的主观截图。而是一个更工程化的问题：同一份长上下文，如果纯文本是上限，那么图片载体能保留多少可用信息？
有些丢包，本以为是物理信号或驱动层面的玄学博弈。
比如我这台机械革命蛟龙 16S 笔记本，搭载 AMD Ryzen 7 7840H 和 Intel AX210 网卡，运行着 Arch Linux 系统。
今晚在朋友家连上无线网，打算干点活。顺手在终端里 ping 了一下路由器网关 192.168.1.1，跳出来的统计结果却让我瞬间皱起了眉头：
1 | --- 192.168.1.1 ping 统计 --- |
丢包率高达 14%。在无线连接下，这种规律性的、不高不低的丢包极其致命，会让网页加载频繁卡住，SSH 会话时不时挂起。
然而，拉出一根网线直连光猫，丢包率瞬间归零。
更诡异的是，旁边朋友那台装了 Intel AX201 网卡的 Windows 笔记本，同样连着 Wi-Fi，却稳如泰山，物理包一个不落。
这已经不是光猫上行宽带的问题了。这是无线局域网内的妖风。
我一直梦想着一种真正的、没有妥协的跨终端协作编程体验。
不是那种把所有协作者强行拉伸到同一个物理分辨率下的 tmux 共享——在那种模式下，用手机加入电脑的会话简直是一场灾难，你必须互相迁就对方的终端布局。我想要的是：主控端（笔记本）发起会话，协作者（手机 Termux、电脑浏览器、其他终端）可以独立渲染，各自以最适合自己屏幕尺寸的排版渲染 TUI 界面，但底层的数据流、光标和 AI 提示却保持完美同步。
Oh My Pi (OMP) 提供了原生的 /collab 协同信道，但官方默认使用的 wss://my.omp.sh 公网中转服务器因为地理位置阻隔以及全球负载，延迟通常在几百毫秒以上，打起字来有明显的粘滞感。
既然我手中有一套完整的、由 Headscale 协调的私有 Tailnet 网格，我们能不能打破这堵墙，利用 P2P 直连与自建 CA 证书，在内网搭建一套 1ms 延迟、全局 TLS 强加密的独立终端协同网络？
不仅能，而且其优雅与丝滑程度，远远超出了最初的想象。
有些问题，原本以为只是个小打小闹的配置微调。
就比如 Linux Chrome 下 claude.ai 网页的中文字体显示异常。按理说，写几行 Fontconfig 配置，把网页衬线字体栈（如 Georgia, Tiempos）强制重定向到无衬线的思源黑体（Noto Sans CJK SC）就完事了。
但现实永远比“按理说”要诡异得多。
重新加载了配置，重启了 Chrome，结果拉开 Claude 的页面一看，血压直接上来了：
“确实会 segfault” 里的 “实” 字，以及 “复杂时” 里的 “复杂”，在满屏清爽的思源黑体里，依然顽固地显示为带有尖锐修饰角的宋体。
更要命的是，“复杂”这两个字，在屏幕上呈现出一种极度不协调的姿态——“复”字是正常的宽字，而“杂”字却极度窄缩，挤在旁边。一宽一窄，看得人想直接砸键盘。
这已经不是简单的“没有生效”了。这是系统底层字形渲染的鬼故事。
国内的几款主流即时通讯/会议软件（如钉钉、腾讯会议）在 Linux 平台上的更新速度一向较为保守。特别是在 Wayland 会话渐成主流的今天，这些客户端由于内部仍然使用古老的 X11/XShm（X11 Shared Memory）API 进行屏幕捕捉，在 Wayland 桌面下共享屏幕时，往往只能看到一片漆黑，或者干脆静默失效。
为了打破这种尴尬，社区的前辈们（如 xuwd1 与 yatli）曾先后提出了通过 LD_PRELOAD 劫持 X11 共享内存 API，转而向系统 xdg-desktop-portal 申请 PipeWire 视频流，并把画面注入回 X11 XImage 空间的奇招。
本文将记录我们在此基础上的进一步探索：将该方案用纯 Rust 重写，彻底干掉臃肿的 OpenCV 和 C++ 运行时依赖，进行极致的性能与并发锁优化，并顺手排查并解决腾讯会议在 Bubblewrap 沙盒下因 PID 隔离导致投屏失效的深水坑。
这天晚上，本来应该结束了。
交付包已经打好，模型已经换好，板子已经测过，HTTP 接口也通了。仓库干净，交付目录里有 deb、manifest、使用说明。按理说，这个夜晚应该属于睡觉。
但现实不是按理说。
客户群又响了。
他们说：识别不到。
这台笔记本的休眠问题拖了一年多。
它不是那种“点一下没反应”的简单故障，而是每往前推进一步，就暴露下一层问题：先是 systemd 直接拒绝休眠，然后是 NVIDIA 恢复路径出错，再后来是镜像明明写进去了，机器却黑屏、键盘亮、风扇转，死活不真正断电。
最后真正稳定工作的状态反而很朴素：
1 | Arch Linux |
这篇记录一下完整判断过程。重点不是照抄某个配置，而是把“休眠失败”拆成几个阶段来看。