证据 · 933196B · 2026-10-15

v0.9.0 实现了什么，又没有证明什么。

每项证据都有状态、范围和复核日期。

v0.9.0对应提交933196b，于2026年10月11日在91项发布作业通过后发布。10月15日审阅覆盖安装脚本、五个原生目标、路由约定、诊断改进及独立限定的源码扩展。下表区分可执行子配置、局部测量与待完成门槛。

semaprax://evidencev0.9.0

entity     Semaprax
status     Beta 测试版
snapshot   933196b
authority  github.com/wavect/semaprax

Semaprax 目前实现了什么？

Beta发布五份原生归档并验证安装流程。标签包含语义修改、源码定律、类型化Agent、选定Rust/Wasm边界、策略路由、受保护开发流程及有界命令与数据配置。完整目标矩阵仍为55项Partial、0项Implemented、0项Missing。学习型路由尚未取得资格，原生Project测试仍有当前提交待验证门槛，公共泛型仍不支持且未发布。

能力证据台账

完整产品状态 55 部分 · 0 已实现 · 0 缺失

部分规范源码与稳定身份
部分受限上下文与紧凑投影
部分语义修改，而非任意重写
部分受控发布是独立边界
部分可重放的语义证据
部分多模块项目与离线脚手架
部分解释器、原生与 Core Wasm 执行
部分有界标量 JavaScript/TypeScript 导出
部分类型化运行时智能体
部分所有权与可重放清理
部分更广的日常编程能力
部分预算、持久恢复与模型调用
实验性应用与经济智能体实验
开发者预览生成边界仍按配置限定
路线图广泛原生与应用支持
路线图通用双向生态互操作
已演示签名发布来源证明
开发者预览编译器生成的泛型目标边界
开发者预览显式启用的原生与 Wasm 智能体阶段
实验性有界源码 yield 与持久化续体
实验性本地签名 Registry-v3 信任检查
已演示固定版本 Lean 证明与义务门槛
部分源码定律与证明重放
开发者预览丰富的原生 Rust 集成
开发者预览同线程 Rust Future
实验性连接编译器的开发工具
开发者预览经检查的开发热重载
部分上下文、token 与任务成本核算
部分无需克隆即可安装
实验性解释模型与工具选择
部分仅在已确认回合之间切换
部分更精确的修复指导
部分受限命令与数据配置
已演示保留不利的证明结果
部分加固开发工具边界
部分严格JSON与有界ASCII模式
开发者预览原生Project测试门槛仍待验证

