Recent B.Eng. graduate (Information Technology, Centria, 2026) who builds production-grade backend systems, full-stack products and infrastructure — Python/FastAPI and Go, React and TypeScript, Kubernetes and cloud — with a strong testing and observability habit. Independently formally-verified a capability-security kernel in Rust and Lean4.

A housing search and eligibility-application platform for a Finnish non-profit housing operator, across four regulated housing forms.

• Full pipeline driven live end to end against the real deployment: search → application → adaptive eligibility form → rule-engine decision with cited evidence → admin ranking by need, wealth and income — every outcome backed by a rule id and the exact numbers compared.
• 10-table Postgres schema with meaning encoded in the DDL: rent/price XOR constraint, a row-locking trigger that makes viewing-capacity overbooking structurally impossible under concurrency.
• 14-rule eligibility engine, every rule a pure function of (application, apartment, limits) — no clock, session or database read inside a rule — with a generated rule catalogue CI fails on drift against.
• Deployed on Vercel (Neon Postgres) as two projects, frontend and API; CI runs backend (ruff, mypy strict, pytest) and frontend (eslint, tsc, vitest, next build) independently.

A formally-verified capability-security kernel (TCB) for AI agents.

• 1,096 tests; zero use of `sorry` anywhere in the Lean4 proofs.
• Typed SemanticGate trait and a RightsViolationMetric — authority is a first-class, provable property, not a runtime check bolted on after the fact.

Async multi-tenant SaaS backend that detects silent data-pipeline failures before anyone notices the data is wrong.

• 346 tests; RS256 JWT auth; RBAC (VIEWER < MEMBER < ADMIN < OWNER); Clean Architecture with Protocol ports.
• Silent-failure detection: a run reporting SUCCEEDED with zero records processed is re-classified and alerted CRITICAL.
• Latency drift caught via rolling p50/p95 + z-score anomaly detection, not a static threshold.

A log-analytics pipeline: Kafka-buffered ingestion, full-text-searchable Postgres storage, and real-time alerting.

• Four services (ingestion, processor, query, alerting) connected by a dead-letter queue with idempotent re-delivery.
• Redis rate limiting and query caching in front of the search path.

Namespace-based multi-tenant isolation on Kubernetes — his thesis, extended into a research project.

• Three formally-defined metrics: Interference Index, Resource Fairness Deviation, Autoscaling Stability Score.
• A federated-learning extension with differential privacy and Byzantine-robust aggregation; 111 tests at 100% coverage.

A bike-taxi platform: rider, driver and admin PWAs on one FastAPI backend with live WebSocket ride tracking.

• Installable PWAs for iOS and Android; Stripe payments, Mapbox navigation, phone OTP and Google OAuth.
• Admin KPI dashboard with CSV exports.