Papers by research line.
Preprints and manuscripts grouped by research line.
ML / AI / Formal Systems
Evaluation records, tool-call traces, proof obligations, model boundaries, state invariants, and audit-ready run histories.
A study of mechanistic localization as a score-to-circuit pipeline, separating scorer quality from circuit quality across calibration, selection, and evaluation.
A certified Lean 4 decomposition layer for theorem-proving agents, with proof obligations, witnesses, dependencies, replay semantics, and schedule selection.
A claim-centered audit framework for selected circuits in mechanistic interpretability, reporting preservation, localization, minimality, stability, robustness, power, and structural recovery.
A runtime reference monitor for field-level authorization in tool-using agents, enforcing source-field-sink authority over typed dependency graphs before protected actions execute.
A human-adjudicated audit of IFEval strict-fail/loose-pass disagreements, separating valid corrections, loose false positives, and ambiguous cases.
Crypto / PQC / Security
Measurement artifacts, certificate-chain behavior, parser and import validation, decapsulation-test harnesses, threat models, and operational regression cases.
A black-box analysis of what confirmation-code-augmented Fujisaki-Okamoto decapsulation tests can certify, with pass bounds, list-hit obstructions, and dependency-cone limits.
A multi-surface framework for post-quantum TLS observability across passive evidence, active probing, certificate chains, registry knowledge, and explicit uncertainty.
A workflow-centric assurance framework for ML-KEM and ML-DSA in X.509, covering certificate profiles, SPKI representation, private-key import, policy registries, and mutation-based evaluation.
A state-aware study of post-quantum ACME enrollment, comparing standard issuance, reusable-authorization renewal, certificate-based fast re-enrollment, and hardened workflow variants.
A topology-aware WebAuthn recovery model for multi-account and multi-authenticator settings, with intent-bound client behavior, provenance checks, and symbolic corroboration.