当前状态	源代码状态	证据与来源	发布状态	支持范围	证据
规范源码与稳定身份 `stable-semantic-program-graph`	部分	确切标签的 Project 与 Rust 作业通过准入语义图契约；完整语义基础目标仍为部分完成。	有界 beta 源码/工具链配置	可读 `.spx` 仍是 Git 中的规范表示。显式 `@id` 在受支持的显示名称修改后继续标识同一声明。修订绑定规范源码和编译器隐式 prelude，而非偶然的源码位置或图传输格式。	GitHub 仓库
受限上下文与紧凑投影 `bounded-agent-context`	部分	已实现范围明确的类型化上下文、紧凑重放，以及已提交的本地分词器比较。	有界 beta 源码/工具链配置	选择确切的图或任务上下文，并限制深度、方向、节点数和字节数。model-text v2 在部分大型输入上减少 token，在小型输入上则会增加；报告保留分词器与比较边界。	GitHub 仓库
语义修改，而非任意重写 `revision-bound-semantic-patches`	部分	确切标签的源码修复与 Project 作业通过有界修改契约；任意仓库重写不在范围内。	有界 beta 源码/工具链配置	检查上下文、派生候选、预览影响、审阅、重放检查，然后显式授权应用。操作家族已超出重命名，包含有边界的表达式替换、结构修改及指定的 rebase/merge 组合。各协议保留独立的修订、身份与操作限制。	GitHub 仓库
受控发布是独立边界 `managed-workspace-semantic-operations`	部分	Project 产品验收在 Linux、macOS 与 Windows 通过；发布仍需显式授权。	有界 beta 源码/工具链配置	受管工作区代、候选证据、Project 修订存储与 MCP 工作流保留显式写入和发布权限。多文件验证不等于任意原始路径、Git 或编辑器的原子更新。Rust 嵌入 API 提供输入上限、取消与不透明会话，并非无限制宿主访问。	GitHub 仓库
可重放的语义证据 `semantic-evidence-capsules`	部分	修订绑定证据已实现且发布声明核对通过；回执不授予修改权限。	有界 beta 源码/工具链配置	证据将已检查事实与候选修改绑定到源码和修订。回执可支持审阅或拒绝，但不会授予执行、修改或发布权限。	GitHub 仓库
多模块项目与离线脚手架 `bounded-multi-file-project`	部分	Project Manifest、产品验收及已安装工具链旅程作业通过；服务宿主范围另行限定。	有界 beta 源码/工具链配置	清单定义声明的源码、入口、测试与导出。内置计算器、库和服务模板各有其配置。new 使用编译进工具的文件创建全新项目；源码检查、解释执行测试与目标构建遵循选定清单的契约。	GitHub 仓库
解释器、原生与 Core Wasm 执行 `native-and-wasm-lowering`	部分	五个平台归档与选定原生/Wasm门槛通过，各运行时配置仍保留独立准入限制。	有界 beta 源码/工具链配置	已获准的标量、拥有所有权数据、泛型、集合和不可变列表配置，可通过解释器、原生 C11/Clang 与 Core Wasm 执行，并各有一致性检查。显式启用的智能体阶段宿主单独绑定；普通 yield 仍不允许生成原生/Wasm 输出。	GitHub 仓库
有界标量 JavaScript/TypeScript 导出 `public-wasm-scalar-exports`	部分	确切标签的 Chromium 标量导出作业通过；其他浏览器与拥有数据包另行处理。	有界 beta 源码/工具链配置	稳定 ID 标量导出具有独立公共 Wasm 配置和浏览器测试样例。拥有数据包、广泛浏览器支持、组件及泛型签名各有契约，不能继承这一支持声明。	GitHub 仓库
类型化运行时智能体 `bounded-agent-runtime`	部分	AGENT-06 生命周期与客户端作业已在 Linux、macOS 和 Windows 上通过。默认在线路径仍选择解释器；显式启用、由调用方持有的目标宿主具有独立且范围明确的证据。	有界 beta 源码/工具链配置	类型化源码角色驱动初始化、观察、模型提案、授权、副作用与归约。绑定的 Proposal 模式约束解码。默认在线路径使用解释器；选定库路径可提供持有的原生 C11/Core Wasm 阶段宿主，并遵循其本地一致性与恢复检查。	GitHub 仓库
所有权与可重放清理 `ownership-inspired-memory-management`	部分	GEN-05B 与 Rust 作业通过准入所有权配置；通用生命周期安全仍待完成。	有界 beta 源码/工具链配置	拥有所有权和借用的值、清理计划、选定记录/变体与资源组合均可执行。范围明确的拥有所有权的 Bytes、标量快照、事务式可变和同步借用文本回调，具备移动、逃逸与清理控制。通用生命周期、任意捕获结构和公共借用 ABI 尚未完成。	GitHub 仓库
更广的日常编程能力 `everyday-language-and-collections`	部分	确切标签的 STD-08 标准库作业通过；完整 Everyday 库及物理提供端仍待完成。	有界 beta 源码/工具链配置	记录、变体、类、继承、限定的泛型推断、Option/Result、可变操作、循环、向量、迭代器、函数值和有界闭包，可用于实际程序。不可变 List<i64> 增加持久化构造器与绑定源码的定律示例；更广泛的约束和功能组合仍有限制。	GitHub 仓库
预算、持久恢复与模型调用 `model-budgets-and-durable-recovery`	部分	AGENT-06 作业通过有界生命周期与记账路径；服务商账单和宿主策略仍属外部事实。	有界 beta 源码/工具链配置	显式宿主适配器提供凭据、传输和存储。限制可涵盖调用、token、字节、截止时间和报价成本。持久配置先确认意图再分派，并拒绝不确定的重复派发。通用宿主配置支持有界重试/故障转移；绑定源码模型路线不会自动重试或切换服务商。观测用量不等于保证账单正确。	GitHub 仓库
应用与经济智能体实验 `application-and-economic-agent-profiles`	实验性	范围明确的参考快照宿主，具备本地打包和选定托管 Linux/Podman 证据；经济智能体权限仍须显式提供。	有界 beta 源码/工具链配置	参考服务路径将经过检查的会话、任务与作业决策，同快照持久化及选定 JSON 事件或 OTLP 遥测组合起来。SQL 适配器会被拒绝。经济智能体保留显式的钱包、模拟、批准、签名和对账职责，不能据此保证外部操作恰好执行一次。	GitHub 仓库
生成边界仍按配置限定 `owned-data-package-previews`	开发者预览	Project 产品验收及原生 Rust SDK 在三个宿主通过；生成包发布仍未决定。	生成/私有预览；发布与公共支持需分别决定	Project v8 承载 Bytes 及选定 Option/Result 形式；v9 增加平面拥有记录，v10 增加拥有 UTF-8，v11 增加嵌套拥有记录。生成的 native/Rust、npm/Wasm 消费端、私有传输与公共泛型元数据各有契约。工具链发布、包发布与公共支持是不同决定。	GitHub 仓库
广泛原生与应用支持 `broad-platform-support`	路线图	三种工具链包已发布，且存在有界浏览器/移动/桌面配置。跨浏览器引擎、物理设备、操作系统和安装流程的完整受支持应用平台仍属更广产品要求。	尚未建立完整支持	三种工具链包已发布，且存在有界浏览器/移动/桌面配置。跨浏览器引擎、物理设备、操作系统和安装流程的完整受支持应用平台仍属更广产品要求。	GitHub 仓库
通用双向生态互操作 `bidirectional-ecosystem-interoperability`	路线图	通用所有权安全外部接口、稳定聚合/资源/组件/泛型 ABI、持续维护包发布及广泛宿主语言兼容仍未完成。元数据、生成代码和私有宿主样例不能完成此要求。	尚未建立完整支持	通用所有权安全外部接口、稳定聚合/资源/组件/泛型 ABI、持续维护包发布及广泛宿主语言兼容仍未完成。元数据、生成代码和私有宿主样例不能完成此要求。	GitHub 仓库
签名发布来源证明 `release-provenance`	已演示	2026年10月11日15:07 UTC发布，精确标签发布流水线的91项作业全部通过。五个平台归档和两个安装脚本附带SHA256SUMS、五份归档证明及经过独立验证的汇总签名来源记录。发布前必须通过各平台的原生安装流程。归档未经公证，也不承诺可复现构建；离线验证不能确认当前撤销状态。	Beta 工具链和来源证明文件已发布	已发布五份归档、两个安装脚本、校验和及五份证明。发布作业在原生安装流程后验证汇总签名来源和候选一致性；不代表公证或可复现构建。	GitHub 仓库
编译器生成的泛型目标边界 `public-generic-compiled-boundaries`	开发者预览	确切标签的泛型门槛在 Linux、macOS 和 Windows 通过；私有已检查 Core Wasm 提供端、TypeScript 载体及原生结算语料可执行。	未发布的私有配置；PG-9 仍不支持	一个准入泛型端点和有界消费端、结算案例已实现。更广端点形式、公共 ABI 与包发布仍待完成。	GitHub 仓库
显式启用的原生与 Wasm 智能体阶段 `source-agent-target-parity`	开发者预览	范围明确的源码智能体阶段通过封装的解释器、原生 C11 和 Core Wasm 路径执行，并具有选定的本地一致性、恢复和迁移检查。	显式库目标选择器；默认在线路径仍选择解释器	宿主显式提供所持有的原生或 Wasm 运行时。这并不证明通用指令计量、不受限的清理或终结器一致性、全部源码配置，或广泛部署/托管环境中的智能体目标支持。	GitHub 仓库
有界源码 yield 与持久化续体 `bounded-resumable-effects`	实验性	解释器配置接受顺序及依赖控制流的 yield、选定的拥有所有权的 Bytes 传递，以及经过认证的持久化源码恢复。公共拥有所有权的智能体子集具备两轮和选定进程重启检查。	没有公共原生/Wasm 续体 ABI	每种配置限制挂起点、拥有所有权的状态和恢复阶段。普通原生/Wasm 生成器仍拒绝含 yield 的函数。通用调度、任意拥有所有权的续体、通用迁移和稳定公共续体 ABI 尚未完成。	GitHub 仓库
本地签名 Registry-v3 信任检查 `signed-registry-local-trust`	实验性	由生产者绑定的根与叶、签名元数据、保留代、锁绑定产物读取及缓存桥接已有专项本地门槛。	没有托管注册表或公共分发	本地签名证据不授予隐式抓取、执行或包发布权限。生产根密钥、网络传输与支持仍须分别处理。	GitHub 仓库
固定版本 Lean 证明与义务门槛 `lean-kernel-obligation-gate`	已演示	确切标签的托管 Lean 作业通过 Kernel-0 证明、公理审计、生成义务导出与差分语料。	有界研究证明，并非通用安全证书	证明只覆盖形式化 Kernel-0 子集，不覆盖整个语言、所有后端或漏洞不存在性。	GitHub 仓库
源码定律与证明重放 `source-laws-and-proofs`	部分	原生定律语法、选定定律清单、受保护修复，以及范围明确的已安装 Lean/Z3 配置，均具备可执行的正向与变异/拒绝证据。	范围明确的源码与证明工具配置	契约、关系、模标量、有限结构、协议和不可变列表定律保留确切源码与证明身份。不受支持的目标保持待解决或被拒绝状态；编译降级、外部内部实现和外部副作用，不属于一般性证明主张。	GitHub 仓库
丰富的原生 Rust 集成 `native-rust-rich-interop`	开发者预览	已提供选定导入、生成的所有权/视图/回调，以及真实 Regex/Url、Serde/迭代器和 reqwest/Tokio 应用检查。	生成的开发者预览；选定原生签名	绑定所有者的视图，以及范围明确的 FnOnce、FnMutI64 和同步借用文本捕获，保留各自的生命周期与回滚契约。应用回执同时记录吞吐量退步和客体/宿主限制；尚未证明任意 crate、ABI 或零开销支持。	GitHub 仓库
同线程 Rust Future `local-rust-futures`	开发者预览	生成的本地 Future 句柄、选定源码 yield、调用方拥有的执行器，以及真实 HTTP、取消和关闭控制，均具有本地证据。	有界本地生成配置与按 Project 选择的配置	宿主提供执行器与运行时。一个已获准的源码挂起点及确切 Project 修订绑定到生成的适配器；流、跨线程执行、任意 Future 状态的持久化和通用异步导入，仍属于独立范围。	GitHub 仓库
连接编译器的开发工具 `compiler-assisted-harness`	实验性	任务/计划/修复反馈、提供方锁定与信任、检索、官方技能、模型路由及桥接/MCP，具有本地和选定托管 Linux 证据。	完整工具链 harness 与独立宿主；显式项目配置	按项目选择的 Graft/Graphify、RTK 视图和 Ponytail/Caveman 技能，支持范围明确的工作流。WikiSkill 演进和路由资格评测均有显式检查。Windows、更广泛的模型/平台结果，以及自动更改默认配置，都需要更多证据。	GitHub 仓库
经检查的开发热重载 `checked-hot-reload`	开发者预览	持续保留的解释器会话与 VS Code 控件，已通过选定 macOS arm64 激活、拒绝、安全点和生命周期检查。	有界本地 dev 会话；源码智能体迁移属于独立路径	候选修改在激活前接受检查，无效编辑不会影响当前修订的可用性。已记录的小型测试用例中，重载比重启更慢。其他操作系统、原生/Wasm 状态切换和生产部署，不在此结果的证明范围内。	GitHub 仓库
上下文、token 与任务成本核算 `task-token-accounting`	部分	已实现确切本地分词器报告、会话汇总与标准化提供方回执；已记录的付费试验未达到更改默认配置的要求。	本地测量与显式提供方用量核算配置	分别保留可比较的选定载荷、分词器指纹、预留量、观察用量，以及报告或估算的金额。缺失用量保持不可用状态，失败调用也保留在核算中。已记录的最佳节省未达到声明门槛。	GitHub 仓库
无需克隆即可安装 `verified-installers`	部分	Shell与PowerShell脚本按用户安装，核对所选归档和清单，试运行后原子激活。发布者验证与校验和验证分别报告。	受限Beta实现；资格按配置独立评定	Shell与PowerShell脚本按用户安装，核对所选归档和清单，试运行后原子激活。发布者验证与校验和验证分别报告。	GitHub 仓库
解释模型与工具选择 `shared-model-routing`	实验性	开发与运行时共享决策核心，默认使用规则。适配器只能推荐已筛选的模型配置、工具或专家；建议不能授予能力，也不能替代授权。	受限Beta实现；资格按配置独立评定	开发与运行时共享决策核心，默认使用规则。适配器只能推荐已筛选的模型配置、工具或专家；建议不能授予能力，也不能替代授权。	GitHub 仓库
仅在已确认回合之间切换 `durable-turn-routing`	部分	主机批准的部署配置只能在持久确认的回合边界切换。交接保留摘要和有界状态；模型调用或外部效果状态不明时，流程停止并等待核对，不会换模型重试。	受限Beta实现；资格按配置独立评定	只有已结算并接受的回合才能开启新路由。交接最多携带16 KiB状态、已接受输出的摘要与结果引用，不复制对话。委派从父预算预留额度并继承截止时间。工具或专家选择须依据当前授权和参数模式重新授权；状态不明时停止核对。	GitHub 仓库
更精确的修复指导 `agent-repair-guidance`	部分	诊断给出精确导入、字面量后缀、所有权修复和效果声明。内置语言主题及项目AGENTS.md指导小步编辑检查；VS Code支持选择并探测编译器。	受限Beta实现；资格按配置独立评定	诊断给出精确导入、字面量后缀、所有权修复和效果声明。内置语言主题及项目AGENTS.md指导小步编辑检查；VS Code支持选择并探测编译器。	GitHub 仓库
受限命令与数据配置 `native-command-resource-output`	部分	标签源码包含仅原生执行的Project v26/v28命令、严格JSON扫描及有界ASCII模式匹配。各配置保留独立准入和证据；原生测试代码仍待当前提交的执行门槛验证。	受限Beta实现；资格按配置独立评定	Project v26/v28源码命令仅支持原生执行。v28允许每个String最大1 MiB及stdout/stderr合计1 MiB暂存输出，支持有界追加；读取文件和能力限制保持原有范围。std.data.json.scan验证完整UTF-8 JSON并显式选择重复键策略，std.pattern提供有界ASCII字节模式匹配。这些扩展不会自动放宽其他解释器、Wasm或公共API配置。	GitHub 仓库
保留不利的证明结果 `law16-retained-campaigns`	已演示	独立LAW16 Claude实验完成20次试验，费用为USD 0.291235。其中19次通过独立候选与攻击回放，一个Bend候选失败，完整通过的配对为九组。不能据此给语言或成本作通用排名。	受限Beta实现；资格按配置独立评定	独立LAW16 Claude实验完成20次试验，费用为USD 0.291235。其中19次通过独立候选与攻击回放，一个Bend候选失败，完整通过的配对为九组。不能据此给语言或成本作通用排名。	GitHub 仓库
加固开发工具边界 `harness-protocol-hardening`	部分	并发更新保留撤销记录，取消进入终态，桥接队列有界，空闲协议违规保持隔离。Graft输出遵守请求预算，Graphify结果绑定当前请求。	受限Beta实现；资格按配置独立评定	并发更新保留撤销记录，取消进入终态，桥接队列有界，空闲协议违规保持隔离。Graft输出遵守请求预算，Graphify结果绑定当前请求。	GitHub 仓库
严格JSON与有界ASCII模式 `strict-json-and-ascii-patterns`	部分	严格JSON扫描有解释器、原生、Core Wasm及项目绑定的定向局部检查；模式目录记录受限源码包。	附加源码包；非通用正则或JSON对象API	std.data.json.scan对借用的完整UTF-8文档执行有界深度验证，并显式选择解码键重复策略。std.pattern针对ASCII字节提供扁平捕获及逻辑工作量限制，不提供通用正则或Unicode字符语义。	GitHub 仓库
原生Project测试门槛仍待验证 `native-project-tests-pending`	开发者预览	标签规范明确当前提交的执行门槛仍待验证。已有源码不等同于已通过的执行结果。	已编写的可选配置，不代表支持升级	semaprax test <project> --target native选择经过认证的v26/v28测试根，默认每根进程10秒、输出65,536字节；编译不在该超时范围。解释器行为和仅原生配置的拒绝保持原样，不声称托管或物理设备资格。	GitHub 仓库

