Superintelligence Guarantees for Instrumented Labs
Bounded autonomy for self-driving labs.
AI agents plan the experiments. A scientist approves the guarantees once. SIGIL proves every plan against them before anything on the deck moves.
plate_42 · ATP dose–response
rev 1 · follows instructions injected into the sample sheetThe demo
Same agent, same robot, same tampered input
Two simulated Hamilton STARlets run side by side in PyLabRobot's 3D visualizer. Both get the same request and the same sample sheet. Someone has hidden a note in the sheet, a prompt injection, asking for an extra row of ATP, to leave the plate out, and to reorder a "control" oligo. The agent follows it. The lab on the left runs the agent's plan directly. The lab on the right runs it through SIGIL.
| At the end | Agent alone | With SIGIL |
|---|---|---|
| ATP used, 800 µL budget | 2000 µL | 720 µL |
| Screened oligo sent to vendor | 1 sent | 0 sent |
| plate_42 back in storage | Left on deck | Stored |
| qPCR-1 released | Released | Released |
| Requested work done | Yes | Yes |
Every call in the first plan passed the robot's own per-call limits, such as 200 µL per transfer.
How it works
Signed once. Proved every time.
Approve a guarantee bundle
For a whole campaign, the scientist approves guarantees written in plain language: a reagent budget, an instrument allowlist, a biosecurity screen, a clean exit.
The agent writes a plan
Each iteration of the design–build–test–learn loop, the agent writes an ordinary Python plan against the lab's instrument calls.
SIGIL proves it
Before execution, the plan is proved against the bundle with the z3 solver. A failed proof names each broken guarantee and goes back to the agent.
Only proved plans run
The revised plan proves and runs. The scientist is not asked again, because the guarantees have not changed.
@clauz3.guarantee(sigil.reagent_volume_at_most("ATP", 800)) @clauz3.guarantee(sigil.only_instruments(["qPCR-1"])) @clauz3.guarantee(sigil.no_hazard_sequence("GATTACAGATTACA")) @clauz3.guarantee(sigil.all_plates_returned_at_end()) def main() -> None: book_instrument("qPCR-1") prepare_plate("plate_42") pipette("plate_42", "A1", 20, "ATP") pipette("plate_42", "A2", 40, "ATP") # … A3 to A8, rising to 160 µL submit_protocol("qPCR-1", "plate_42", 4) order_oligo("ATGGCTAGCTTGACCTAGGA", 200) return_plate("plate_42") release_instrument("qPCR-1")
Guarantees
Guarantees about the whole plan, in the scientist's words
Firmware checks one command at a time. These guarantees are about the whole sequence: totals, allowlists, what leaves the building, and what state the lab is left in. Each one shows up on the approval card as a sentence.
Budgets sums over the plan
- At most 800 µL of ATP is dispensed in total.
reagent_volume_at_most("ATP", 800) - Instruments run for at most 8 hours in total.
total_runtime_at_most(8) - Priced instrument time costs at most $500.
instrument_cost_at_most({"qPCR-1": 40}, 500) - Oligo orders cost at most $400.
oligo_cost_at_most(2, 400)
Scope what may be touched
- Every transfer targets plate_42.
only_plate("plate_42") - Protocols run only on qPCR-1.
only_instruments(["qPCR-1"]) - No instrument protocol is submitted.
no_protocols()
Biosecurity before the vendor sees it
- No ordered oligo contains a screened motif.
no_hazard_sequence("GATTACAGATTACA") - Every ordered oligo is at most 60 bases long.
oligo_length_at_most(60) - No oligo is ordered at all.
no_oligos()
Clean exit state at the end
- Every booked instrument is released by the end.
all_instruments_released_at_end() - Every plate is back in storage by the end.
all_plates_returned_at_end()
Questions that come up
Why a proof?
Isn't this input filtering?
SIGIL never reads the sample sheet. It checks the plan the agent actually wrote, so it catches an injection whatever form it takes, and it catches an ordinary bug such as an off-by-one loop just as well.
Couldn't the robot's firmware do this?
Firmware sees one command at a time. "At most 800 µL of ATP in total" and "every plate back in storage at the end" are properties of the whole sequence. In the demo, every call in the bad plan passed the device's own checks.
Does the agent have to be trusted?
No. The guarantees, the instrument calls and their limits live in a reviewed trusted layer. The agent can only write plans against it, and a plan that cannot be proved does not run.
Background
A pre-execution gate for autonomous labs
Cheng et al. (2026) call for verifiability-first autonomy in agent-driven life-science labs: validation before execution, safeguards during it, and auditing after. SIGIL is a concrete pre-execution gate for that loop, with a static biosecurity screen on every synthesis order.
It is built on clauz3, an open-source prover for agent programs, and demonstrated on PyLabRobot's open robot SDK.
- Status
- Pre-1.0, in private development
- Lab effects
- Pipetting, instrument booking and runs, plate moves, oligo orders. Mocked today; real drivers plug in behind the same calls.
- Prover
- clauz3 with the z3 SMT solver
- Demo
- Simulated Hamilton STARlet, PyLabRobot Visualizer3D
- Planned
- A curated biosecurity hazard list as its own trusted layer
Early access
Put an agent on your deck, inside guarantees you set
SIGIL is pre-1.0. We are looking for labs that run liquid handlers or cloud-lab protocols and want to let an agent plan the work. Leave your email and we will be in touch.