We combine formal verification and generative AI to make software provably secure. As AI gets better at finding vulnerabilities, mathematical proofs of correctness are becoming essential for critical systems.
What We Do
We provide a white-glove auditing and formal verification for Sui smart contracts. Our approach:
- Analyze customer codebases to create mathematical proofs of security
- Use AI to accelerate specification writing, proof construction, and adjusting specs as code changes
- Focus on real-world security properties that matter for production systems
Our work
Our Team
Andrei Stefanescu β Chief Scientist
- Led verification of AWS cryptographic algorithms using SAW at Galois
- Created first Ethereum smart contract verification tool
- Three-time International Math Olympiad silver medalist
- PhD in Computer Science from UIUC with David J. Kuck Outstanding Thesis Award
- ACM SIGPLAN Distinguished Paper Award at OOPSLA 2016
- Pioneered K Framework for programming language semantics and verification
Cosmin Radoi β CEO
- Created GritQL, a language for large-scale code migration (backed by Founders Fund, 8VC)
- PhD in Computer Science from UIUC focusing on programming languages
- Multiple ACM SIGSOFT Distinguished Paper Awards at top conferences (ICSE, OOPSLA, FSE)
- IBM PhD Fellowship recipient and NSF SBIR Award winner
- Key contributor to K Framework for language semantics and verification
- Research expertise in parallelism, race detection, and performance optimization
Mykhailo Burakhin β Principal Auditor
- Conducted detailed security audits and gas optimizations for complex DeFi applications
- Developed and audited ERC-20, ERC-721, and ERC-1155 token contracts, including staking, vesting, auctions, and launchpads
- Engineered cross-chain bridges using ERC-4337 account abstraction, multi-signature wallets, and upgradeable proxy contracts
- Implemented protections against anti-sniping and front-running, and secure onboarding with MPC and zero-knowledge proofs
- Over 15 years of experience architecting secure, high-performance systems with a strong focus on cryptography, blockchain security, and advanced C++ engineering
Rijnard van Tonder β Staff Engineer
- Built core Sui developer tools at Mysten Labs (package registry, source viewer); authored ICSE'24 demo on verifying/displaying Move source
- Creator of Comby, a structural code rewrite tool (2.5K GitHub stars)
- ICSE'23 Best Industry Paper and ICSE'18 ACM Distinguished Paper
- Advanced large-scale code search and refactoring at Sourcegraph; early LSP/LSIF work
- Enhanced Facebook's Pyre Python static type checker with parallel processing (5x speedup)
- PhD in Computer Science, CMU
Andrii Matskiv β Senior Blockchain Engineer
- Worked on Solana/EVM Express Audit system and various analytical tools for blockchain data insights
- Led development of Solana-based DEX with core smart contracts for token operations, presale, staking, and vesting (Rust-Anchor)
- Architected and built a DEX on Bitcoin L2 (Stacks) with cross-chain project funding mechanisms
- Designed token sale, vesting, and staking products, as well as blockchain token bridges for De.Fi
- Proficient in Rust, Solidity, TypeScript, and Python, and extensive engineering experience otherwise
Dmytro Sotnyk β Blockchain Engineer
- Developed cross-chain bridges between Ethereum and Kadena, and reconstructed Hyperlane protocol using Pact
- Conducted smart contract audits, developed audit methodologies, and researched vulnerabilities at Hacken
- Built backend solutions for Hedera Hashgraph and Solidity-based smart contracts with Web3 wallet integrations
- Proficient in Solidity, Pact, TypeScript, Python, and blockchain testing tools (Echidna, Slither)
Danylo Provilskyi β Blockchain Engineer
- Built solo an EVM protocol achieving $10M+ TVL with formal verification
- Shipped 6+ production Web3 projects from architecture to deployment, leading 15+ developers
- Selected for Uniswap Hook Incubator for DeFi protocol innovation
- Conducted security audits on EVM and Algorand using Echidna, Slither, Certora, and Foundry
- Won ETHWarsaw 2025 Spring Hackathon with cross-chain AI Agent on ViaLabs and OP Stack
Ethan Menell β Research Intern
- Built a programming language with a monomorphized polymorphic trait-based type system.
- Researched methods for detecting logical race conditions in asynchronous Rust code.
- Proficient in Rust, C++, TypeScript, React, and Python, and extensive programming experience.