系统 · 设计，不在任何发布里
LSPE
每一次构建，都是对程序的一串判断。LSPE 让编译器为这些判断给出依据：它先为每一个判断找来源， 找不到就把一个会被记录的问题交给你，并把这次往来写进产物。它不承诺你的程序是对的。 它承诺的是没有一次放行是无声的。
这是一个设计，不是能下载的东西
截至 2026-10-18，LSPE 是一个设计。没有任何一个发布包含它，没有东西可以安装，这一页也不写
它会在哪天到来。设计本身写在仓里的 docs/262 —— 和其它带编号的设计文档一样是
中文的，这个项目把计划放在那里，而不是放在公开的 issue 追踪器里。
下面说的是这个设计为了什么，以及它拒绝声称什么。它不是一篇"某个功能可以打开了"的公告。
设计不是承诺。 有两件事已经知道做不到，设计把它们写下来，而不是绕开： 没有编译器能证明一个程序没有缺陷，也没有编译器能回答它自己答不出的每一个问题。 下面每一条都由这两件事塑形。
每一个判断都有一张小票
今天的编译器只给你一位信息：接受，或者拒绝。理由留在编译器里，而它为了走到"接受"所做的 假设，没有写在任何你能查的地方。
LSPE 加一份记录。每当编译器放行一件它证明不了的事，产物就记下：那是哪一个判断、依据了 什么证据，以及 —— 如果是人回答了一个问题 —— 是谁回答的。产物里带的是这份记录的哈希； 推导树留在产物旁边、不进产物，所以产物不会因为它而变大。
这不是"没有缺陷"。 一个程序有没有缺陷，编译器判不了；每一次放行有没有 被写下来，判得了。前者不可判定；后者是过程的一条性质，可以由一个不信任这个编译器的人， 事后离线核对。
四件东西
LSPE 是四件东西，作用在同一个空间里：一个单元里做过判断的站点、这些站点背着的义务、 支持它们的证据，以及每一格最后怎么了的记录。它不是第五套检查器 —— 检查器都留在原地。
质疑器
编译器不再只是判定者。在接受一个判断之前，它先为它找来源、试着构造反例，并拿去和 另一套实现对照。三样都失败，它就有一个洞 —— 而且它说的是自己有洞， 不是你的代码有问题。
反问器
一个洞会变成一个带选项的问题：每个选项的默认值是什么、选了会有什么后果。你的回答 会被记录。没有记录的推迟本身就是编译错误 —— 于是"我知道这里可疑，但说不清为什么" 不再只活在某个人的脑子里。
警察 LSPC
在构建之前，它把账单递给你：你接下来要接受哪些残余风险，一行一族，并写明这一族 不成立时会怎样。它默认不拦。你想修的修，不想修的留着，而你留下的那部分会被记下来。
台账
其它安全组件做出的判决 —— 回收梯、内存安全等级、能力域、所有权 —— 都汇到同一本台账里。 那些组件一个都不替换、不改名；台账是它们的判决可以放在一起读、互相对账的地方。
举证责任换了方向
通常的编译器站在程序之外，宣布一个结果。LSPE 站在交易之内：它点名自己的依据，给自己 做的假设标价，再递给你一张小票。它证不出来的时候，不可以说"你的代码有问题"；它必须说 "我的证明在这里有个洞"。前者是对你的主张，后者是对编译器的主张 —— 这两件事被刻意分开。
这个分开有代价，设计认这笔账：质疑器给每一次类型替换留日志，并在每次替换之后把义务重新 证一遍。Rust 自己的记录里就有一条正是这个形状的健全性缺陷 —— 一条在替换前成立的检查， 替换之后没有再跑。只问"有没有来源"的编译器抓不到它，因为来源当时存在，只是过期了。
店员不是权威。 语义归标准、归各个组件。LSPE 记录判断并给它标价； 它不决定什么是真的。