VeriBiota v0.2.1: Deterministic Verification with Proven Guarantees

Source: Dev.to

Overview

This is the first release we’re comfortable calling product grade.
The goal is simple: trust that comes from alignment and verification, not from promises or marketing diagrams.

VeriBiota drops into existing computational biology pipelines without ceremony. You run it locally or in CI, it checks what you said you produced, and it tells you very clearly when something does not hold.

What it does in practice

• Runs locally or in CI
• Emits deterministic artifacts
• Fails loudly when invariants break
• Leaves a durable audit trail: schemas, hashes, provenance records, optional signing

What v0.2.1 actually delivers

Deterministic verification of structured biology artifacts

Profile checks return stable exit codes and machine‑readable verdicts that CI can gate on.

Reproducible provenance records

Designed for audits and post‑mortems, not screenshots.

Formally proven guarantees for selected invariants

Backed by Lean theorems, not placeholders.

Zero‑friction adoption

Pre‑built binaries and a pinned container. No Lean install required to use it.

Proven today (Lean backed)

The following profiles are backed by non‑placeholder Lean theorem anchors:

• Global affine alignment correctness – global_affine_v1
• Edit script application correctness – edit_script_v1
• Edit script normalization – edit_script_normal_form_v1
• Semantic preservation plus idempotence – snapshot_signature_v1

Verification outputs are provably bound to

• the input hash
• the registered schema identity and schema hash
• the registered theorem list

Contract checked today (proofs expanding)

These profiles are enforced by schema‑aligned decoding, executable checks, fixtures, and CI. Formal proofs are planned and actively being added.

• PairHMM bridge – pair_hmm_bridge_v1
• Prime editing plans – prime_edit_plan_v1
• VCF normalization – vcf_normalization_v1

Some profiles may appear in the manifest but are not yet routed through VeriBiota checks. That is intentional and explicit.

A necessary clarification about snapshot signatures

snapshot_signature_v1 is not a cryptographic signature. It is a provenance binding record that guarantees integrity and traceability of verification outputs through canonical JSON and hash binding. It does not provide non‑repudiation.

If you need cryptographic authenticity, use the Ed25519 and JWS signing flow for checks and certificates, verified via JWKS. That system is separate by design.

Try it in CI

No Lean install. No setup gymnastics.

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

This release is about setting a floor: determinism, verification, provenance, and proofs where they matter. The surface area will grow, but the contract does not get softer.

Resources

• Github
• Docs