Formalhuman

Tessera is a verified self-optimization loop for AI inference. Give Astra a PyTorch workload, a GPU, and a fixed formal specification. It profiles the model, writes optimized Triton kernels, constructs and repairs Lean proofs, benchmarks candidates, and keeps an optimization only when its proof checks, numerical tests pass, and it is actually faster. In our demo, Tessera optimizes RMSNorm across SmolLM2-135M-Instruct, improving full-model prefill from 6.35 ms to 5.48 ms (1.16×). The goal is to make verification scale alongside AI-generated optimization: as models increasingly improve the software underneath AI, incorrect improvements should be rejected automatically rather than discovered after deployment.