自己动手验证

Vera 是 Celina 内置的验证引擎。本文说明她如何生成无需我们在场、您的 QA 团队就能核验的证据。

面向质量负责人、数据完整性负责人以及计算机化系统验证团队。

临床研究中的每一个 AI 系统都在请求信任。这一个的构建方式，让它不必开口请求。

Vera 是 Celina 中负责检查记录的那部分。不是模型的推理，也不是模型的输出，而是平台在工作进行时生成的已签名账本：每个事件都经过哈希、链接到前一事件，并按内容寻址。Vera 机械地遍历这条链，并签发一份证书，准确说明她检查了什么，以及她未能检查什么。

她的裁定只有一句话，而且从不改变。

No break detected under the following checks.

在以下检查项下未发现断裂。

不是"有效"，不是"干净"，也不是一个孤零零的"已验证"。而是：哪些项目经受住了检查、在哪些检查项下、哪些项目被排除并已列明。任何持有公钥的人都可以重新运行这套计算。

Vera 是什么，不是什么

Vera 的验证路径中任何位置都不含语言模型。没有概率推理，没有置信度分数，没有推断。相同输入，相同裁定，每一次都如此。这一属性不是设计偏好，而是验证团队真正会去测试的属性，也是她的输出可以被当作证据而非意见的原因。

她不是生成 Celina 答案的部分。她是检查这些答案的记录是否完好的部分。模型提议，证据裁决。Vera 就是那份证据。

为什么 Vera 不是形式化证明

Vera 的最初设计是围绕定理证明器 Lean 构建的。当时的计划是证明验证逻辑的正确性，让一个小型的、经机器检查的内核来承载这份保证。我们后来放弃了这条路线，原因应当公开说明。

Lean 中的证明附着于链的一个模型。输入输出、数据库、网络和抽取层全都在证明之外。你证明的是模型，然后指望模型与生产环境之间的差距足够小。而 Vera 遍历的是生产环境的事件流本身：真实的字节、真实的数据库、完整的链。一次规则变更是一个带测试的 pull request，而不是一个证明工程项目；第三方核验她的工作只需获取公钥，而不必重新运行证明器。

这笔交换所放弃的东西是真实的，我们不假装不是：对验证逻辑本身是否可靠的机器检查保证。这份保证现在依托于检查项的简单性、绑定真实数据库的测试套件，以及任何人都能重新计算结果并抓住我们错误这一事实。证明说的是"我们的推理是正确的"。公开的密钥说的是"来证明我们错了"。验证团队更信任后一句话，因为那正是他们自己工作的形态。

遍历

Vera 在三个层级上检查记录。

第零级，密码学链。 事件哈希、前驱链接、文档完整性。每个事件的哈希是否与其声明一致，每个事件是否链接到它之前的事件。

第一级，结构。 模式有效性、排序、双时态一致性、取代链。有效时间和事务时间是否都被记录且相互一致。当某项内容被取代时，从原始版本到后继版本的链条是否成立。

第二级，溯源图。 每个工件是否都能追溯到生成它的来源。

没有抽样。遍历覆盖整条链，无法覆盖的部分会被列明，而不是跳过。

证书

每份证书都列举已运行的检查项。证书还带有一份预先登记的排除登记表，列明任何未能运行的检查项及其原因。没有任何内容被静默省略，这正是证书与安慰之间的区别。

证书由具名的验证者身份 vera-audit-v1 以 Ed25519 签名，随后作为已签名事件追加到它们所描述的同一份账本中。验证这一行为本身就在审计追踪之中。

自己动手验证

这是对验证团队最重要的部分，所以直接说明。

重新验证一份证书只需要公钥，别无其他。无需供应商访问权限，无需数据库，无需任何密钥，也无需与我们通话。

算法、密钥标识符、PEM 格式的公钥、签名编码以及载荷规范化契约均发布在一个开放端点：

GET /vera/v1/keys

证书可在以下端点凭该公钥重新验证：

GET /vera/v1/certificates/verify

验证契约完整且公开。安全或 QA 职能部门可以获取公钥、独立验证证书，并在任何商务洽谈开始之前得出自己的结论。这正是我们设想的操作顺序。

底层账本

仅追加。 记录不能被编辑，只能被追加。更正即取代：先前版本保留，链接到其后继版本，两个时间戳完整无缺。不存在任何改写历史的途径，对我们自己也一样。

按内容寻址。 工件以 SHA-256 哈希标识。记录之所以是原件，是由构造保证的，而非靠制度约定。

双时态。 有效时间和事务时间都在事件发生的那一刻记录，而非事后重建。

