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.