1270 index index.xml Dr. Derek Sorensen Derek Sorensen I am a mathematician and computer scientist. I work on Protocol Snarkification at the Ethereum Foundation, and these days I am mostly interested in Lean. Here you can see my research, notes, logs, work history, and bio. GitHub | ORCID | LinkedIn 337 dhsorens-001S dhsorens-001S.xml Featured Article 2025 10 9 Derek Sorensen true See my latest on building a formally verified LC3 virtual machine in Lean. 339 dhsorens-000D dhsorens-000D.xml Education 2025 6 15 Derek Sorensen true MSc in Mathematics and Foundations of Computer Science (MFoCS) at the University of Oxford. PhD in formal methods at the University of Cambridge under Anil Madhavapeddy. 341 dhsorens-pubs dhsorens-pubs.xml Peer-Reviewed Publications Derek Sorensen true Sorensen, D. Formally Specifying Contract Optimizations With Bisimulations in Coq. FMBC (ETAPS) (2025). [link] Sorensen, D. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. FMBC (ETAPS) (2024). [link] Sorensen, D. (In)Correct Smart Contract Specifications. ICBC (2024). [link] Jaffer, S., Dales, M., Ferris, P., Sorensen, D., Swinfield, T., Message, R., Keshav, S., and Madhavapeddy, A. Global, robust and comparable digital carbon assets. ICBC (2024). [link] Sorensen, D. Tokenized Carbon Credits. Ledger (2023). [link] Sorensen, D. Structured Pools for Tokenized Carbon Credits. ICBC CryptoEx (2023). [link] Butt, K., Sorensen, D. Streamlining Classical Consensus. International Journal of Blockchains and Cryptocurrencies, Vol. 1, No. 4 (2019). [link] Sorensen, D. Establishing Standards for Consensus on Blockchains. ICBC (2019). [link] A. Francis, D. Smith, D. Sorensen and B. Webb. Extensions and applications of equitable decompositions for graphs with symmetries. Linear Algebra and its Applications 532 (2017). [link] I also keep some preprints on record. 343 dhsorens-talks dhsorens-talks.xml Talks Derek Sorensen true Some selected talks: CompPoly: Computable Polynomials in Lean. ZKProofs 8, May 2026, Rome, Italy. Correct and Computable Specifications in Lean. SViL26, April 2026, Paris, France. Safely Snarkifying the Ethereum Protocol. EthCC[9], March 2026, Cannes, France. Formally Specifying Contract Optimizations With Bisimulations in Coq. FMBC 2025, May 2025, Hamilton, Canada. (In)Correct Smart Contract Specifications. ICBC, May 2024, Dublin. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. FMBC 2024, April 2024, Luxembourg. Abstraction, Specification, and Proof. Undone Science, February 2024, Nantes, FR. Structured Pools for Tokenized Carbon Credits. ICBC 2024, Dubai. Establishing Standards for Consensus on Blockchains. ICBC 2019, San Diego. K framework and type theory. RCon, May 2019, Berlin. I also keep some of my slides here. 345 dhsorens-000E dhsorens-000E.xml Work History 2025 6 15 Derek Sorensen true See my CV or a work bio. Related 1272 dhsorens-ef dhsorens-ef.xml Ethereum Foundation Institution 2025 12 18 Derek Sorensen true https://ethereum.foundation 1274 dhsorens-0020 dhsorens-0020.xml Protocol Snarkification 2025 12 18 Derek Sorensen true There are ongoing efforts to "snarkify" Ethereum, i.e. to integrate zero knowledge proofs into every layer of the Ethereum protocol. I contribute to this via formal verification in Lean. My main focus is currently on CompPoly and Arklib. See our website for more information. 1276 dhsorens-001C dhsorens-001C.xml Work Bio 2025 9 3 Derek Sorensen true For a summary of my work experience, see my CV (updated 11/2025). 585 dhsorens-0018 dhsorens-0018.xml Summary of Work and Projects 2025 9 3 Derek Sorensen true Since early 2018 I have held various roles in crypto, working mostly in research and formal verification. My original interests in crypto were in consensus algorithms and formal verification frameworks for verifying smart contracts. When I started, those frameworks and tools were in their infancy, K Framework being the only tool at the time to my knowledge that was production-ready for actual smart contracts. Over time, I became interested in the financial applications of smart contracts and I did my PhD in verification strategies for financial smart contracts. Along the way, I became deeply interested in type theory and proof assistants, and these days am interested broadly in theorem-proving, whether applied to software or formalized maths. In my day-to-day, I still do a lot of work in the design, construction, and formal verification of smart contracts. 376 dhsorens-0019 dhsorens-0019.xml Pre-PhD (2017-2019) 2025 9 3 Derek Sorensen I started working in crypto during the two years between my MSc and my PhD. My first job was at a small, Utah-based crypto startup called Pyrofex, which was mostly providing consulting services to the RChain co-op at the time. I was tasked with building the formal semantics for rholang, the smart contracting language on RChain, in K Framework in order to formally verify rholang contracts down the line. RChain, famously, encountered sudden and urgent financial problems because of a questionable set of decisions from the co-op's president, Greg Meredith, which necessitated a split between RChain and Pyrofex. We then pivoted to consensus-level research, designed our own layer-one blockchain and consensus protocol. Sadly, we ran out of money, and I had to look for a new job for the few months before my PhD started. I took a short internship with Digital Asset, working in Zurich and New York, and implementing an experimental currency on their blockchain-esque project Canton. 378 dhsorens-001A dhsorens-001A.xml During the PhD (2019-2023) 2025 9 3 Derek Sorensen During my PhD, I took several part-time jobs with various crypto startups. My work ranged from research and formal verification, to DeFi protocol modeling and design, to zero-knowledge proofs, to business development. Each of my jobs during the PhD informed my research and helped to broaden and sharpen my thinking. I took the last year of my PhD to focus fully on writing up and submitting. 380 dhsorens-001B dhsorens-001B.xml Post PhD (2024 - 2025) 2025 9 3 Derek Sorensen Since my PhD has ended, I went through a process of unifying my various interests in people, proofs, smart contracts, digital money, and zero-knowledge proofs. I took a job with Certora straight out of my PhD, doing a mix of formally verifying smart contracts and project managmenet/business development/product development/client support. Ultimately, it became clear that Certora was not the place that I was going to do my best work, so early 2025 we parted ways. I then took some temporary contract work over the summer of 2025 building, designing, and verifying DeFi protocols (my specific area of expertise) while I looked for something that I can truly sink my teeth into and that would define the next period of my career. 382 dhsorens-001E dhsorens-001E.xml Ethereum Foundation (2025 - Present) 2025 11 22 Derek Sorensen As of November 2025 I joined the Ethereum Foundation, working on Protocol Snarkification. This mostly consists of formally specifying and verifying ZK primitives in Lean. Last updated January 2026. For more updates, see my logs. 1278 dhsorens-lean dhsorens-lean.xml The Lean Theorem Prover Tool 2025 6 15 Derek Sorensen true http://lean-lang.org 1280 dhsorens dhsorens.xml Derek Sorensen Person 0000-0003-4937-6984 https://www.github.com/dhsorens Mathematician and computer scientist. PhD in computer science with Anil Madhavapeddy at the University of Cambridge, in formal methods applied to financial smart contracts. 610 dhsorens-0005 dhsorens-0005.xml Intellectual and Educational Bio 2025 6 14 Derek Sorensen true 612 dhsorens-000H dhsorens-000H.xml Undergraduate in Mathematics 2025 6 15 Derek Sorensen true I got into mathematics as an undergraduate by accident. My declared majors were first philosophy, then economics, and then mathematics. What really got me into mathematics was the notion of mathematical proof, as taught in the introduction to proofs course. Famous for "weeding people out," the course struck me at the core because I knew that in mathematics I could get to the bottom of any definition or proof, all the way down to axiomatic logic and logical systems. This sense of rigor and precision was precisely what I was craving intellectually at the time. I knew that it would be the best possible training, no matter what I was going to do with my life later. During my undergraduate I had one particularly influential professor, Greg Connor, who let me take topology courses early and who encouraged me to become a research mathematician. I'd known since my early 20's that I wanted to do a PhD, and by the end of my undergraduate mathematics was the clear option. Another professor, Ben Webb, took me on as a research assistant and we did some research in linear algebra and graph theory. It culminated in a paper and was my first taste of research, something I knew was deeply appealing to me. 614 dhsorens-000I dhsorens-000I.xml Year in Moscow 2025 6 15 Derek Sorensen true I spent my final year as an undergraduate in Moscow, studying mathematics at the Independent University of Moscow and the Higher School of Economics as part of the Math in Moscow program. During that time, I learned Russian by teaching kids at church, taking courses, and spending time with as many Russians as I could. The Russians are very intense mathematically. The courses met once a week for three hours each, with a five minute tea break in the middle. They called it the "Russian brainstorm." While my undergraduate education was of very high quality (no complaints really), this was at another level and I was forced to be much more independent mathematically. I had one professor in particular, Alexei Gorinov, who was educated in the French tradition and taught topology exceptionally well. He built off the interest in topology cultivated during my undergraduate. His problem sets in particular were exceptional, and I still keep the links for his Toplogy I and Topology II courses on hand. Gorinov's courses have left a lasting impact on me. If I were to become a professor at any point, I would endeavor to teach courses like he did. During this time, I also got into category theory by reading Awodey's Category Theory on my own. The courses, and my independent study, prepared me for my masters degree the following year, in which I continued to pursue algebraic topology. 616 dhsorens-msc dhsorens-msc.xml MSc in Algebraic Topology 2025 6 12 Derek Sorensen true I did my MSc during the 2016-2017 academic year at St Peter's College, Oxford. The course spanned through areas of pure mathematics and theoretical computer science. I focused mostly on algebraic topology, homotopy theory, homological algebra, and category theory. Chris Douglas and Andre Henriques were two standout professors to whom I am very grateful. My MSc dissertation was essentially commentary on one of Oscar Randal-Williams' papers on tautological rings on the connected sums of n-dimensional tauri. It deals with spectral sequences (in particular the Serre spectral sequence) and characteristic classes, among other things. The paper in question proved a result for odd-dimensional spheres, and my masters dissertation was an exploration on why the proof failed to generalize to the even-dimensional case. I have my dissertation here, but the dissertation included introductory appendices to various useful topics, which I have separated into their individual notes below. 579 dhsorens-000T dhsorens-000T.xml Some Notes in Algebraic Topology 2025 8 29 Derek Sorensen true An introduction to fiber bundles. An introduction to principal bundles. An introduction to characteristic classes. An introduction to systems of local (twisted) coefficients. Homotopy groups of spheres. Introduction to Algebraic K-theory. Introduction to the Serre Spectral Sequence. Classification of vector bundles over the projective line. Stability theorems for persistent homology. 618 dhsorens-phd dhsorens-phd.xml PhD in Formal Methods 2025 6 13 Derek Sorensen true 424 dhsorens-000C dhsorens-000C.xml Links and Referencing my PhD Thesis 2025 6 15 Derek Sorensen true Here is my PhD thesis and the associated GitHub repo. More information (including citation instructions) can be found using its DOI: 10.17863/CAM.118487. 426 dhsorens-0009 dhsorens-0009.xml The Background to my PhD Thesis 2025 6 15 Derek Sorensen true From October 2019 until December 2023, I was a PhD student at the University of Cambridge. I started my PhD trying to look at the Adam's Spectral Sequence in HoTT (ambitious, by what I'm given to understand), but life and covid lockdowns happened. I ended up pivoting into interactive theorem proving, thinking about financial smart contracts and their specifications. The main question that haunted me during my PhD was this: We can prove software correct with regards to a specification, but how does one know that a specification is correct? What could a notion of "correctness" even look like for software specifications? What followed was a prolonged meditation on the nature of the process of going from ideas and intuition into concrete implementation. My research was mostly an exploration on the formal tools used to write formal specifications. I was particularly fascinated by the use of interactive theorem provers (ITPs)—Rocq, Lean, Isabelle/HOL and the like—to specify smart contracts because of their extreme flexibility and versatility. You can state and prove anything in these, which can be thrilling but also provides a huge amount of flexibility. At the same time, the formalization of mathematics (in Lean) was beginning to catch my attention. The computer lab at the time had a weekly seminar on the formalization of mathematics, which I could attend when it didn't conflict with my commitments with Clare choir. While I knew I was not interested in actually doing the formalization myself, I was unquestionably drawn into the research of those that were—in particular, the observations they made about the intricacies of going from pen-and-paper proofs to formal proofs. Mathematicians were finding small, nuanced, and implicit assumptions made and expressed intuitively through notation and definitions that all mathematicians seemed to understand and get, but that had to be both discovered and made explicit during the process of formalization. I really started to learn the role of intuition that a mathematician undergoes when they codify a new mathematical concept into a formal definition—both in the realm of pen-and-paper mathematics as well as in the realm of formal proof. It was during this time that I started to experiment with formal definitions and structures that are common to mathematics, and highly useful for mathematical definitions, for the specification and verification of smart contracts. The structures and definitions I chose, mostly from very basic category theory, play a heavy role in modern theories of computation and programming languages but do not feature in specifications themselves (e.g. from a behavioral perspective). 428 dhsorens-000A dhsorens-000A.xml The Main Contributions of my PhD Thesis 2025 6 15 Derek Sorensen true My PhD thesis proposes two different ways of handling the problem of a specification's correctness. Both draw heavily on the theoretically robust nature of proof assistants. The first is through what I would informally call the "meta work," where the specification itself is treated like a mathematical object to study and prove correctness, like the software we're trying to prove correct. This uses prose and specification to articulate desired behaviors of a smart contract that are already easy to define, e.g. desirable economic or game-theoretic properties. The second is through the use of abstract tools that approximate the desired behavior. My first motivating example is that of a smart contract upgrade. When upgrading any software, intuitively we understand an updated version as incrementally different from a previous version—we're adding feature X, Y, and Z, fixing bugs, removing outdated functionality. All of this frames conversation and understanding of the new software in terms of the old. Why not then apply that to the formal specification? I introduced the notion of a contract morphism, or a formal structural relationship between two contracts that could be used in specification. The term "morphism" is category-theoretic, and is a general mathematical way of establishing a relationship between two objects. Once this formal relationship is established, proofs of one contract can be transported over that relationship to another contract. If the morphism is invertible, then the formal relationship establishes an equivalence of contracts, which could be useful e.g. for proving optimized code correct with regards to a reference implementation. The morphism allows one to use a contract as a specification, something which can be far more intuitive than using prose. All of this is encapsulated fairly well in the slides of this talk. 430 dhsorens-0008 dhsorens-0008.xml The Papers of My PhD Thesis 2025 6 15 Derek Sorensen true Sorensen, D. Formally Specifying Contract Optimizations With Bisimulations in Coq. FMBC (ETAPS) (2025). [link] Sorensen, D. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. FMBC (ETAPS) (2024). [link] Sorensen, D. (In)Correct Smart Contract Specifications. ICBC (2024). [link] Sorensen, D. Tokenized Carbon Credits. Ledger (2023). [link] Sorensen, D. Structured Pools for Tokenized Carbon Credits. ICBC CryptoEx (2023). [link] 620 dhsorens-001C dhsorens-001C.xml Work Bio 2025 9 3 Derek Sorensen true For a summary of my work experience, see my CV (updated 11/2025). 585 dhsorens-0018 dhsorens-0018.xml Summary of Work and Projects 2025 9 3 Derek Sorensen true Since early 2018 I have held various roles in crypto, working mostly in research and formal verification. My original interests in crypto were in consensus algorithms and formal verification frameworks for verifying smart contracts. When I started, those frameworks and tools were in their infancy, K Framework being the only tool at the time to my knowledge that was production-ready for actual smart contracts. Over time, I became interested in the financial applications of smart contracts and I did my PhD in verification strategies for financial smart contracts. Along the way, I became deeply interested in type theory and proof assistants, and these days am interested broadly in theorem-proving, whether applied to software or formalized maths. In my day-to-day, I still do a lot of work in the design, construction, and formal verification of smart contracts. 376 dhsorens-0019 dhsorens-0019.xml Pre-PhD (2017-2019) 2025 9 3 Derek Sorensen I started working in crypto during the two years between my MSc and my PhD. My first job was at a small, Utah-based crypto startup called Pyrofex, which was mostly providing consulting services to the RChain co-op at the time. I was tasked with building the formal semantics for rholang, the smart contracting language on RChain, in K Framework in order to formally verify rholang contracts down the line. RChain, famously, encountered sudden and urgent financial problems because of a questionable set of decisions from the co-op's president, Greg Meredith, which necessitated a split between RChain and Pyrofex. We then pivoted to consensus-level research, designed our own layer-one blockchain and consensus protocol. Sadly, we ran out of money, and I had to look for a new job for the few months before my PhD started. I took a short internship with Digital Asset, working in Zurich and New York, and implementing an experimental currency on their blockchain-esque project Canton. 378 dhsorens-001A dhsorens-001A.xml During the PhD (2019-2023) 2025 9 3 Derek Sorensen During my PhD, I took several part-time jobs with various crypto startups. My work ranged from research and formal verification, to DeFi protocol modeling and design, to zero-knowledge proofs, to business development. Each of my jobs during the PhD informed my research and helped to broaden and sharpen my thinking. I took the last year of my PhD to focus fully on writing up and submitting. 380 dhsorens-001B dhsorens-001B.xml Post PhD (2024 - 2025) 2025 9 3 Derek Sorensen Since my PhD has ended, I went through a process of unifying my various interests in people, proofs, smart contracts, digital money, and zero-knowledge proofs. I took a job with Certora straight out of my PhD, doing a mix of formally verifying smart contracts and project managmenet/business development/product development/client support. Ultimately, it became clear that Certora was not the place that I was going to do my best work, so early 2025 we parted ways. I then took some temporary contract work over the summer of 2025 building, designing, and verifying DeFi protocols (my specific area of expertise) while I looked for something that I can truly sink my teeth into and that would define the next period of my career. 382 dhsorens-001E dhsorens-001E.xml Ethereum Foundation (2025 - Present) 2025 11 22 Derek Sorensen As of November 2025 I joined the Ethereum Foundation, working on Protocol Snarkification. This mostly consists of formally specifying and verifying ZK primitives in Lean. Last updated January 2026. For more updates, see my logs. 1281 dhsorens-logs dhsorens-logs.xml Logs Derek Sorensen true 251 dhsorens-002B dhsorens-002B.xml Q2 2026 Log 2026 5 10 Derek Sorensen We have spent the last few months travelling. I'm writing this in May 2026 from Rome. The most recent two trips were Cannes (for EthCC) and Paris (for SViL26). SViL26 was one of the most productive trips yet, only rivaled by HACS. We are now at a point where we can feasibly extract Plonky3 from Rust into Lean and formally prove things! In my talk today at zkproofs8, I showed a minimal example of formally verifying Koalabear in Plonky3, in Lean. We're making fast progress on CompPoly, Arklib, and now with the tooling where it's at it looks like it's time to start to marry them and actually formally verifying real code in Lean! Once I'm back from Rome, I will basically be full-time on this problem. This is good for me because I have so far avoided learning too much about cryptography, and now that I'll be staring at the implementations in Rust as well as the formal specs, it will be hard to avoid actually understanding things. I'm hoping that this process will stimulate Arklib into grater maturity, starting with CompPoly; I'm also hoping that the tooling will get a lot better (with my help) through this project. This will be the main thing this summer, hoping that by the end of the summer we have serious formal proofs of Plonky3! 253 dhsorens-0026 dhsorens-0026.xml Q1 2026 Log 2026 3 24 This has been a productive quarter. In early January we gave grants to Runtime Verification to test Hax for extracting code into Lean. They were successful in improving the tool, landing pull requests, and developing some good examples of (toy versions of) Rust programs of interest. Collaborating with them on this helped us see shortcomings in the Arklib specs and get a more realistic idea of what Rust verification could look like for us. Happily, our CompPoly specs did come in useful and they were able to verify some small Rust snippets against them. We settled on a roadmap for CompPoly in January, and while I and collaborators took CompPoly Phase 1 to the finish line, we put out a call for grants for Phase 2 of CompPoly. We got a lot of grant applications, and have just sent emails awarding grants for *all* of Phase 2. That should be done by the summer. We attended HACS and RWC26 in Taipei in early March, which was extremely productive. I learned a lot about Hax and Aeneas, verified compilers, and cryptography in general. Got strong insights for the upcoming work, and had a chance to evangelize our work on CompPoly. Bolton Bailey and I had a great conversation about the (many many) applications of computable polynomials in Lean. I hope that we can upstream CompPoly to CSLib and have many people using and maintaining it. Accomplishments: CompPoly roadmap established and merged in this pull request Contributed a lot to CompPoly, established style guides and standards for contribution, integrated into CI, and built out a lot more theory with the help of collaborators, old and new. CompPoly Phase 1 of the Roadmap completed - see the Zulip announcement We have some basic examples of extraction from Rust to Lean (thank you RV) that we can hopefully build on. Events: Giving two talks at EthCC[9], one (maybe two?) with Alex Hicks and one on my own. Invited to give a talk at SViL26 with Leo de Moura, Son Ho, and Karthikeyan Bhargavan in April. Next: I am responsible to see CompPoly make it through Phase 2 by the summer, though I will likely not be doing as much coding on it. Instead, I'll take a coordinating role and make sure the codebase fits together well and that the incoming code is high quality. We will likely have 8-10 contributors for Phase 2, which is exciting! This will be serious progress. We continue to integrate AI into our pipelines, successfully. I am currently looking for another chunk of technical work to do while I manage the CompPoly stuff, possibly contributing to evm-asm. 254 dhsorens-0021 dhsorens-0021.xml November/December 2025 Log 2025 12 18 I joined the EF in November 2025 with a week at Devconnect. My first projects will focus on stress-testing formal verification tools, including Hax and Arklib to start. 1283 dhsorens-notes dhsorens-notes.xml Notes Derek Sorensen true I am interested, broadly speaking, in formal proposition and proof. From a high level, what tends to catch my attention is the nuance of going from an intuitive, abstract idea into something formal—whether it's a formal specification of a program, a formalized theorem statement, or even something simply written out as a program. During my PhD this manifested as written work focused on the problem of (correctly) specifying and formally verifying financial smart contracts. But I continue to be interested in software verification more broadly, the ongoing work to formalize mathematics, and other developments in using proof assistants in production. I recently started work on formally verifying all things zero-knowledge on the Ethereum protocol, so my interests are broadening but are still rooted in the same topics. 279 dhsorens-0027 dhsorens-0027.xml LC3 in Lean Blog 2026 3 27 Derek Sorensen I recently implemented a formally verified virtual machine in Lean on which you can run 2048 in terminal! Try it out! ISA-level model The LC-3 is a small 16-bit instructional architecture: eight general-purpose registers, a program counter, condition flags, and a -word address space. At each step the machine fetches a word from memory at the PC, decodes it as one of fourteen opcodes (from arithmetic and bitwise operations to loads, stores, branches, jumps, and subroutine calls), then updates registers, memory, and control flow accordingly. Beyond those opcodes, LC-3 programs rely on trap routines for console I/O and on memory-mapped I/O for the keyboard—so a faithful simulator must implement both the core instructions and this I/O story. For more on the architecture, see here. The code in LC3-Lean is laid out as follows: register and flag state lives in LC3Lean/Registers.lean, the flat memory model in LC3Lean/Memory.lean, opcode decoding in LC3Lean/Instructions.lean, the fetch–decode–execute step and per-opcode semantics in LC3Lean/Execution.lean, The runnable binary wires together loading of .obj files, the execution loop, and MMIO in Main.lean. If you open those modules, every informal claim in this paragraph—word size, register count, opcode coverage, traps, MMIO—is meant to be visible as definitions and executable code rather than hand-waving. The runnable binary wires together loading of .obj files, the execution loop, and MMIO in Main.lean. For full details, see this page. Formal proofs "Formally verified" here means that Lean checks mathematical theorems relating the implementation above to an explicit ISA-level specification of how each instruction may read and write registers and memory. Those theorems are stated and proved in the LC3Correct package—especially LC3Correct/ExecutionCorrect.lean, with supporting lemmas about registers and memory in LC3Correct/RegisterLemmas.lean and LC3Correct/MemoryLemmas.lean. Together they aim to capture, opcode by opcode, that the Lean executor’s effect on machine state matches the spec encoded alongside it. All proofs pass without sorry! Trust Base and Verification Boundary The boundary worth keeping in mind is the thin C shim (c/terminal.c) used for POSIX terminal raw mode and polling: it affects how characters reach your screen and keyboard, but the LC-3 machine semantics and the correctness proofs live on the Lean side. Readers who want the precise logical statement for a single opcode should start from LC3Correct/ExecutionCorrect.lean and follow the definitions it references—the prose here is only a map to those lemmas. For full details, see this page. 281 dhsorens-0025 dhsorens-0025.xml CompPoly and Computable Specifications 2026 3 11 Derek Sorensen During Q1 of 2026 we worked building out CompPoly, a formally verified model of computable polynomials in Lean. The purpose of CompPoly is to provide a computable base for the specs in Arklib. My thoughts on computable specifications are still developing. They are growing out of an interest during my PhD in the integrity of formal specifications in the case of smart contracts. zkVMs and SNARKS also have complicated specifications, but for a different reason than smart contracts. Whereas smart contract specifications have difficult-to-define, high-level, socio-economic properties that one must aim at with a spec, the specs of zkVMs are complex because they correspond to some pretty intense mathematics. Just stating the desired properties requires quite a bit of machinery -- see Arklib for a taste of that. So, we can write complex mathematical specifications in Lean - great, what does computability add to this, or any specification? For one, it lets you run tests. Having tests lets you test the integrity of your spec and test it in sort of a meta- way. It helps build confidence that the spec was built out correctly, something that is difficult (impossible?) to really know. I have written before about metaspecifications, or formal specifications of specifications, in the context of smart contracts. I really believe that metaspecifications can add a lot to the security of smart contracts, but a lot of theory has to be built up (even just developed from a cryptoeconomic point of view) before this becomes a reasonable strategy for contracts in the wild. However, metaspecifications already show up in cryptography! An implementation has a specification, the design of the cryptographic system or protocol (e.g. FRI). The system or protocol is defined in mathematical terms, with assumptions, and with associated proofs of security. Security proofs (reduction proofs) show that if the cryptographic protocol fails, then some assumption of the system was violated. This is a metaspecification! But, as with all specifications, it is very hard to be sure that your specification is correct. This is where computability comes in. Having an executable/computable specification means that you can run tests on it, further extending your specification in an informal way. It makes your spec act more like software, and in some sense makes it stronger as a specification because as a program that runs it is closer to the thing that you're verifying. Lean is of course a great place for this. It is easy to go between computable and non-computable terms, spec and implementation, and more and more of the infrastructure of verification is becoming available in Lean. 283 dhsorens-0020 dhsorens-0020.xml Protocol Snarkification 2025 12 18 Derek Sorensen true There are ongoing efforts to "snarkify" Ethereum, i.e. to integrate zero knowledge proofs into every layer of the Ethereum protocol. I contribute to this via formal verification in Lean. My main focus is currently on CompPoly and Arklib. See our website for more information. 285 dhsorens-000U dhsorens-000U.xml Formal Specification and Verification 2025 8 29 Derek Sorensen true Most of my formal research work is in formal specification and verification, especially in proof assistants like Lean, Rocq, and the like. During my PhD and in the years after a lot of time thinking about smart contract design, specification, and verification. 287 dhsorens-000W dhsorens-000W.xml Smart Contract Design, Specification, and Verification 2025 8 29 Derek Sorensen Smart contracts are interesting from the perspective of formal specification and verification because: they are risk- and property-dense, they are typically small in size, with a deterministic and well-defined execution environment, making them feasible to formally reason about in a short time frame, and they often manage huge sums of money (so the incentives line up). Furthermore, because smart contracts act as social and financial intermediaries, they often have extremely interesting (and nontrivia) specifications, which warrants a study not only of the science of going from specification to verification (formal proof), but of the specifications themselves as independent, mathematical objects. 289 dhsorens-0015 dhsorens-0015.xml Formal Verification in Proof Assistants 2025 9 2 Derek Sorensen true Speaking more broadly, formal verification in proof assistants is interesting because in the robustly mathematical setting provided by proof assistants, one can state and prove arbitrary properties. This may be a blessing and a curse. Much like with programming languages, being able to state and do arbitrary things is not always an advantage. Due to the extreme flexibility, formal counterparts of informal specifications can vary widely without an obvious way to compare them or evaluate them for correctness or practical utility (for more on this see the introduction to my PhD thesis). In my PhD and my subsequent writing (e.g. this paper or my research statement), I have argued that the robustly mathematical setting of proof assistants offers us an opportunity for unmatched rigor, but we must draw on mathematical practice and tradition and use them in a more sophisticated way than we are using them now. There is much to be learned from the ongoing work in the formalization of mathematics and formal specification and verification in proof assistants more broadly, from theoretical and practical perspectives. 291 dhsorens-000V dhsorens-000V.xml Type Theory and Formal Proof 2025 8 29 Derek Sorensen true I am also interested more broadly in type theory and formal proof, especially as they relate to proof assistants. This has included some preliminary work in HoTT on the formal side, but ongoing work in the formalization of mathematics in Lean is deeply interesting to me as a peripheral development to my work. 1285 dhsorens-rsrch dhsorens-rsrch.xml Research Derek Sorensen true 700 dhsorens-000S dhsorens-000S.xml Research Statement 2025 8 13 Formal proposition and proof, especially in Lean and Rocq, catch my attention from various angles. This is my most recent research statement as a PDF. (Last updated 09/2025.) 701 dhsorens-pubs dhsorens-pubs.xml Peer-Reviewed Publications Derek Sorensen true Sorensen, D. Formally Specifying Contract Optimizations With Bisimulations in Coq. FMBC (ETAPS) (2025). [link] Sorensen, D. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. FMBC (ETAPS) (2024). [link] Sorensen, D. (In)Correct Smart Contract Specifications. ICBC (2024). [link] Jaffer, S., Dales, M., Ferris, P., Sorensen, D., Swinfield, T., Message, R., Keshav, S., and Madhavapeddy, A. Global, robust and comparable digital carbon assets. ICBC (2024). [link] Sorensen, D. Tokenized Carbon Credits. Ledger (2023). [link] Sorensen, D. Structured Pools for Tokenized Carbon Credits. ICBC CryptoEx (2023). [link] Butt, K., Sorensen, D. Streamlining Classical Consensus. International Journal of Blockchains and Cryptocurrencies, Vol. 1, No. 4 (2019). [link] Sorensen, D. Establishing Standards for Consensus on Blockchains. ICBC (2019). [link] A. Francis, D. Smith, D. Sorensen and B. Webb. Extensions and applications of equitable decompositions for graphs with symmetries. Linear Algebra and its Applications 532 (2017). [link] I also keep some preprints on record. 703 dhsorens-talks dhsorens-talks.xml Talks Derek Sorensen true Some selected talks: CompPoly: Computable Polynomials in Lean. ZKProofs 8, May 2026, Rome, Italy. Correct and Computable Specifications in Lean. SViL26, April 2026, Paris, France. Safely Snarkifying the Ethereum Protocol. EthCC[9], March 2026, Cannes, France. Formally Specifying Contract Optimizations With Bisimulations in Coq. FMBC 2025, May 2025, Hamilton, Canada. (In)Correct Smart Contract Specifications. ICBC, May 2024, Dublin. Towards Formally Specifying and Verifying Smart Contract Upgrades in Coq. FMBC 2024, April 2024, Luxembourg. Abstraction, Specification, and Proof. Undone Science, February 2024, Nantes, FR. Structured Pools for Tokenized Carbon Credits. ICBC 2024, Dubai. Establishing Standards for Consensus on Blockchains. ICBC 2019, San Diego. K framework and type theory. RCon, May 2019, Berlin. I also keep some of my slides here.