- π 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.