- π I am currently working on:
- redacted 4 protocol specification and verification with Quint
- π¨ playing with proving correctness of distributed algorithms in Lean
- π maintaining and improving Apalache β symbolic model checker for TLA+
- πΈ web3 security contests
- Recent past work:
-
redacted 3 consensus spec audit
-
redacted 2 Solidity protocol audit
- βredacted 1 for Matter Labs
- πͺ specification and model checking of ChonkyBFT for Matter Labs
- π© model checking of 3-slot finality for Ethereum
- π runtime verification of Soroban/Stellar smart contracts with Solarkraft
- π¬ 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 konnov.phd.
- π‘ You can ask me about Quint, TLA+, and protocol specification.
- π Pronouns: he/him/his.
Independent Research Scientist in Security and Formal Verification
-
konnov.phd
- Vienna, Austria
-
23:20
(UTC +02:00) - https://konnov.phd
- @k0nn0v
Highlights
- Pro
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/ssf-mc
freespek/ssf-mc PublicEF project Exploring Automatic Model-Checking of the Ethereum specification
TeX 7
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.