Topics

Topic (verification) Formal verification is how I turn design intent into provable evidence. My approach is pragmatic: focus on proof structure, build helper assertions, and iterate using counterexamples and coverage signals. Focus: proof structure · convergence · evidence trail Methods: helper lemmas · CEX-guided refinement · coverage-aware iteration What I optimize for Fast convergence: break big goals into smaller provable claims Explainable failures: counterexamples should point to actionable causes Repeatability: artifacts, logs, and assumptions are preserved so results can be reproduced Typical workflow Scope the intent: what must be true (and under which assumptions) Define the interface: clocks/resets/handshakes; avoid underspecified properties Decompose: create a staged plan (invariants / helper lemmas first) Run and refine: use counterexamples to repair constraints and properties Measure evidence: coverage/vacuity checks; avoid “proved but meaningless” Where this shows up on my site Floating-point case study: proof decomposition + refinement Publications: canonical paper links and write-ups Want to discuss a formal verification problem? If you want to collaborate, discuss roles, or review artifacts, reach out. ...

Topic (workflows) I use GenAI where it creates leverage: generating structured artifacts, accelerating iteration loops, and reducing repetitive engineering work—while keeping an evidence trail so results remain trustworthy. Goal: faster iteration without losing rigor Approach: tool-centric pipelines · structured artifacts · reproducibility What I believe works (and what doesn’t) Works Constraining generation with structured schemas Grounding with project context (specs, IRs, signal allowlists) Using LLMs for draft → critique → repair loops with tooling in the loop Doesn’t ...

Topic (properties) SVA is not just syntax—good assertions encode intent precisely, resist vacuity, and scale with a proof plan. I write SVA with explicit assumptions, clear temporal structure, and reusable patterns. Principles: clarity · vacuity resistance · minimal assumptions Patterns: interface contracts · invariants · refinement lemmas What “good SVA” means in practice Signal discipline: assertions reference stable, meaningful signals (not accidental internals) Temporal intent: preconditions and consequences are separated clearly Assumptions are explicit: environment constraints are documented and reviewable Vacuity checks: proved properties should still be informative Common patterns I use Interface contracts: request/ack, ready/valid, FIFO rules Safety properties: “this bad thing never happens” Liveness under assumptions: “eventually” properties only where appropriate Helper lemmas: small provable stepping stones for complex end-to-end goals Where this shows up on my site Formal case studies (proof structure) Publications (property strategy and evaluation) Need help structuring assertions for a block? If you want to collaborate, discuss roles, or review artifacts, reach out. ...