whoami
I prove backend systems are correct — not just that they compile.
Nguyễn Tiến Đạt. Backend engineer in Hanoi, building Java & Go systems — and increasingly, verifying them formally with Z3.
01
The Ledger
claim → evidence → verdict
API Billing Platform · abp
Concurrent merchant top-ups never lose an update, even under load.
load-tested
- Atomic
INSERT … ON CONFLICT DO UPDATE — not a read-then-write race — plus a DB-level unique constraint so double-subscribes can't slip through an app-level check.
- Per-merchant Resilience4j bulkhead + circuit breaker, so one broken merchant can't starve every other tenant's requests.
- Redis cache-aside for merchant routing/pricing (read:write ratio ~10⁵), with a fail-open
CacheErrorHandler — a dead cache degrades the path, it doesn't take the gateway down.
- RabbitMQ drives the operational write; the same event republishes to Kafka, partitioned by merchant, as a durable and independently replayable audit log.
- Proven with dedicated k6 load tests and Testcontainers integration tests, not just unit coverage.
JavaSpring BootResilience4j
KafkaRabbitMQRedisPostgreSQL
View repo
Skolem
Two SQL queries are semantically equivalent — or here's the exact row where they disagree.
Z3-backed
- Formal equivalence checking via Z3 SMT solving — deterministic proof, not linting or heuristics.
- Three surfaces on one engine: a web UI, a CI/CD JSON endpoint, and an MCP server so AI coding agents call verification in-loop, powering a counterexample-driven self-healing repair.
- Fails closed on unsupported SQL — an unencodable predicate is rejected, never silently dropped into a false "equivalent."
- A
divergent verdict is re-run against a concrete SQLite witness before being trusted, catching encoder bugs instead of showing a fake counterexample.
- Auth, per-project API keys, Supabase/Postgres with RLS, billing via Lemon Squeezy, circuit breaker on LLM calls.
PythonFastAPIZ3 / SMTSupabaseDocker
View repo
InstaClone
Sessions survive a horizontal scale-out, not just a single instance.
containerized
- Google OAuth2 login via Spring Security with auto-provisioned users.
- Redis-backed distributed HTTP sessions (Spring Session) — sessions live outside the JVM, so any instance can serve any request.
- MinIO (S3-compatible) object storage for image uploads.
- Centralized exception handling via
@RestControllerAdvice, mapping domain exceptions to stable HTTP codes.
- Full stack — MySQL, Redis, MinIO, backend — containerized with Docker Compose; API documented via auto-generated OpenAPI.
Java 21Spring Boot 3.5Spring SecurityRedisMySQLMinIO
View repo
go-api-gateway
Routes can change at runtime — no restart, no hand-written SQL.
thread-safe
- SQLite-backed route table matched on path, method, and header, behind a router guarded by
sync.RWMutex — concurrent reads under exclusive writes.
- Runtime admin API to register routes on the fly, persisted immediately for the next startup.
- Two pluggable rate limiters (token bucket, fixed window) — defaults to token bucket to avoid the boundary-burst problem fixed windows allow at the edges.
GoSQLite
View repo
arxiv-lens
Two extraction runs on the same papers must produce the same graph — or the build refuses to ship.
drift-gated
- Closed ontology — 6 entity types, 6 relations with domain/range constraints — enforced as a decoding constraint on structured extraction, a mechanical repair rule for schema violations, and a canonicalization tiebreak, not schema-free extraction.
- A structural drift gate diffs snapshot N against N+1 and exits non-zero the moment unchanged inputs produce a different graph, refusing to promote a bad build into Neo4j.
- Z3 encodes the ontology's transitivity, asymmetry, and irreflexivity, surfacing a minimal unsat core for contradictions that span multiple papers — no single paper wrong on its own.
- Two services glued by Kafka (async
graph.updated) and gRPC (sync queries): a hexagonal Spring Boot query-service whose Caffeine cache-aside layer cuts /api/stats from a 4.1s cold traversal to 8ms cached.
- Benchmarked against a conventional vector-RAG baseline on the same golden questions — full paper recall vs. 61% for vector search, and vector retrieval can't represent "no relationship exists" since top-k always returns k results.
JavaSpring BootPython
KafkagRPCNeo4jZ3 / SMTDocker
View repo
02
Filed & Reviewed
open source
Ran the full compiler matrix weekly instead of every PR — cut CI jobs per pull request from 28 to 11.
merged
Made BulkheadConfig's constructor protected to allow subclassing for custom metadata, with a test proving it.
under review
Self-found a silent-null-return bug in getSeleniumAddress(); replaced it with a fail-fast exception.
under review
03
Before the Proofs
constraint solving, academic
Bachelor's Thesis
AlienTile
Solver comparison for a tiling/coloring problem across CP-SAT, CPLEX (CP & ILP), and Gurobi.
View repo →
Related work
BoardPackagingSATConvert
Pseudo-Boolean SAT encoding for the Board Packing Problem, in Java.
View repo →
ESLab
UniCorT
SAT/MaxSAT university course timetabling via Google OR-Tools CP-SAT.
View repo →