LIMS example

The LIMS example is the autonomous-science / cloud-lab analog of the bank example. It exercises the same relation primitives — allowlists, numeric aggregation, and per-field substring guards — against a wet-lab effect vocabulary: pipetting, instrument scheduling, and oligo ordering.

It is a toy: a production trusted layer for autonomous science (MADSci nodes, Emerald Cloud Lab, Strateos) would live in a separate domain repo and be installed with clauz3 install. See issue #41 for the bud-off plan and #42 for the biosecurity-screening angle that the no_hazard_sequence contract here gestures at.

Trusted module

Three trusted effects, each with a per-call precondition lifted into a proof obligation. The volume, hours, and copies bounds are written in natural chained-comparison form (0 < volume_ul <= 200); see issue #43 for the fix that made this idiomatic form actually enforce both bounds.

examples/lims/tools/lims/trusted/effects.py

import deal


@deal.pre(
    lambda plate, well, volume_ul, reagent: 0 < volume_ul <= 200,
    message="volume_ul must be in (0, 200]",
)
@deal.has("trusted")
def pipette(plate: str, well: str, volume_ul: int, reagent: str) -> None:
    """MOCK trusted pipette action.

    Transfers ``volume_ul`` microlitres of ``reagent`` into ``well`` on
    ``plate``. Per-call volume is bounded by the trusted layer; total volume
    per reagent and per-plate scope are agent-stated guarantees.
    """
    pass


@deal.pre(
    lambda instrument, plate, hours: 0 < hours <= 24,
    message="hours must be in (0, 24]",
)
@deal.has("trusted")
def submit_protocol(instrument: str, plate: str, hours: int) -> None:
    """MOCK trusted instrument submission.

    Books ``instrument`` for ``hours`` to run a protocol on ``plate``.
    Per-call duration is bounded; instrument allowlist and total runtime
    are agent-stated guarantees.
    """
    pass


@deal.pre(
    lambda seq, copies: 0 < copies <= 1000,
    message="copies must be in (0, 1000]",
)
@deal.has("trusted")
def order_oligo(seq: str, copies: int) -> None:
    """MOCK trusted oligo order.

    Submits an order for ``copies`` of synthesized oligonucleotide ``seq``.
    Sequence content (length, hazard motifs) is an agent-stated guarantee
    and is the surface biosecurity policies attach to.
    """
    pass

The contract vocabulary covers plate scope, reagent and runtime budgets, oligo-length bounds, and a substring-based hazard guard.

examples/lims/tools/lims/trusted/contracts.py

"""LIMS / cloud-lab predicates built from generic trusted effect facts.

These contracts let an agent state policies about a wet-lab campaign before
any reagent moves:

- spatial scope (``only_plate``);
- instrument allowlist (``only_instruments``);
- reagent and runtime budgets (``reagent_volume_at_most``, ``total_runtime_at_most``);
- absence of effects (``no_protocols``, ``no_oligos``);
- sequence-content guards on synthesis orders (``oligo_length_at_most``,
  ``no_hazard_sequence``).

The sequence-content guards ride on the same z3.Contains primitive used by
``examples/text``'s ``must_not_contain``: they are the static-screening shape
biosecurity policy can attach to before submission, rather than after.
"""

from clauz3.spec import ContractSpec, contract, effect
from clauz3.spec import no_guarantees as core_no_guarantees

Pipette = effect("pipette")
Protocol = effect("submit_protocol")
Oligo = effect("order_oligo")


@contract
def no_guarantees() -> ContractSpec:
    """Make no guarantees about lab effects."""
    return core_no_guarantees()


# ── Pipette / plate scope ────────────────────────────────────────────────────


@contract
def only_plate(plate: str) -> ContractSpec:
    """Guarantee every pipette targets this plate."""
    return Pipette.all(lambda e: e.plate == plate)


@contract
def reagent_volume_at_most(reagent: str, max_ul: int) -> ContractSpec:
    """Guarantee total volume of ``reagent`` dispensed is at most ``max_ul``."""
    by_reagent = Pipette.where(lambda e: e.reagent == reagent)
    return by_reagent.sum(lambda e: e.volume_ul) <= max_ul


@contract
def total_pipette_volume_at_most(max_ul: int) -> ContractSpec:
    """Guarantee total volume across all pipette calls is at most ``max_ul``."""
    return Pipette.sum(lambda e: e.volume_ul) <= max_ul


# ── Instrument / runtime ──────────────────────────────────────────────────────


@contract
def only_instruments(allowed: list[str]) -> ContractSpec:
    """Guarantee every submitted protocol uses an instrument in ``allowed``."""
    return Protocol.all(lambda e: e.instrument in allowed)


@contract
def total_runtime_at_most(hours: int) -> ContractSpec:
    """Guarantee total instrument runtime booked is at most ``hours``."""
    return Protocol.sum(lambda e: e.hours) <= hours


