# API Reference


## Contracts


State what a transformation assumes and promises, and have it proved before any data runs.


[transform()](transform.md#sverify.transform)  
Decorate a function from Ibis tables to an Ibis table with a contract.

[verify()](verify.md#sverify.verify)  
Try to prove `ensures` about `query` (an Ibis table expression or a

[unique()](unique.md#sverify.unique)  
A key: at most one row per combination of `cols`.

[key()](key.md#sverify.key)  
A primary key: at most one row per combination of `cols`, and no NULL

[references()](references.md#sverify.references)  
A foreign key: every non-NULL value of `col` occurs in the column `to`

[Report](Report.md#sverify.Report)  
What the checker proved about a transformation, returned by `verify` and kept

[Report.from_substrait()](Report.from_substrait.md#sverify.Report.from_substrait)  
Read a plan `to_substrait` exported, and prove its contract again


## Report Methods


Methods for the Report class


[Report.to_json()](Report.to_json.md#sverify.Report.to_json)  
The report as a versioned JSON document, for CI jobs and tools

[Report.from_json()](Report.from_json.md#sverify.Report.from_json)  
A report from what `to_json` wrote, by this version of sverify or

[Report.from_substrait()](Report.from_substrait.md#sverify.Report.from_substrait)  
Read a plan `to_substrait` exported, and prove its contract again

[Report.to_substrait()](Report.to_substrait.md#sverify.Report.to_substrait)  
The verified plan for any conforming Substrait consumer, with its

[Report.substrait_contract()](Report.substrait_contract.md#sverify.Report.substrait_contract)  
The contract `to_substrait` embeds, as JSON, for a sidecar file.

[Report.to_sql()](Report.to_sql.md#sverify.Report.to_sql)  
The verified plan as SQL whose meaning is the proof's, in

[Report.check_inputs()](Report.check_inputs.md#sverify.Report.check_inputs)  
Check the preconditions (`requires`, the inferred bounds among

[Report.run()](Report.run.md#sverify.Report.run)  
Run the plan this report checked (`plan`) over the tables of

[Report.proved](Report.proved.md#sverify.Report.proved)  
Every postcondition holds and no runtime error is possible. With

[Report.floats_unmet](Report.floats_unmet.md#sverify.Report.floats_unmet)  
Why no engine's doubles meet the observation's `floats` (exact

[Report.needed](Report.needed.md#sverify.Report.needed)  
With `on_inferred="error"`, the preconditions the proof needs that

[Report.needed_text](Report.needed_text.md#sverify.Report.needed_text)  
`needed` in words: per input table and operation, the preconditions

[Report.equivalence](Report.equivalence.md#sverify.Report.equivalence)  
The equivalence the result is proved up to: `sv.equivalent(...)` in

[Report.needs](Report.needs.md#sverify.Report.needs)  
`needed` as data, one `Needed` per precondition: the table, the

[Report.needed_conditions](Report.needed_conditions.md#sverify.Report.needed_conditions)  
`needs` as conditions, per input table, ready for `requires=`: Ibis

[Report.needs_text()](Report.needs_text.md#sverify.Report.needs_text)  
Deprecated: `needed_text` lists every needed precondition.

[Report.needs_lines()](Report.needs_lines.md#sverify.Report.needs_lines)  
Deprecated: the property `needed_text`.

[Report.errors](Report.errors.md#sverify.Report.errors)  
The `issues` an engine fails on at run time (`Issue.error` is true).

[Report.warnings](Report.warnings.md#sverify.Report.warnings)  
The `issues` that do not count against a proof. None do: an

[Report.suggestions](Report.suggestions.md#sverify.Report.suggestions)  
For each unproved postcondition with one, the preconditions per

[Report.unproved](Report.unproved.md#sverify.Report.unproved)  
The postconditions in `ensures` that were not proved.

[Report.notes](Report.notes.md#sverify.Report.notes)  
What the report notes about the result as a whole, as `str(report)`

[Report.route()](Report.route.md#sverify.Report.route)  
The route by which `run` would take the plan to `engine`, and the

[Report.verdict](Report.verdict.md#sverify.Report.verdict)  
The report's first line: "proved", or "NOT proved:" and what is

[Report.__str__()](Report.__str__.md#sverify.Report.__str__)  


## Transforms, nodes and refresh


A source piped into a contracted transform, `orders.pipe(paid)`, builds a node. Nodes compose left to right with `.pipe`, are stored with `.write(sink)`, and are kept up to date by `.refresh()`, with update plans proved equal to a full recompute.


[Node](Node.md#sverify.Node)  
The result of a contracted transform over sources or other nodes.

[sql.Unsupported](sql.Unsupported.md#sverify.sql.Unsupported)  
The plan is outside the Lean model, or the dialect cannot express it.

[sql.Dialect](sql.Dialect.md#sverify.sql.Dialect)  
SQL syntax and semantics of one engine.

[sql.parse_plan()](sql.parse_plan.md#sverify.sql.parse_plan)  
Read a Substrait JSON plan (as a dict) into the model, as `parsePlan` does.

[sql.to_sql()](sql.to_sql.md#sverify.sql.to_sql)  
SQL for a Substrait JSON plan, with the semantics `Rel.eval` gives it.

[sql.dialect_of()](sql.dialect_of.md#sverify.sql.dialect_of)  
The `Dialect` named `dialect` (`"duckdb"`, `"snowflake"` or

[sql.Kind](sql.Kind.md#sverify.sql.Kind)  
What a value is in SQL. `time` is a microsecond TIMESTAMP without time

[sql.DIALECTS](sql.DIALECTS.md#sverify.sql.DIALECTS)  

[group()](group.md#sverify.group)  
Several nodes to refresh together, against the same source versions:

[io.Changes](io.Changes.md#sverify.io.Changes)  
Rows to insert into and delete from one table (bag semantics: each

[nodes.Group](nodes.Group.md#sverify.nodes.Group)  
Nodes refreshed together; see `group`.

[nodes.Refresh](nodes.Refresh.md#sverify.nodes.Refresh)  
What a refresh did, node by node, upstream first: returned by

[nodes.Status](nodes.Status.md#sverify.nodes.Status)  
Where each node of a group stands: returned by `Node.status` and

[nodes.NodeStatus](nodes.NodeStatus.md#sverify.nodes.NodeStatus)  
Where one node stands; see `Node.status`. `str()` gives one line,

[nodes.StageRefresh](nodes.StageRefresh.md#sverify.nodes.StageRefresh)  
What one refresh did to one node: how its state started (on the first


## Node Methods


Methods for the Node class


[Node.__repr__()](Node.__repr__.md#sverify.Node.__repr__)  

[Node.schema](Node.schema.md#sverify.Node.schema)  
The node's columns and their types, known when the node is built.

[Node.internal_plan](Node.internal_plan.md#sverify.Node.internal_plan)  
The Substrait plan (JSON) of the node's stage, as Lean checked and

[Node.plan](Node.plan.md#sverify.Node.plan)  
Deprecated: `internal_plan`, sverify's own form of the plan

[Node.report](Node.report.md#sverify.Node.report)  
The `Report` of the contract that made the node's result: the

[Node.to_substrait()](Node.to_substrait.md#sverify.Node.to_substrait)  
The node's verified plan for any conforming Substrait consumer,

[Node.to_sql()](Node.to_sql.md#sverify.Node.to_sql)  
The node's stage as SQL, in `dialect`: what `refresh` runs for a

[Node.pipe()](Node.pipe.md#sverify.Node.pipe)  
Apply `step` to this node, left to right: `orders.pipe(paid)` is

[Node.write()](Node.write.md#sverify.Node.write)  
Store this node in `sink` (`sverify.io.DeltaSink`, `IcebergSink`),

[Node.refresh()](Node.refresh.md#sverify.Node.refresh)  
Bring this node and every node it reads up to date, and write the

[Node.status()](Node.status.md#sverify.Node.status)  
Where the node stands: the source versions of its state, where it

[Node.table](Node.table.md#sverify.Node.table)  
The node's state as an Ibis table, to query further.

[Node.versions](Node.versions.md#sverify.Node.versions)  
The version of every source the node's state reflects, by name,

[Node.to_arrow()](Node.to_arrow.md#sverify.Node.to_arrow)  
The node's state as an Arrow table.

[Node.quarantined()](Node.quarantined.md#sverify.Node.quarantined)  
The rows of the node's sources set aside by \`on_violation=

[Node.to_polars()](Node.to_polars.md#sverify.Node.to_polars)  
The node's state as a Polars DataFrame (needs `polars`).

[Node.to_pandas()](Node.to_pandas.md#sverify.Node.to_pandas)  
The node's state as a pandas DataFrame (needs `pandas`).


## Sources and sinks


Delta Lake and Iceberg tables as versioned sources, sources of preconditions, and sinks that carry the contract (`sverify.io`).


[io.DeltaSource](io.DeltaSource.md#sverify.io.DeltaSource)  
A Delta table read by version, as the input of transforms.

[io.DeltaSink](io.DeltaSink.md#sverify.io.DeltaSink)  
Stores a node in a Delta table, exactly once per state:

[io.IcebergSource](io.IcebergSource.md#sverify.io.IcebergSource)  
An Iceberg table of a catalog, read by snapshot sequence number, as

[io.IcebergSink](io.IcebergSink.md#sverify.io.IcebergSink)  
Stores a node in an Iceberg table, exactly once per state:

[io.StaticSource](io.StaticSource.md#sverify.io.StaticSource)  
An in-memory Arrow table as a source, such as a small lookup table or

[io.SinkWrite](io.SinkWrite.md#sverify.io.SinkWrite)  
What storing a node's state did, in any sink.

[io.Contract](io.Contract.md#sverify.io.Contract)  
What a sink records with each commit: which plan produced the data,

[io.Storage](io.Storage.md#sverify.io.Storage)  
Options for the object store tables live in (credentials, region,


## Your own sources and sinks


Read from an API, a database or a folder of files with one `read` method, and write anywhere with one `write` method; sverify keeps the versions, the changes, the contract and the exactly-once writes. Table formats with metadata implement the full `VersionedSource` protocol.


[io.Source](io.Source.md#sverify.io.Source)  
A table you read yourself: subclass it and implement `read`.

[io.Batch](io.Batch.md#sverify.io.Batch)  
What a `Source` read: new rows and the cursor to read from next time.

[io.from_query()](io.from_query.md#sverify.io.from_query)  
A source that reads new rows by a high-water mark: `fn(since)`

[io.from_frame()](io.from_frame.md#sverify.io.from_frame)  
A source that reads the whole table on every refresh: `fn()` returns

[io.from_files()](io.from_files.md#sverify.io.from_files)  
A source that reads the files dropped in a directory: each refresh

[io.Sink](io.Sink.md#sverify.io.Sink)  
Where `node.write(sink)` stores a node: subclass it and implement

[io.SinkChange](io.SinkChange.md#sverify.io.SinkChange)  
What a sink writes for one state of its node: the change since the

[io.sink_from()](io.sink_from.md#sverify.io.sink_from)  
A sink that hands the node's whole table to `fn` whenever it

[io.VersionedSource](io.VersionedSource.md#sverify.io.VersionedSource)  
What a pipeline needs of a source: a table with integer versions that

[io.Snapshot](io.Snapshot.md#sverify.io.Snapshot)  
A table at one version, as a source hands it to a pipeline: what

[io.SourceBatch](io.SourceBatch.md#sverify.io.SourceBatch)  
What a versioned source has between a recorded version and its latest


## Engines and SQL


Run a checked plan on DuckDB, Polars, DataFusion or Spark, or write it as DuckDB, Snowflake or Spark SQL (`Node.to_sql`, `Report.to_sql`; `sverify.engines`). `Dialect`'s SQL-writing methods change as functions land, so they are left out; subclassing it is outside the 1.x promise.


[connect()](connect.md#sverify.connect)  
A new, empty connection whose plans run on `engine`.

[engines.run()](engines.run.md#sverify.engines.run)  
Run a plan in Lean's written form on `engine` (default: the

[engines.ENGINES](engines.ENGINES.md#sverify.engines.ENGINES)  
The engines a `Connection` runs plans on: `"duckdb"` (the default),

[engines.Connection](engines.Connection.md#sverify.engines.Connection)  
Named Arrow tables, and the engine that runs plans over them.

[engines.Dialect](engines.Dialect.md#sverify.engines.Dialect)  
SQL syntax and semantics of one engine.

[engines.DUCKDB](engines.DUCKDB.md#sverify.engines.DUCKDB)  

[engines.SNOWFLAKE](engines.SNOWFLAKE.md#sverify.engines.SNOWFLAKE)  

[engines.SPARK](engines.SPARK.md#sverify.engines.SPARK)  

[engines.Unsupported](engines.Unsupported.md#sverify.engines.Unsupported)  
Sverify refuses the input: the SQL lift or the Ibis producer cannot

[engines.SPARK_CONF](engines.SPARK_CONF.md#sverify.engines.SPARK_CONF)  

[engines.run_sharded()](engines.run_sharded.md#sverify.engines.run_sharded)  
The plan's result on all the data, computed shard by shard on Polars.


## ASOF joins


Align two time series, each row with the latest earlier row of the other.


[asof_join()](asof_join.md#sverify.asof_join)  
Match each left row with the latest right row at or before it.


## Plans


The low-level layer: Substrait plans, Lean's written form of them, the SQL of a plan, and the update plans of incremental maintenance (`sverify.engines`). They take sverify's internal plan, so they are outside the 1.x promise and may change in a minor release; `Node.to_sql`, `Report.to_sql` and `Report.to_substrait` are the stable way to a plan.


[engines.to_sql()](engines.to_sql.md#sverify.engines.to_sql)  
SQL for a Substrait JSON plan, with the semantics `Rel.eval` gives it.

[engines.substrait_json()](engines.substrait_json.md#sverify.engines.substrait_json)  
Compile DuckDB's SQL to a Substrait plan with sverify's lift

[engines.written_plan()](engines.written_plan.md#sverify.engines.written_plan)  
The plan as Lean parsed it, written back out from its `Rel`

[engines.run_substrait_json()](engines.run_substrait_json.md#sverify.engines.run_substrait_json)  
Run a Substrait plan on DataFusion.

[engines.delta_plans()](engines.delta_plans.md#sverify.engines.delta_plans)  
Ask Lean for the weighted delta plans of a Substrait JSON plan; the


## Testing


Test transforms and their contracts with pytest (`sverify.testing`). Installing sverify registers a pytest plugin with the fixtures `sv_source` (in-memory sources) and `sv_engine` (a test per installed engine).


[testing.assert_contract()](testing.assert_contract.md#sverify.testing.assert_contract)  
Assert that a node's contract is proved, and that it holds on `data`.

[testing.assert_engines_agree()](testing.assert_engines_agree.md#sverify.testing.assert_engines_agree)  
Assert that every engine gives the same rows for a node on `data`.

[testing.cases()](testing.cases.md#sverify.testing.cases)  
A Hypothesis strategy of input tables that meet a node's preconditions.

[testing.source()](testing.source.md#sverify.testing.source)  
An in-memory source (`sverify.io.StaticSource`) holding `rows`.

[testing.installed_engines()](testing.installed_engines.md#sverify.testing.installed_engines)  
The engines of `sverify.engines.ENGINES` that can run here: DuckDB


## Command line


The `sverify` command (`sverify.cli`): `check`, `suggest`, `refresh` and `explain` a pipeline's file from a shell, a CI job or an agent.


[cli.main()](cli.main.md#sverify.cli.main)  
Run the `sverify` command with `argv` (default: `sys.argv[1:]`) and

[cli.discover()](cli.discover.md#sverify.cli.discover)  
Import the Python file at `path` without running its pipelines, and

[cli.summary()](cli.summary.md#sverify.cli.summary)  
What a report's contract means for the data, in words:

[cli.Discovery](cli.Discovery.md#sverify.cli.Discovery)  
What `discover` found in a file.

[cli.Checked](cli.Checked.md#sverify.cli.Checked)  
One application of a contracted transform in the file, and its proof.


## Standards


Contracts in the Open Data Contract Standard (`sverify.odcs`, \#791): a node's contract written as ODCS, and ODCS contracts read as conditions.


[odcs.export()](odcs.export.md#sverify.odcs.export)  
The contract of `node` as an ODCS document (`ODCS_VERSION`).

[odcs.write()](odcs.write.md#sverify.odcs.write)  
Write `export(node, **kwargs)` to `path`: JSON for a `.json` file,

[odcs.read()](odcs.read.md#sverify.odcs.read)  
Read an ODCS contract as conditions.

[odcs.OdcsContract](odcs.OdcsContract.md#sverify.odcs.OdcsContract)  
An ODCS contract as `read` gives it.

[odcs.Unread](odcs.Unread.md#sverify.odcs.Unread)  
A rule of an ODCS contract that `read` could not read as a condition.

[odcs.UnreadRuleWarning](odcs.UnreadRuleWarning.md#sverify.odcs.UnreadRuleWarning)  
`read` met rules it cannot read as conditions; `OdcsContract.unread`


## Errors


What sverify raises, and when (`sverify.errors`).


[errors.SverifyError](errors.SverifyError.md#sverify.errors.SverifyError)  
The base of every exception sverify raises on purpose: a refusal

[errors.VerificationError](errors.VerificationError.md#sverify.errors.VerificationError)  
A postcondition, or the absence of runtime errors, could not be proved.

[errors.PreconditionError](errors.PreconditionError.md#sverify.errors.PreconditionError)  
Input data violates a precondition.

[errors.PostconditionError](errors.PostconditionError.md#sverify.errors.PostconditionError)  
Output data violates a postcondition (only raised by runtime checks).

[errors.CompositionError](errors.CompositionError.md#sverify.errors.CompositionError)  
A contracted transformation's precondition on an input is not implied

[errors.NotIncremental](errors.NotIncremental.md#sverify.errors.NotIncremental)  
The plan is outside the fragment with verified delta rules.

[errors.AuditError](errors.AuditError.md#sverify.errors.AuditError)  
In audit mode, the change feed or a view disagrees with recomputation.

[errors.SchemaError](errors.SchemaError.md#sverify.errors.SchemaError)  
A source's new schema cannot be read in the old one, and a node

[errors.SqlError](errors.SqlError.md#sverify.errors.SqlError)  
A SQL producer refused a query.

[errors.ExportError](errors.ExportError.md#sverify.errors.ExportError)  
The plan has no conforming Substrait form that keeps its proof: the

[errors.Unsupported](errors.Unsupported.md#sverify.errors.Unsupported)  
Sverify refuses the input: the SQL lift or the Ibis producer cannot