按司法辖区分密钥。 签名使用按命名空间划分的密钥环，美国记录和巴西记录使用各自独立的密钥，带版本，分阶段轮换。历史记录行在密钥环下保持验证不变，因为切换在构造上是逐字节相同的。一条美国记录和一条巴西记录在密码学上是可分离的。

边界防护

两道相互独立的防线立在记录之前。平台级身份认证在未认证请求触及应用代码之前就将其拒绝，且这一拒绝经过测试。其后，应用级主体检查遵循失败即关闭：配置错误的依赖项会拒绝，而不是默认放行。

谱系导出按工件、按司法辖区提供，仅限记录所有者或审计员角色。空结果返回的行数为零，而不是一个可区分的"未找到"，因此该接口无法被用来探测哪些内容存在。

写入和签发均受速率限制。已部署镜像的摘要以基础设施即代码的方式固定为部署记录，任何偏差都会导致构建失败。Vera 的严格测试套件在每次变更时都针对真实数据库运行。她的代码不会未经验证就上线。

对照 ALCOA+ 来看

我们不做合规声明。下表描述的是底层基础所做的事。结论由您来下。

FAQ

这符合 21 CFR Part 11 吗？

我们不做这样的声明。合规性是贵组织依据自身框架进行的评估。我们能够陈述的是能力：一份仅追加、哈希链式、双时态的记录，带有具名的人工签署和可独立验证的证书。上文正是为了让您的验证团队能够直接评估而写。

为什么证书写的是 "no break detected under the following checks"，而不是"已验证"？

因为"已验证"会是对未执行检查项的一种断言。证书列明已执行的检查项和被排除的检查项，措辞的范围严格限于此。任何超出这一范围的说法都是安慰，而非结论。

排除登记表里有什么？

某次遍历中未能执行的任何检查项，逐项明确列出，并附原因。该登记表是预先登记的，也就是说可能的排除项集合是事先声明的，而不是事后发现的。没有任何检查项会被悄悄跳过。

我的团队能否在不接触 NexTrial 任何系统的情况下验证证书？

可以。验证只需要公钥，公钥连同完整的验证契约一起发布在开放的密钥端点上。无需账号，无需数据库访问，无需联系支持。

Vera 会检查 Celina 的答案是否正确吗？

不会。Vera 检查的是这些答案的记录是否完好：密码学、结构和溯源。一项判定是否正确，由确定性裁定引擎基于经签署的语料库确立，并由具名的人最终定案。Vera 证明的是，此后记录未被篡改。

如果验证端点不可用会怎样？

已签发的证书无论服务是否可用都可凭公钥验证，因为验证并不依赖该服务。服务本身遵循失败即关闭：依赖项不可用时产生明确的拒绝，绝不会静默放行。

密钥轮换后，旧证书还能验证吗？

可以。密钥环是版本化的，轮换分阶段进行。历史记录行在密钥环下按构造保持验证不变。

我们能把记录导出到自己的系统吗？

可以。已签名的谱系导出按工件、按司法辖区提供给记录所有者或审计员角色。它以数据形式流转，接收方无需从 NexTrial 获取任何东西即可核验。

记录出错时会怎样？

记录会被取代，绝不会被编辑。原始记录保留，并链接到其后继版本，两个时间戳均完整保存。从原始记录到更正记录的链条本身就是已验证记录的一部分。

Vera 是语言模型吗？

不是。她的验证路径中不存在任何模型。她不推理，她只检查。

Vera 自身如何被测试？

她的测试套件在每次代码变更时都针对真实数据库运行，套件失败即阻止合并。已部署镜像的摘要被固定为部署记录，固定摘要与实际运行版本之间的任何偏差都会导致构建失败。

我们能在任何商务洽谈之前先试用吗？

这正是我们设想的顺序。获取公钥，验证一份证书，形成您自己的判断。带一个工件来，看着它带着证书离开。

Vera 最初是基于 Lean 构建的吗？

是的。Vera 的最初设计围绕定理证明器 Lean 构建，验证逻辑将被证明正确并由一个小型可信内核检查。我们把保证转移到了确定性、完全透明以及对生产链的独立重算之上，因为关于模型的证明并不检查您的数据。上文说明了这笔交换放弃了什么、换来了什么。

放弃形式化证明会让 Vera 更不可信吗？

它改变的是信任所依托的基础。Lean 证明在模型假设范围内保证验证逻辑，但对已部署的数据库、网络或抽取层不置一词。Vera 的检查项小到可以直接阅读，她的测试套件在每次变更时针对真实数据库运行，任何第三方都可以凭公钥重新计算她的裁定。如果我们将来重新引入形式化深度，方式将是证明规范化、链接和取代这些小型规范内核，同时继续针对真实数据执行。

为数据完整性靠审计而非靠声明的环境而构建。

NexTrial.ai · Celina · Trial Activation Intelligence