- 🚀 Currently, I'm dedicating my efforts as a maintainer for the Strimzi project. Explore more at Strimzi.io.
- 📬 Reach out to me via my LinkedIn:
.
- 🌐 On a journey of discovery about formal verification methods, always eager to absorb new knowledge and explore rigorous system validations.
- ✍️ Visit my Blog: see-quick.github.io
| Date | Title | Link |
|---|---|---|
| 2025-03-01 | 12 🚀 Supercharge Your Dev Setup with Neovim, Starship, and WezTerm | Read more |
| 2024-12-24 | 11 My Advent of Code 2024 Journey | Read more |
- 💻 Actively contributing to various interesting open-source projects, always looking for new challenges and collaborations.
🛠️ Formal Verification
┌───────────────────────────────────────────────┐
│ ∀x, y ∈ S. (x ≠ y) → ¬(P(x) ∧ P(y)) │ (Uniqueness)
│ □(φ → ◇ψ) → ¬◇(¬ψ ∧ φ) │ (Temporal Logic)
│ ⊢ {P} Code_Block {Q} │ (Hoare Triple)
│ │
│ ✅ Liveness Example │
│ System ⊨ □(Button_Pressed → ◇Light_On) │ (If the button is pressed, the light will turn on)
│ │
│ 🛡️ Safety Property │
│ System ⊨ □(¬Bad_State) │ (System never reaches an invalid state)
│ │
│ 🔄 Mutual Exclusion │
│ System ⊨ ¬◇(Critical1 ∧ Critical2) │ (Two processes can’t be critical at once)
│ │
│ 📜 Proof: │
│ 1️⃣ Assume φ holds at time t │
│ 2️⃣ By transition rules, ◇ψ holds at t+1 │
│ 3️⃣ Therefore, □(φ → ◇ψ) is valid │
│ 4️⃣ Since □(¬Bad_State), no invalid state │
│ ✅ Q.E.D. │
└───────────────────────────────────────────────┘NOTE: Top Languages does not indicate my skill level or anything like that, it's a GitHub metric of which languages have the most code on GitHub. It's a new feature of github-readme-stats.