VeriBiota v0.2.1：确定性验证与已验证保证

Source: Dev.to

概览

这是我们首次可以自信称之为产品级的发布。
目标很简单：信任来源于对齐和验证，而不是承诺或营销图示。

VeriBiota 可以无缝嵌入现有的计算生物学流水线。你可以在本地或 CI 中运行，它会检查你声称生成的内容，并在出现不符合时明确告知。

实际功能

• 可在本地或 CI 中运行
• 生成确定性的产物
• 当不变量被破坏时会大声报错
• 留下持久的审计痕迹：模式、哈希、来源记录、可选签名

v0.2.1 实际交付内容

结构化生物学产物的确定性验证

配置检查返回稳定的退出码和机器可读的判定，CI 可以据此进行门控。

可复现的来源记录

为审计和事后分析而设计，而非截图。

对选定不变量的形式化证明保证

基于 Lean 定理，而非占位符。

零摩擦采纳

预编译二进制和固定容器。使用时无需安装 Lean。

今日已证明（Lean 支持）

以下配置已由非占位符的 Lean 定理锚点支撑：

• 全局仿射比对正确性 – global_affine_v1
• 编辑脚本应用正确性 – edit_script_v1
• 编辑脚本规范化 – edit_script_normal_form_v1
• 语义保持加幂等性 – snapshot_signature_v1

验证输出可证明绑定于

• 输入哈希
• 已注册的模式标识和模式哈希
• 已注册的定理列表

今日已检查的合约（证明正在扩展）

这些配置通过模式对齐的解码、可执行检查、夹具和 CI 强制执行。正式证明已计划并正在积极添加中。

• PairHMM 桥接 – pair_hmm_bridge_v1
• Prime 编辑计划 – prime_edit_plan_v1
• VCF 规范化 – vcf_normalization_v1

某些配置可能出现在清单中，但尚未通过 VeriBiota 检查。这是有意且明确的。

关于快照签名的必要说明

snapshot_signature_v1 不是 加密签名。它是一种来源绑定记录，通过规范化 JSON 和哈希绑定来保证验证输出的完整性和可追溯性。它 不提供 不可否认性。

如果需要加密真实性，请使用 Ed25519 和 JWS 签名流程进行检查和证书签发，并通过 JWKS 验证。该系统在设计上是独立的。

在 CI 中尝试

无需安装 Lean。无需繁琐的设置。

docker pull ghcr.io/omnisgenomics/veribiota:v0.2.1
mkdir -p ci_signatures

docker run --rm \
  -v "$PWD":/work \
  -w /work \
  ghcr.io/omnisgenomics/veribiota:v0.2.1 \
  check alignment global_affine_v1 \
  examples/profiles/global_affine_v1/match.json \
  --snapshot-out ci_signatures/global_affine_v1.sig.json \
  --compact

此版本旨在奠定底线：确定性、验证、来源以及在关键位置的证明。功能范围将会扩大，但合约不会变得宽松。

资源

• Github
• Docs