vielite's blog

Blockchain security, vulnerability research, and AI-assisted formal verification.

Download PDF

Amos Dominion

Profile

Blockchain and systems security researcher specializing in adversarial analysis of smart contracts, distributed systems, and security tooling. Combines static analysis, coverage-guided fuzzing, reverse engineering, and exploit development to turn complex protocol failures into reproducible, high-impact findings. Current work explores AI-assisted formal verification, pairing LLM-guided specification synthesis with SMT-based invariant checking to scale security analysis.

Education

University of Delta

Bachelor's Degree in Cyber Security, CGPA: 4.43

Experience

Independent Security Researcher

2022 – Present

Immunefi, HackenProof, Remedy, and Code4rena

  • Discovered and responsibly reported 100+ valid vulnerabilities across major audit and bounty platforms, earning $10K+ through accepted findings and competitions.
  • Identified 10+ valid vulnerabilities in the $500K Monad Code4rena contest with keccack_crew, using agentic vulnerability-hunting workflows and coverage-guided fuzzing with cargo-fuzz to analyze the Rust codebase at scale.
  • Ranked top 3 in the Glider Security Contest by engineering offensive Python queries that surface live, high-severity EVM smart-contract candidates.

Penetration Tester & Security Analyst

University cybersecurity research team

  • Collaborated with professors and a leading university research team to design and deploy hands-on penetration-testing labs.
  • Performed authorized, real-world penetration tests against live systems and translated findings into practical remediation guidance.
  • Delivered applied lectures and trained security personnel, including police officers, in digital forensics and penetration testing methodology.

Reverse Engineering & Competitive Security

  • Reverse engineer x86/x86-64 binaries, Solana SBF bytecode, and EVM bytecode using GDB, Ghidra, and Binary Ninja; competed in 200+ CTFs with 50+ top-ten finishes.
  • Led teams to national and international finals, including CYSEC, SECCON, and Black Hat, under production-like time constraints.

Selected Projects & Open Source

z3ro-spec

Python · Z3

Developing an agentic CLI for automated EVM formal verification and on-chain vulnerability research, with an emphasis on AI-guided specification and invariant generation.

TheFaultyVendingMachine

Static Analysis

Building vulnerability-detection passes for Solana programs and EVM smart contracts.

4naly3er

TypeScript

Contributed vulnerability-detection passes to an open-source smart-contract analyzer used across 100+ protocol reviews.

Hound

Agentic Security Research

Extended the open-source security agent with a custom workflow for large-scale Rust vulnerability hunting during the Monad audit competition.

Damn Vulnerable DeFi — Foundry

Solidity · Foundry

Contributed Foundry-based material to an open-source smart-contract security challenge suite.

Achievements

Top 3, Glider Security Contest (2025) • Ranked #8 globally on CTFtime (2025)

1st at Backdoor CTF and L3ak CTF (2025) • 2nd at DaVinci Code CTF (2022) • 3rd at K!nd4susCTF (2025)

Finalist, Black Hat MEA (2023) • Finalist, CYSEC as university team captain (2022) • Finalist, SAS CTF (2025)

Skills

Languages: Solidity, Rust, Python, TypeScript, C, x86/x86-64 Assembly

Security & formal methods: Smart-contract and DLT auditing, AI-assisted formal verification, static analysis, fuzzing, reverse engineering, exploit development

Tools: Z3, Lean 4, Certora Prover/CVL, Foundry, Glider, Hound, Ghidra, GDB, Binary Ninja, Slither, cargo-fuzz, AFL++