We are building a new computing stack with formally verified data, memory, and resource isolation between executions for instant, truly elastic global compute. This includes designing and building a production language with complete, mechanized formal specifications and a certifying compiler, from the start. Our immediate goals include an alternative to eBPF and building the world's first serverless networking infrastructure. We are VC-funded with runway for multiple years. The team is composed of PhDs from Stanford, UW, OSU, and Brown, advised by professors from MIT and UWaterloo.