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 formal verification auditing service 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 β Senior Smart Contract 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
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)
Ethan Menell β Summer 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.