- π I am currently working on:
- πͺ specification and model checking of ChonkyBFT for Matter Labs
- π maintaining and improving Apalache
- πΈ web3 security contests
- π runtime verification of Soroban/Stellar smart contracts with Solarkraft
- π© model checking of 3-slot finality for Ethereum
- π¬ specification and model checking of ZKsync governance
- π improving usability of specification languages with Quint
- π improving Apalache for finding bugs in smart contracts, dApps, and Cosmos protocols
- π¦ You can find how to reach me on my GH page.
- π‘ You can ask me about Quint, TLA+, and protocol specification.
- π Pronouns: he/him/his.
Independent Security and Formal Methods Research Scientist
-
Independent
- Vienna, Austria
-
03:29
(UTC +01:00) - https://konnov.phd
- @k0nn0v
Pinned Loading
-
apalache-mc/apalache
apalache-mc/apalache PublicAPALACHE: symbolic model checker for TLA+ and Quint
-
informalsystems/quint
informalsystems/quint PublicAn executable specification language with delightful tooling based on the temporal logic of actions (TLA)
-
freespek/solarkraft
freespek/solarkraft PublicSolarkraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache
-
informalsystems/atomkraft
informalsystems/atomkraft PublicAdvanced fuzzing via Model Based Testing for Cosmos blockchains
-
Something went wrong, please refresh the page to try again.
If the problem persists, check the GitHub status page or contact support.
If the problem persists, check the GitHub status page or contact support.