Systems Researcher | Compilers & Distributed Runtimes
"The more you know, the more you know you don't know."
BSIT Graduate (June 2026, Colegio de Montalban) focused on formal verification, runtime security, and low-level systems architecture. I build compilers, virtual machines, and distributed execution engines from first principles.
- Core Focus: Formal Methods, Runtime Security, Systems Architecture.
- Primary Languages: Rust for core infrastructure, Zig for native interception, Python and JavaScript/TypeScript for orchestration and tooling.
- Web Stack: Next.js and FastAPI for web applications and APIs.
A selection of open-source projects covering language verification, runtime security, distributed engines, and steganographic systems.
| Repository | Project Specification | Technologies |
|---|---|---|
| Lirien | A verifying JIT compiler for a safe subset of Python. Uses Z3 SMT verification to statically prove refinement types, memory bounds, and safety invariants before lowering to native code with Cranelift. | |
| Nimue | A selective Rust code virtualization and obfuscation framework. Transforms sensitive Rust functions into dynamically generated virtual machine instructions executed by a hardened Zig kernel. | |
| Astraea | A security middleware for Node.js implementing Object-Capability enforcement at the native boundary via dynamic C-ABI syscall hijacking (Zig) and kernel Seccomp-BPF filters. | |
| Iris | A distributed actor runtime in Rust with Python bindings, featuring a reduction-based cooperative scheduler, location-transparent messaging, and live actor code updates. | |
| Causm | A domain-specific research language addressing concurrent non-determinism through explicit temporal pacing, entropic state decay, and Z3-checked correctness guards. | |
| Ocular | An instruction-level tracer and telemetry runtime for Python 3.12+ (PEP 669). Uses hardware TSC cycle counting and adaptive de-instrumentation to minimize profiling overhead. | |
| MirageFS | A steganographic virtual block device (FUSE / WebDAV) that mounts encrypted filesystems inside media containers (PNG, MP4, MP3) with custom format-specific injectors. | |
| Argus | An entropy-based security scanner combining Aho-Corasick pattern matching with Shannon entropy analysis to detect secrets and credentials in source repositories. |
- Systems & Runtimes: Building core infrastructure and low-level runtimes in Rust, paired with Python or Node.js for high-level APIs.
- Compilers & Formal Methods: Designing DSLs and JIT pipelines backed by SMT solvers (Z3) to guarantee safety constraints at compile time.
- Security & Systems Internals: C-ABI dynamic interception using Zig, Linux Seccomp-BPF sandboxing, and binary obfuscation/steganography research.
- Web Engineering: Building web applications and backend services with Next.js and FastAPI.
|
|
