Lean-oriented formalization work for reasoning about stack behavior, invariants, and the gap between executable systems and proof-carrying claims.
Security arguments often depend on small state transitions that are easy to describe informally and hard to preserve under implementation pressure.
This line of work explores compact formal models that make the state, operations, and invariants explicit enough to be reviewed and extended.
Formalization turns broad security statements into smaller objects: state, transitions, invariants, and proof obligations.
An evaluation scaffold for automated research workflows: scenario design, trace capture, failure review, and reproducible comparisons between agents.
A testbed for studying size, fragmentation, resolver behavior, and protocol boundaries when DNSSEC meets post-quantum cryptographic material.
A measurement-oriented harness for tracking post-quantum TLS behavior, handshake shape, certificate chains, and interoperability risks across real deployments.