I build systems that bridge Generative AI, Formal Verification, and High-Throughput Network Plumbing.
My work focuses on the intersection of probabilistic models and deterministic guarantees:
- 🧠 Neurosymbolic AI & LLMs: Harnessing modern LLMs to synthesize code patches, coupled with Z3 SMT solvers that mathematically prove safety before a single line ships.
- ⚡ Zero-Disk Media Streaming: Custom byte-range proxies translating HTTP
Rangerequests into real-time MTProto chunks without touching the server's disk. - 🌐 Real-Time Synchronized Web Apps: Reactive multi-client sync architectures on Next.js, WebSockets, and Prisma.
I spend most of my time on what happens off the happy path: memory ceilings, token budgets, failure recovery, concurrency locks, and where the trust boundaries sit.
| VeriFix: Binding LLM generative synthesis to Z3 SMT formal verification in a self-healing CEGIS loop. | Tagged releases of CineVault and TeleVault: Streaming multi-gigabyte media with flat memory ceilings. | Ace Hub and AceUnzipBot: Lockstep watch-parties and FIFO MTProto workers. |
Ask me about:
Generative AI & LLMs · Z3 SMT Formal Verification · CEGIS Loops · MTProto / Telethon · HTTP Range Requests · Async Python Concurrency · Docker in Production
🛡️ VeriFixNeurosymbolic code repair: LLM generative patching meets Z3 formal verification. Combines LLMs with an SMT constraint solver in a CounterExample-Guided Inductive Synthesis (CEGIS) loop. Solvers mathematically prove patches or generate concrete counterexample models to trigger LLM self-correction.
|
Netflix-style discovery and streaming, powered by Telegram. Search for a title, press play, and the bytes flow from Telegram directly to the browser or VLC player via HTTP range requests. No persistent media storage on the server.
|
|
A private media library with a custom browser player. Playback runs on zero-disk byte-range streaming, thumbnails are WebP, and access is locked down with security-focused controls, including Argon2id hashing.
|
Bulk archive extraction inside Telegram. Powered by 7-Zip. Jobs run through an asynchronous FIFO queue with live progress bars and thumbnails, plus a dedicated CLI and VPS deployment tooling.
|
🍿 Ace HubVideo discovery and synchronized watch parties. Real-time playback sync keeps every viewer in lockstep, on a responsive modern interface backed by a Prisma-managed database and WebSockets.
|
|
Note
Probabilistic generation needs deterministic verification. LLMs generate intuitive patches; the Z3 SMT solver either mathematically proves the contract or extracts the exact failing edge-case input.
flowchart LR
A["Buggy Code + Spec<br/>(@requires / @ensures)"] --> B["Symbolic Executor<br/>AST & Path Constraints"]
B --> C{"Z3 SMT Solver<br/>Satisfiability Check"}
C -->|"UNSAT<br/>(No counterexamples)"| D["✔ Formally Proven Sound<br/>Ready for Production"]
C -->|"SAT<br/>(Violation found)"| E["Concrete Counterexample<br/>(e.g., x=None, amt > bal)"]
E --> F["LLM Patch Generator<br/>(Prompt + Concrete Failure Model)"]
F --> G["AST Patcher<br/>Apply Candidate"]
G --> B
Note
The server is a pipe, not a warehouse. Bytes move from Telegram to the client player as they are requested, and nothing is retained on disk.
flowchart LR
A["Player<br/>Browser / VLC"] -->|"GET + Range: bytes=a-b"| B["FastAPI<br/>Auth & Range Parser"]
B -->|"Chunk requests (1 MiB)"| C["Telethon<br/>MTProto Client"]
C <-->|"Encrypted MTProto"| D[("Telegram Datacenter")]
B -.->|"206 Partial Content<br/>Streamed chunk-by-chunk"| A
- Range-first: Each
Range: bytes=a-brequest maps directly to the minimal set of MTProto chunk fetches. - Flat memory: Chunks stream into the HTTP response buffer on the fly. Memory use stays constant regardless of whether the file is 50 MB or 10 GB.
- Immediate cancellation: When the viewer scrubs or disconnects, the in-flight MTProto stream is aborted immediately.
pie title Stack & Engineering Focus
"AI & Neurosymbolic Systems (LLMs + Z3)" : 35
"Zero-Disk Streaming & MTProto" : 30
"Real-Time Sockets & Next.js" : 20
"Systems, Docker & Linux Ops" : 15
| Principle | In practice |
|---|---|
| Prove, don't guess | LLMs propose candidate solutions; formal SMT solvers mathematically verify correctness before deployment. |
| Stream, don't store | Data flows from source to client. Nothing sits on the server waiting to be pruned. |
| Bound everything | Memory, concurrency, LLM token limits, and queue depths all have explicit hard ceilings. |
| Automate the repetitive | If I do it twice by hand, it becomes a script, a background queue, or a service. |
| Design for failure | Retries, cancellation, and recovery are fundamental architectural pillars, not post-incident patches. |
| Keep trust boundaries explicit | Cryptographic hashing (Argon2id), auth tokens, and permissions live at strictly drawn edges. |
| AI & Verification |
|
| Languages |
|
| Backend |
|
| Frontend |
|
| Real-Time |
|
| Data & Security |
|
| Ops & Infra |
|
- AI & Neurosymbolic Engineering: LLM agent tool calling, structured generation, CEGIS self-repair, SMT formal contract proofs.
- Telegram Automation & MTProto: Telethon userbots, bot transactions, high-volume queue workers, MTProto chunk streaming.
- Zero-Disk Streaming Engines: Range-request media proxies that stream directly from cloud networks with flat memory.
- Real-Time Collaborative Apps: Synchronized state, WebSockets, Next.js frontend architectures.
- Production Hardening: Dockerizing complex Python/Node runtimes, systemd daemon management, secure reverse proxies.
Got an ambitious challenge involving LLMs & AI, formal verification, streaming infrastructure, or real-time systems? Message me on Telegram or send an email.