Leadership
Andrey Lyashin
Government Blockchain Association (GBA) - Member Active participant in blockchain governance and standardization initiatives.
Blockchain technology expert and formal verification specialist with over 13 years of active participation in the cryptocurrency community. Founder of Pruvendo, a world-leading company in formal verification of smart contracts, and creator of Ursus - an innovative domain-specific language for mathematically proven smart contract development. Background in theoretical physics with extensive experience in developing rigorous methodologies for ensuring smart contract security through mathematical proofs.
Current Position
Co-Founder & CTO, Hero2Quest (2023 - Present)
• Co-Founder and Chief Technology Officer • Designed system architecture and smart contract infrastructure • Led the development team for Soroban smart contracts • Implemented comprehensive testing methodology based on formal verification principles
Technical Implementation:
• Smart contracts developed in Rust for Stellar Soroban platform • Extensive test coverage applying formal verification-inspired approaches • Secure and auditable contract architecture
Co-Founder & CTO, Pruvendo (2018 - Present)
World’s Leading Formal Verification Experts
• Founded and lead a company specializing in mathematically proven security for smart contracts • Developed Ursus - a pioneering embedded Domain-Specific Language (eDSL) in Coq proof assistant for smart contract verification • Delivered formal verification for major blockchain projects for multiple enterprise-grade DeFi protocols • Established a staged deductive verification flow from plain-language specifications to Coq-checked proofs • Created methodologies for translating Solidity/Rust into verifiable intermediate representations
Key Achievement: Zero critical, high, or major security issues in verified contracts deployed to mainnet.
Ursus - Smart Contract Verification Language
Creator and Lead Developer
Ursus is a domain-specific language embedded in the Coq/Rocq proof assistant, designed for writing and verifying smart contracts with mathematical certainty.
Core Features:
• Coq Integration - Deep embedding in an industrial-strength theorem prover • Familiar Syntax - Bridges Solidity/Rust style with formal verification capabilities • Multi-Language Support - Target platforms include Solidity, Rust, and FunC • Type Safety & Panic Tracking - Comprehensive static analysis guarantees
Impact: Enables development of smart contracts that are mathematically proven to behave exactly as specified.
Key Publications:
• “PoS Forging Algorithms: Formal Approach and Multibranch Forging” (2014) • “PoS Forging Algorithms: Multi-strategy Forging and Related Security Issues” (2014) • “Multibranch Forging Algorithms: Tails-switching Effect and Chain Measures” (2014)
Research & Open Source
Founder, ConsensusResearch (2014 - 2016)
Research project dedicated to formal analysis of consensus algorithms in blockchain systems.
Key Publications:
• “PoS Forging Algorithms: Formal Approach and Multibranch Forging” (2014) • “PoS Forging Algorithms: Multi-strategy Forging and Related Security Issues” (2014) • “Multibranch Forging Algorithms: Tails-switching Effect and Chain Measures” (2014)
Contributions:
• Formal mathematical models for Proof-of-Stake consensus mechanisms • Analysis of forging algorithm security and fairness properties • Research cited in academic blockchain literature (Qeditas, Input Output HK)
Note: In recent years, open source activity has decreased due to work on proprietary code. Smart contracts developed for Hero2Quest will be open sourced based on company decisions.
Education
Freie Universität Berlin - PhD Studies (Theoretical Physics)
• Advanced research in theoretical and mathematical physics and mathematical modeling
Earlier Career
Robotics Research (2000 - 2005)
• Collaborated with leading academic institutions including Fraunhofer Institute (Bonn/Cologne) • Applied mathematical and computational methods to robotics autonomous systems
Technical Expertise: Technologies & Skills
Formal Verification: Coq, Theorem Proving, Specification Languages
Smart Contract: Solidity, Rust
Development
Blockchain Platforms: Ethereum, Stellar/Soroban, EVM/TVM-compatible chains
Research Methods: Formal Methods, Mathematical Modeling, Consensus Analysis
Languages: Ursus (creator), DSL development
Andrew Akulich
Game systems and algorithms architect combining product ownership with hands-on engineering execution. 20+ years of experience in software and game development (since 2002).
Key Focus
Game logic & systems design — progression, economy, meta-game, engagement mechanics
Runtime algorithms & architecture — deterministic simulation, matchmaking, FSM/state machines, scaling patterns
Product execution — from concept and specifications to implementation, iteration, and continuous improvement
Practical application and configuration of Stable Diffusion, and orchestration of LoRA models for creating graphic content for games: from rapid prototyping of visual styles and characters to building reproducible asset-generation pipelines that accelerate production and expand content variability.
Designed to enable rapid launch of P2P casual games using modular, reusable components.
Two higher education degrees: the first is technical — an engineer in automated systems, with a fundamental background in systems analysis, modeling, architecture, and the development of complex hardware-software solutions; the second is art-and-technology oriented — computer design and graphics.
Last updated