@contract
def no_protocols() -> ContractSpec:
    """Guarantee no instrument protocol is submitted."""
    return Protocol.empty()


# ── Oligo / sequence content ─────────────────────────────────────────────────


@contract
def no_oligos() -> ContractSpec:
    """Guarantee no oligo is ordered."""
    return Oligo.empty()


@contract
def oligo_length_at_most(max_bases: int) -> ContractSpec:
    """Guarantee every ordered oligo is at most ``max_bases`` long."""
    return Oligo.all(lambda e: len(e.seq) <= max_bases)


@contract
def no_hazard_sequence(motif: str) -> ContractSpec:
    """Guarantee no ordered oligo contains ``motif`` as a substring.

    This is the static-screening shape for biosecurity: the prover discharges
    the guarantee before any synthesis order is submitted, so a hazard-motif
    list maintained by a biosafety officer can be enforced *before* a vendor
    sees the sequence rather than after.
    """
    return Oligo.all(lambda e: motif not in e.seq)

A DBTL campaign

The pattern that motivates the example: an LLM-driven design-build-test-learn loop submits one plan per iteration. The user approves the campaign-level guarantee once; each iteration's plan is discharged automatically as long as it entails the guarantee.

examples/lims/cases/dbtl_campaign_pass.py

# ruff: noqa: F821
from tools.lims.trusted import contracts as lims
from tools.lims.trusted.effects import pipette, submit_protocol

import clauz3


@clauz3.guarantee(lims.only_plate("plate_42"))
@clauz3.guarantee(lims.reagent_volume_at_most("ATP", 500))
@clauz3.guarantee(lims.only_instruments(["qPCR-1"]))
@clauz3.guarantee(lims.total_runtime_at_most(10))
def main() -> None:
    for _ in range(8):
        pipette("plate_42", "A1", 50, "ATP")
    submit_protocol("qPCR-1", "plate_42", 4)

A biosecurity guard

no_hazard_sequence(motif) lowers to the same z3.Contains primitive that the text example's must_not_contain uses. Before any oligo synthesis is submitted, the prover discharges the substring guard over every ordered sequence — exactly the static-screening shape a biosafety officer's policy can attach to.

examples/lims/cases/no_hazard_sequence_pass.py

# ruff: noqa: F821
from tools.lims.trusted import contracts as lims
from tools.lims.trusted.effects import order_oligo

import clauz3


@clauz3.guarantee(lims.no_hazard_sequence("GATTACA"))
@clauz3.guarantee(lims.oligo_length_at_most(60))
def main() -> None:
    order_oligo("ACGTACGTACGT", 10)

A sequence containing the hazard motif is rejected:

examples/lims/cases/no_hazard_sequence_fail.py

# ruff: noqa: F821
from tools.lims.trusted import contracts as lims
from tools.lims.trusted.effects import order_oligo

import clauz3


@clauz3.guarantee(lims.no_hazard_sequence("GATTACA"))
def main() -> None:
    order_oligo("AAAGATTACATTT", 5)

All cases

Browse the full set on the all-cases page.

How they run

examples/lims/Justfile

trusted := "tools/lims/trusted"
effects := trusted + "/effects.py"
prove := "uv run clauz3 prove --trusted-root " + trusted

test: lint cases

lint:
    uv run python -m deal lint {{effects}}

cases: only-plate-pass only-plate-fail reagent-budget-pass reagent-budget-fail only-instruments-pass only-instruments-fail total-runtime-pass total-runtime-fail no-hazard-sequence-pass no-hazard-sequence-fail dbtl-campaign-pass pipette-volume-precondition-fail lims-no-guarantees-pass

only-plate-pass:
    {{prove}} cases/only_plate_pass.py

only-plate-fail:
    if {{prove}} cases/only_plate_fail.py; then exit 1; fi

reagent-budget-pass:
    {{prove}} cases/reagent_budget_pass.py

reagent-budget-fail:
    if {{prove}} cases/reagent_budget_fail.py; then exit 1; fi

only-instruments-pass:
    {{prove}} cases/only_instruments_pass.py

only-instruments-fail:
    if {{prove}} cases/only_instruments_fail.py; then exit 1; fi

total-runtime-pass:
    {{prove}} cases/total_runtime_pass.py

total-runtime-fail:
    if {{prove}} cases/total_runtime_fail.py; then exit 1; fi

no-hazard-sequence-pass:
    {{prove}} cases/no_hazard_sequence_pass.py

no-hazard-sequence-fail:
    if {{prove}} cases/no_hazard_sequence_fail.py; then exit 1; fi

dbtl-campaign-pass:
    {{prove}} cases/dbtl_campaign_pass.py

pipette-volume-precondition-fail:
    if {{prove}} cases/pipette_volume_precondition_fail.py; then exit 1; fi

lims-no-guarantees-pass:
    {{prove}} cases/lims_no_guarantees_pass.py