Selected work
Ten projects that show what I do: AI agents on production data, migrations against a deadline, warehouses at 100 TB, and correctness you can prove.
Projects done for an employer are described without internal names or commercial details.
An AI-agent platform for a data team
A 12-engineer team owns the billing data of millions of sellers: Greenplum, ClickHouse, PostgreSQL, Kafka, Airflow and a dozen internal systems around them.
- Built: an MCP server with 100+ tools over 15 systems, with read/write annotations, tool allowlists and personal read-only database roles; an autonomous on-call agent; an agentic merge-request reviewer with a job queue, CI integration and an egress-allowlisted sandbox. All of it sits under a 21-ADR security architecture.
- Measured: on a benchmark the reviewer found 6 of 7 reference issues, against about 2.5 for diff-only LLM review. Its first production run produced 15 findings with zero false positives.
- Then paused it ourselves for a formal security review, with a threat model and the open questions ready. Our own reviews found real gaps on the way, and the fixes are written. The formal review is still pending, so both agents stay paused, while agentic review keeps running in production at Groupsi, my startup.
Racing an int32 overflow across three database engines
Product IDs reached 93.5% of the 32-bit range and grew by up to 20 million a day. Every key column in ClickHouse, Greenplum and PostgreSQL had to become 64-bit before the first ID crossed 2³¹.
- Mapped who breaks on a type change: typed Go clients fail at once on any width mismatch, HTTP clients stay silent until the overflow, join tables need exact types.
- Migrated three ClickHouse clusters in a week. Copied 4.7 TB of partitioned PostgreSQL tables into 64-bit twins with a schema swap, without the parent-table lock that
PARTITION OFtakes, and under a WAL budget so that replicas in other datacenters kept up. - Found five live functions that would have failed on the first large ID, one of them called 8.7 million times. The final check was a query that returns only violations.
A global lock in ClickHouse behind portal timeouts
A dashboard widget took a ClickHouse cluster down for 48 minutes while 65 of 80 cores per node sat idle.
- Traced it to a global mutex in the query context: each node handled about 58,000 acquisitions per second, and the widget's query cost 6,849 of them.
- Benchmarked three ClickHouse versions and showed that the upstream fix never reached the 23.8 LTS line.
- Rebuilt the query path around lock cost per query: the widget's call became 30 times cheaper and the portal got about 5x throughput, with no new hardware.
Disaster recovery for a 98 TiB Greenplum warehouse
The warehouse had no copy in a second datacenter, and the commercial replication edition was not available.
- Measured the write side first: about 40 TB of WAL a day. Evaluated five replication strategies against it and the real network between datacenters, down to which 10-gigabit links saturate first.
- Sized the mirrors from storage metadata in 40 seconds, without heavy queries to production, and found 26 TiB to cut before buying anything: test databases, an uncompressed raw Kafka tail nobody read, stale default partitions.
- Found the root cause of the waste: the default storage options created uncompressed heap partitions and columns whenever DDL omitted them, 13.5 TiB in total.
Moving a warehouse off SQL Server, and a cluster between datacenters
Two migrations of the same billing data: one across database engines, one across datacenters.
- Led the six-month move of the billing calculations from Microsoft SQL Server to Greenplum and ClickHouse.
- Moved a 12.7 TB ClickHouse cluster between datacenters. Inventoried what replication does not carry (users, 27 SQL functions, dictionaries, tables without replicas), rehearsed native incremental backup and restore through S3, and verified all four replicas down to a 75-billion-row table with a read-only test harness.
An Iceberg lakehouse pilot on S3
A pilot for a billing data organization of several teams, with a petabyte-scale target.
- Ran the data team's production Spark job unchanged on Iceberg and built exactly-once ingestion from Kafka.
- Established which readers work with which table versions across Spark, Trino and ClickHouse, and measured the metastore ceiling at 2–4 commits per second per table. Along the way, a neighboring team's long-standing bug turned out to be a single server flag in the metastore.
- Wrote 11 ADRs and ran disaster-recovery drills.
Launching a billing data platform in a new country
A country rollout of fee and stock data, in a separate environment with its own ClickHouse and PostgreSQL.
- Found that the country filters saw 2 of about 35 local sellers and silently dropped about 97% of the flow: a seller had two IDs, and a directory kept assigning them to the home country from an outdated list. The fix keyed on the right directory.
- Inventoried the core fee logic to decide what to move and what was dead.
- Designed the warehouse integration as a push receiver instead of Kafka sinks; the warehouse team adopted it as the shared scheme for every country, the home market included.
Formal methods on production billing
In one day, seven verification tools (Z3, TLA+, Dafny, Lean, Gobra, VeriEQL, SQLSolver) ran against a real Go and SQL billing system.
- Linked executable specifications to the production code and compared the tools on the same targets.
- Proved one payment law in Lean and checked it against a verbatim copy of the code on 1,006,000 inputs.
- 42 findings in calculation, versioning and synchronization logic.
BendKV: a Redis-compatible server with a verified core
Built in twelve days with a team of AI coding agents, about 100 pull requests.
- The core is checked against 68 laws, among them key isolation, TTL, pipelines and crash recovery of the append-only file at any byte. The proofs are checked by Bend and by a kernel proved sound in Lean.
- Passes 1,769 of the 1,812 tests of Redis 7.2.16 and the redis-py and go-redis suites.
- Differential testing against Redis found nine bugs in Redis and Valkey.
Groupsi: a health-tech startup run with coding agents
Groupsi is online group therapy for teenagers and adults in Brazil: small groups meet by video with a licensed psychologist, through schools, universities and employers or directly. Its promise in Portuguese: terapia em grupo online para jovens e adultos. I am co-founder and CTO.
- Built the product end to end: mobile and web apps, the API, real-time group video, consent tracking and audit logging under Brazil's data-protection law (LGPD).
- Designed the production cloud platform in Terraform, with managed identities and controlled egress.
- Run engineering with agents: coding agents implement through pull requests, another agent coordinates and verifies, six review seats run in CI. About 950 commits and 450+ pull requests in ten months. One measured result: when the two models disagree, the stricter reviewer is right about four times in five, so agreement between two LLM reviewers is not independent confirmation.