API Reference

Contracts

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

transform(): Decorate a function from Ibis tables to an Ibis table with a contract.
verify(): Try to prove ensures about query (an Ibis table expression or a
unique(): A key: at most one row per combination of cols.
key(): A primary key: at most one row per combination of cols, and no NULL
references(): A foreign key: every non-NULL value of col occurs in the column to
Report: What the checker proved about a transformation, returned by verify and kept
Report.from_substrait(): Read a plan to_substrait exported, and prove its contract again

Report Methods

Methods for the Report class

Report.to_json(): The report as a versioned JSON document, for CI jobs and tools
Report.from_json(): A report from what to_json wrote, by this version of sverify or
Report.from_substrait(): Read a plan to_substrait exported, and prove its contract again
Report.to_substrait(): The verified plan for any conforming Substrait consumer, with its
Report.substrait_contract(): The contract to_substrait embeds, as JSON, for a sidecar file.
Report.to_sql(): The verified plan as SQL whose meaning is the proof’s, in
Report.check_inputs(): Check the preconditions (requires, the inferred bounds among
Report.run(): Run the plan this report checked (plan) over the tables of
Report.proved: Every postcondition holds and no runtime error is possible. With
Report.floats_unmet: Why no engine’s doubles meet the observation’s floats (exact
Report.needed: With on_inferred="error", the preconditions the proof needs that
Report.needed_text: needed in words: per input table and operation, the preconditions
Report.equivalence: The equivalence the result is proved up to: sv.equivalent(...) in
Report.needs: needed as data, one Needed per precondition: the table, the
Report.needed_conditions: needs as conditions, per input table, ready for requires=: Ibis
Report.needs_text(): Deprecated: needed_text lists every needed precondition.
Report.needs_lines(): Deprecated: the property needed_text.
Report.errors: The issues an engine fails on at run time (Issue.error is true).
Report.warnings: The issues that do not count against a proof. None do: an
Report.suggestions: For each unproved postcondition with one, the preconditions per
Report.unproved: The postconditions in ensures that were not proved.
Report.notes: What the report notes about the result as a whole, as str(report)
Report.route(): The route by which run would take the plan to engine, and the
Report.verdict: The report’s first line: “proved”, or “NOT proved:” and what is
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: The result of a contracted transform over sources or other nodes.
sql.Unsupported: The plan is outside the Lean model, or the dialect cannot express it.
sql.Dialect: SQL syntax and semantics of one engine.
sql.parse_plan(): Read a Substrait JSON plan (as a dict) into the model, as parsePlan does.
sql.to_sql(): SQL for a Substrait JSON plan, with the semantics Rel.eval gives it.
sql.dialect_of(): The Dialect named dialect ("duckdb", "snowflake" or
sql.Kind: What a value is in SQL. time is a microsecond TIMESTAMP without time
sql.DIALECTS
group(): Several nodes to refresh together, against the same source versions:
io.Changes: Rows to insert into and delete from one table (bag semantics: each
nodes.Group: Nodes refreshed together; see group.
nodes.Refresh: What a refresh did, node by node, upstream first: returned by
nodes.Status: Where each node of a group stands: returned by Node.status and
nodes.NodeStatus: Where one node stands; see Node.status. str() gives one line,
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.schema: The node’s columns and their types, known when the node is built.
Node.internal_plan: The Substrait plan (JSON) of the node’s stage, as Lean checked and
Node.plan: Deprecated: internal_plan, sverify’s own form of the plan
Node.report: The Report of the contract that made the node’s result: the
Node.to_substrait(): The node’s verified plan for any conforming Substrait consumer,
Node.to_sql(): The node’s stage as SQL, in dialect: what refresh runs for a
Node.pipe(): Apply step to this node, left to right: orders.pipe(paid) is
Node.write(): Store this node in sink (sverify.io.DeltaSink, IcebergSink),
Node.refresh(): Bring this node and every node it reads up to date, and write the
Node.status(): Where the node stands: the source versions of its state, where it
Node.table: The node’s state as an Ibis table, to query further.
Node.versions: The version of every source the node’s state reflects, by name,
Node.to_arrow(): The node’s state as an Arrow table.
Node.quarantined(): The rows of the node’s sources set aside by `on_violation=
Node.to_polars(): The node’s state as a Polars DataFrame (needs polars).
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: A Delta table read by version, as the input of transforms.
io.DeltaSink: Stores a node in a Delta table, exactly once per state:
io.IcebergSource: An Iceberg table of a catalog, read by snapshot sequence number, as
io.IcebergSink: Stores a node in an Iceberg table, exactly once per state:
io.StaticSource: An in-memory Arrow table as a source, such as a small lookup table or
io.SinkWrite: What storing a node’s state did, in any sink.
io.Contract: What a sink records with each commit: which plan produced the data,
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: A table you read yourself: subclass it and implement read.
io.Batch: What a Source read: new rows and the cursor to read from next time.
io.from_query(): A source that reads new rows by a high-water mark: fn(since)
io.from_frame(): A source that reads the whole table on every refresh: fn() returns
io.from_files(): A source that reads the files dropped in a directory: each refresh
io.Sink: Where node.write(sink) stores a node: subclass it and implement
io.SinkChange: What a sink writes for one state of its node: the change since the
io.sink_from(): A sink that hands the node’s whole table to fn whenever it
io.VersionedSource: What a pipeline needs of a source: a table with integer versions that
io.Snapshot: A table at one version, as a source hands it to a pipeline: what
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(): A new, empty connection whose plans run on engine.
engines.run(): Run a plan in Lean’s written form on engine (default: the
engines.ENGINES: The engines a Connection runs plans on: "duckdb" (the default),
engines.Connection: Named Arrow tables, and the engine that runs plans over them.
engines.Dialect: SQL syntax and semantics of one engine.
engines.DUCKDB
engines.SNOWFLAKE
engines.SPARK
engines.Unsupported: Sverify refuses the input: the SQL lift or the Ibis producer cannot
engines.SPARK_CONF
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(): 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(): SQL for a Substrait JSON plan, with the semantics Rel.eval gives it.
engines.substrait_json(): Compile DuckDB’s SQL to a Substrait plan with sverify’s lift
engines.written_plan(): The plan as Lean parsed it, written back out from its Rel
engines.run_substrait_json(): Run a Substrait plan on DataFusion.
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(): Assert that a node’s contract is proved, and that it holds on data.
testing.assert_engines_agree(): Assert that every engine gives the same rows for a node on data.
testing.cases(): A Hypothesis strategy of input tables that meet a node’s preconditions.
testing.source(): An in-memory source (sverify.io.StaticSource) holding rows.
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(): Run the sverify command with argv (default: sys.argv[1:]) and
cli.discover(): Import the Python file at path without running its pipelines, and
cli.summary(): What a report’s contract means for the data, in words:
cli.Discovery: What discover found in a file.
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(): The contract of node as an ODCS document (ODCS_VERSION).
odcs.write(): Write export(node, **kwargs) to path: JSON for a .json file,
odcs.read(): Read an ODCS contract as conditions.
odcs.OdcsContract: An ODCS contract as read gives it.
odcs.Unread: A rule of an ODCS contract that read could not read as a condition.
odcs.UnreadRuleWarning: read met rules it cannot read as conditions; OdcsContract.unread

Errors

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

errors.SverifyError: The base of every exception sverify raises on purpose: a refusal
errors.VerificationError: A postcondition, or the absence of runtime errors, could not be proved.
errors.PreconditionError: Input data violates a precondition.
errors.PostconditionError: Output data violates a postcondition (only raised by runtime checks).
errors.CompositionError: A contracted transformation’s precondition on an input is not implied
errors.NotIncremental: The plan is outside the fragment with verified delta rules.
errors.AuditError: In audit mode, the change feed or a view disagrees with recomputation.
errors.SchemaError: A source’s new schema cannot be read in the old one, and a node
errors.SqlError: A SQL producer refused a query.
errors.ExportError: The plan has no conforming Substrait form that keeps its proof: the
errors.Unsupported: Sverify refuses the input: the SQL lift or the Ibis producer cannot