ancycle
Formal verification
for data pipelines.
Ancycle parses your SQL, builds a constraint model, and feeds it to the Z3 theorem prover. It finds logical contradictions in your DAG natively before any compute is provisioned.
Early Access: Ancycle Cloud
ACCESS GRANTED
You are on the list. We'll deploy your API keys shortly.
bun src/cli/demo.ts
$ ancycle verify pipelines/core.sql
Read [stg_active_users]: Constraints → (= status "active")
Read [process_churned]: Depends on → [stg_active_users]
Read [process_churned]: Constraints → (= status "churned")
Checking constraints with Z3 shadow...
❌ FATAL: Z3 QF_S Resolution: UNSAT
↳ [process_churned] is guaranteed to process 0 rows.
Upstream and downstream filters are mutually exclusive.
Compute provisioned: $0.00
Wall time: 0.04s
_