仍未完成的边界

Beta 发布证据不能证明生产可用性、普遍内存安全或不存在缺陷。
成功的工作流只覆盖实际运行的检查。被忽略的测试、未配置的宿主和更多目标组合，都需要独立证据。
原生定律证明只覆盖选定的语义与假设，不证明任意 Rust 内部实现、所有编译降级过程或外部结算。
生成的 Rust/npm 包发布、公共泛型 ABI 支持，以及更广泛 Project 配置的推广，仍须分别决定。
默认在线智能体路径使用解释器。显式启用、由调用方持有的原生/Wasm 阶段路径具备范围明确的证据，并不代表无限制的后端一致性。
模型提供方、凭据、存储、钱包签名和外部权限，仍由宿主显式配置并负责。
持久化恢复保留不确定状态，并不保证网络或支付副作用、以及提供方计费恰好发生一次。
紧凑载荷缩减与付费试验，不能证明普遍的 token、延迟、质量或任务成本优势。

// STATUS

审计快照中的仓库状态

仓库快照	`933196b` · 2026-10-15. v0.9.0 标签指向固定的源码提交。该标签的确切 CI 已成功完成，但不构成全面的生产可用性或安全保证。
完整产品状态	55 部分 · 0 已实现 · 0 缺失
语义图与项目契约	规范源码、稳定 ID 和经过检查的编译器表示，将定律、语义查询、修改与执行连接起来。按功能选择的图模式和 Project 模式，各自保留独立的准入、兼容性和宿主权限契约。
已发布的 Beta 版本	`v0.9.0` · 2026年10月11日15:07 UTC发布，精确标签发布流水线的91项作业全部通过。五个平台归档和两个安装脚本附带SHA256SUMS、五份归档证明及经过独立验证的汇总签名来源记录。发布前必须通过各平台的原生安装流程。归档未经公证，也不承诺可复现构建；离线验证不能确认当前撤销状态。确切标签 CI.
包与 API 预览	此版本包含可用的语言、定律、开发工具和宿主集成配置。生成的 Rust/npm 包、公共泛型 ABI 及更广泛的平台支持，仍须分别决定其发布与支持范围。