Six-property safety framework combining DFA deny rules, TLA+-verified FSM compliance, Kani-proved taint tracking, and LoRA-based semantic judgment. Composition theorem: Lamport (TLA+) × Denning (lattice) for full-stack agent safety.

One Bit at a Time: measuring how LLM compositional reasoning accuracy degrades exponentially with chain length and state complexity. Formula: η = k · exp(−akn), validated across 14 models and 3 task families.

Automated formal verification of quantized ML kernels against the RISC-V Vector ISA specification. Three-layer proof pipeline: MLIR spec ↔ LLVM IR ↔ Isla ISA traces, all checked by Z3.