Backend engineer based in Hanoi, Vietnam — I like systems that stay correct under concurrency, and I write down why a design decision was made, not just what it does.
Currently: Java/Spring Boot backend work, with a growing interest in constraint solving (Z3/SMT) applied to real developer tooling.
Java Spring Boot Resilience4j Kafka RabbitMQ PostgreSQL Redis Docker
A modular monolith for merchant API billing, split into 5 bounded contexts by data ownership rather than call patterns.
- Atomic
INSERT ... ON CONFLICT DO UPDATE+ DB-level unique constraints prevent lost updates and double-subscribes — no read-then-write races. - Per-merchant Resilience4j bulkhead + circuit breaker, so one bad 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 Redis outage degrades gracefully instead of taking the gateway down. - Dual messaging: RabbitMQ drives the operational write with queue-based load leveling; the same event is republished to Kafka (partitioned by
merchant_id) as a durable, independently replayable audit log. - UUIDv7 primary keys for B-tree write locality under high-volume inserts.
- Verified with dedicated k6 load tests and Testcontainers integration tests.
Python FastAPI Z3/SMT Supabase Docker
Given a DDL schema and two SQL queries, Skolem uses Z3 SMT solving to formally prove semantic equivalence — or produce the exact counterexample database where they diverge. Not linting, not heuristics: deterministic proof.
- Three delivery surfaces, one engine: a web UI for manual review, a CI/CD JSON endpoint for pipelines, and an MCP server so AI coding agents (Claude Code, Cursor) call verification in-loop — powering a counterexample-driven self-healing repair loop.
- Fail-closed encoding: any SQL outside the supported subset is rejected with an error rather than silently dropped (a dropped predicate could produce a false "equivalent").
- Witness cross-check: a
divergentverdict is re-run against a concrete SQLite witness before being trusted, to catch encoder bugs rather than showing a fake counterexample. - GitHub OAuth + magic-link auth, per-user API keys, Supabase/Postgres with RLS, billing via Lemon Squeezy (fails open on metering errors), circuit breaker on LLM calls.
- 7 test suites: smoke tests, regression tests from the VeriEQL paper, and differential fuzzing against SQLite.
Java 21 Spring Boot 3.5 Spring Security Redis MySQL MinIO Docker
An Instagram-style backend with a layered architecture (controller/service/repository) grouped by domain (auth, feed, profile).
- Google OAuth2 login via Spring Security with auto-provisioned users.
- Redis-backed distributed HTTP sessions (Spring Session) for horizontal scalability.
- MinIO (S3-compatible) object storage for image uploads.
- Centralized exception handling via
@RestControllerAdvice, mapping domain exceptions to stable HTTP status codes. - Full stack containerized with Docker Compose (MySQL, Redis, MinIO, backend), documented via auto-generated OpenAPI/Swagger.
Go SQLite
A dynamic API gateway: SQLite-backed route table, matched by path/method/header, behind a thread-safe router (sync.RWMutex, concurrent reads under exclusive writes).
- Runtime admin API (
POST /admin/routes) to register routes without a restart or touching SQL by hand. - Two pluggable rate-limiting strategies (token bucket, fixed window) — defaults to token bucket to avoid the boundary-burst problem fixed windows allow at window edges.
Python discord.py PostgreSQL Redis
Discord bot for Lowie's LeetCode Community, a 250-member university LeetCode practice club running since 2024.
- Contributed features: username-based profile lookup, submission embed rendering.
- Built on a SQLAlchemy-backed relational schema (problems, topics, missions) with a cogs-based command architecture.
- Collaborated through PR review cycles with teammates.
- I also contribute structured solution write-ups (approach, complexity analysis) to the club's daily-solutions channel by signing up for specific days.
- resilience4j #2503 — changed
BulkheadConfig's constructor visibility toprotectedto enable subclassing for custom metadata, with an added test. - testcontainers-java #11964 — self-identified and fixed a silent-null-return bug in
BrowserWebDriverContainer.getSeleniumAddress(), replacing it with a fail-fast exception. - google/highway #3248 (merged) — redesigned CI to run the full compiler matrix only on a weekly schedule instead of every PR, cutting CI jobs per pull request from 28 to 11.
- B.S. Computer Science, VNU University of Engineering and Technology (2022 – 2026)
- Software Engineer Intern, NAB Innovation Center — Java Spring Boot, Kafka microservices, Jenkins/Snyk/Harness
- Semi-Finalist, Code Tour 2024 (VNG-organized competitive programming event)
- AWS Cloud Practitioner · Kaggle Bronze Medal · IELTS Overall 7.0 (C1)
- AlienTile — Bachelor's Thesis: solver comparison for a tiling/coloring problem across CP-SAT, CPLEX (CP and ILP), and Gurobi.
- BoardPackagingSATConvert — related earlier work on the Board Packing Problem: pseudo-Boolean SAT encoding in Java (at-most-one placement constraints, etc.).
- UniCorT — SAT/MaxSAT-based university course timetabling (Google OR-Tools CP-SAT), built on Alexander Lemos's UniCorT with constraints for room conflicts, day/time spacing, and precedence.