whoami

I’m Ilia, a software engineer with nearly four years of experience. Currently, I’m pushing the boundaries of verifiable computation at Nethermind, where I work on engineering and formally verifying cryptographic protocols. Yes, there are two “verifications” – ensuring the computation’s integrity and formally proving the protocol’s correctness – that I’m dealing with on day-to-day basis.

My interests lie in low-level systems, including cryptographic protocols, virtual machines, compilers/interpreters, instruction set architectures (ISAs), and their formal verification. I find immense satisfaction in understanding and manipulating program execution at the bytecode level – it almost feels like some kind of sorcery.

I’ve dedicated a significant portion of my life in the past to working on dependent type theory and its models in higher categories. So it’s pretty natural I believe in correct-by-construction, formally verified software (and hardware too!). While my approach is now more pragmatic, the principles remain. I’m most proficient in Rust and Haskell, but I’m language-agnostic and eager to work with any language if the project is compelling. Even COBOL could be an interesting challenge!

why 1xdev

We’ve all encountered those exceptionally productive individuals – the “10x developers” – whether they’re colleagues or random users from X/GitHub behind an anime profile pic. I believe that anyone can achieve that level of performance. On my blog, I’ll be documenting my personal journey from “1x” to “10x” developer. Join me and see what happens!