Hi, I'm Georgy Dunaev
Mathematician & Systems Software Engineer · Formal Verification · Distributed Systems
Eliminating system failure modes at the mathematical foundation. Specializing in Interactive Theorem Proving (Lean 4, Isabelle/ZF, Rocq/Coq), High-Assurance Functional Programming (Standard ML, OCaml, Rust, C++), and Distributed Reliability. Author of peer-reviewed Isabelle/ZF mechanizations in the Archive of Formal Proofs and architect of the Obelisk proof assistant.
Core Projects
Obelisk Proof Assistant ↗
An interactive proof assistant and programming language designed for Morse–Kelley & NBG class theory.
Features a dual-variant architecture: Variant 1 (1st-Order NBG/MK) with 105 foundational entries in foundations.ML (72 systematic catalog entries), and
Variant 2 (Higher-Order Propositions-as-Types) with 100/100 machine-checked theorems in verified_theorems.ML (77 derived, 16 definitional, 7 axiomatic) and 35/35 compiled .nbg programs.
Targets the verified CakeML compiler and Poly/ML down to machine code, and audited in Lean 4 (0 errors, 0 sorry).
Recursion Theorem in ZF (AFP) ↗
Formalized and machine-checked proof of the classical Recursion Theorem following Hrbacek and Jech, published in the Archive of Formal Proofs (Isabelle/ZF). Models Peano arithmetic in axiomatic set theory and verifies primitive recursive functions with absolute rigor.
Anti-Vibe Coding Manifesto ↗
A foundational philosophy against careless "vibe coding": advocating for machine-checked specifications, zero-trust correctness, formally verified kernels, and independent certification over uninspected generative hallucination.
Metamathematics & Type Theory Formalizations ↗
Mechanized proofs in Rocq (Coq) and Isabelle of classical first-order logic soundness/completeness, ZFC models inside the Calculus of Inductive Constructions, Gödel's incompleteness metatheory (diagonal lemma, Löb's theorem), and contextual categories towards categorical semantics of Homotopy Type Theory (HoTT).
Mathematical Research & Formal Foundations
Dunaev Tagged Pairs & Lists for Proper Classes
Resolves the classical limitation of Kuratowski pairing where proper classes cannot be paired without "phantom partners":
[A, B]D = mark(A, 0) ∪ mark(B, 1).
Unconditional left and right projections pr1 and pr2 are machine-checked in the Obelisk Standard ML kernel.
Recursion Theorem in ZF ↗
Published peer-reviewed mechanization of the transfinite recursion theorem following Hrbacek and Jech in the Archive of Formal Proofs. Establishes rigorous foundations for modeling Peano arithmetic and primitive recursion inside axiomatic set theory.
a ∈ A (Base value well-typed) · g ∈ A × nat → A (Step operator total function)
Categorical Semantics & The Yoneda Lemma
Monograph and formal developments exploring contextual categories, Yoneda embedding, and functorial semantics towards categorical models of Homotopy Type Theory (HoTT) using the UniMath library.
Gödel Incompleteness & Löb's Theorem
Mechanized proofs in Rocq (Coq) and Isabelle of classical first-order logic soundness/completeness, the Diagonal Lemma, Löb's theorem, and reflective internal provability predicates.
Formulas-as-Types vs. Proof-Term Compilation in MK/NBG ↗
In the Obelisk Higher-Order kernel, Morse–Kelley/NBG formulas serve as types (formula <Name> = ...) while proofs are explicit constructive λ/eliminator terms (theorem <Name> : <Formula> = <ProofTerm>). Bidirectional sort checking separates SetSort from ClassSort, barring proper classes such as the Russell class {x | x notin x} : ClassSort from set-quantified comprehension and preventing Russell's Paradox by typing.
Professional Experience
- Conducted weekly tutorial sessions, practical exercise classes, and homework grading for university mathematics courses.
- Taught complex logical arguments, proof techniques, and algebraic foundations to students in English and German.
- Engineered the Obelisk proof assistant from scratch in Standard ML, creating an independent LCF kernel and class theory axiomatics.
- Authored and published peer-reviewed formal proofs in the Archive of Formal Proofs (Isabelle/ZF).
- Acquired German working proficiency (B2 / B1 Zessko certificate, University of Potsdam).
- Developed backend infrastructure for a distributed system utilizing Linux virtualization technologies in asynchronous OCaml.
- Wrote unit and integration test harnesses for C++ and Python components; created automated CI/CD validation scenarios.
- Maintained strict concurrency safety, memory hygiene, and high system throughput.
- Designed and formally verified smart-contract specifications using automated code-generation and formal methods.
- Contributed to cryptographic backend protocols, consensus integration, and state-machine verification.
- Developed firmware and hardware test prototypes for STM32 microcontrollers in C and C++.
- Collected, processed, and analyzed biometric sensor data (iris and fingerprint imaging).
- Built real-time 3D visualization and simulation environments for virtual reality (Oculus Rift).
Technical Skills & Methodologies
🏛️ Proof Assistants & Logic
Deep theoretical foundation and practical mechanization in modern interactive theorem provers.
⚡ Functional & Systems Programming
High-assurance systems development with rigorous type safety and minimal memory overhead.
🤖 Multi-Agent AI & Distributed Systems
Architecting autonomous agent workflows, task pipelines, and isolated container execution.
🛡️ Verification & Security Engineering
Machine-checked state invariants, zero-leak secret detection, and automated audit gates.
Get in Touch
Let's discuss opportunities
I am actively open to engineering and research roles in formal verification, interactive theorem proving, high-assurance software, and functional systems development.