Security of VMs & Containers
Hardening the boundary between guest and host: hypervisor escapes, namespace and cgroup isolation, seccomp/eBPF policy, sandboxes like gVisor and Kata, and the supply chain that ships into your images.
Writing and experiments from Florida's Space Coast — across systems security, formal mathematics, orbital mechanics, synthetic biology, and the tools in between. Eight payloads, one launch site.
Each area is its own orbit — different regime, different math, but launched from the same place and reasoned about with the same tools. Designators encode the domain, not a ranking.
Hardening the boundary between guest and host: hypervisor escapes, namespace and cgroup isolation, seccomp/eBPF policy, sandboxes like gVisor and Kata, and the supply chain that ships into your images.
Building a keyboard-native editing environment from Lua up: LSP, Treesitter, tuned motions, and the small ergonomic decisions that compound over a decade at the terminal.
LLMs as reasoning substrates, multi-agent swarms and the emergent behavior they produce collectively, and the ML foundations underneath. Where individual agents are simple and the group is not.
The algebra of composition that quietly underlies everything else here: functors, natural transformations, adjunctions, and monads — structure that lets ideas move between fields without losing their shape.
Machine-checked mathematics with dependent types. Writing proofs a computer will actually verify, chasing tactic automation, and treating correctness as something you compile rather than hope for.
Orbital mechanics for LEO: injection, decay, station-keeping, and rendezvous. Watched from the coastline it launched from — reasoning about the cadence of the Cape and the smallsats it lofts.
Toward programming languages for the genetic engineering of living cells: cells as a programmable substrate, genetic circuits as compiled logic, and DSLs that let you write a phenotype and lower it to DNA.
The DOS-and-early-Windows era and the craft of keeping it runnable: preservation, emulation, sound-card archaeology, and the demoscene that pushed those machines past spec.
Long-form entries as they clear review. Placeholders below mark the first three on the pad.
A walk through modern VM isolation and where the seams still show — from paravirtualized devices to the parts of the attack surface that never went away.
Read entry FLIGHT LOG // pendingUsing orbital rendezvous as an honest picture of composition: why the awkward part of gluing effects together is exactly the interesting part.
Read entry FLIGHT LOG // pendingWhat a real programming language for living cells would need — types for biology, a standard library of parts, and what “undefined behavior” means when the target is alive.
Read entryspacecoast.dev is a working notebook for someone who refuses to pick a single lane. The through-line isn't a topic — it's a method: build the boundary carefully, prove what you can, and treat living cells, virtual machines, and orbits as systems you can reason about precisely.
Category theory is the connective tissue; Lean and Rocq are where the arguments get checked; the Cape is out the window. Expect deep dives, half-finished experiments, and the occasional retro machine brought back from the dead.