A* Audit is a smart contract security firm focused on decentralized finance. We review DeFi protocols end-to-end, with particular depth on the math underneath — AMM curves, lending invariants, stablecoin pegs, and derivative settlement.
We model smart contracts as finite state automata. Vulnerability detection is framed as directed pathfinding from deployment genesis to unreachable invariant violation states.
Moving beyond superficial checklists. We formulate protocol safety boundaries into formal mathematical assertions checked across all state transitions via SMT/Z3 solvers.
Targeted simulation of flash-loan balance manipulation, oracle price lag arbitrage, liquidation frontrunning, and cross-contract reentrancy interleaving.
The A* algorithm guarantees optimal path discovery via an admissible heuristic. We prioritize deep, high-complexity attack surfaces over trivial line checks.
In formal smart contract auditing, vulnerability detection is framed as a directed graph search over the contract's state-space. An exploit is an optimal path from genesis state $s$ to an invalid target state $t$.
Concentrated liquidity mathematics, bonding curves, dynamic fee algorithms, and multi-asset routing. We verify slippage bounds, invariant conservation, and sandwich/MEV resistance.
Collateral systems, liquidation mechanisms, interest rate jump models, and bad debt isolation. Proving inductive solvency invariants ($\forall s \in \mathcal{S}, \text{Solvent}(s)$) under extreme mempool congestion.
Stablecoin peg mechanisms, oracle dependencies, perpetual margin settlement, and multi-strategy yield vaults. Probing non-trivial economic invariants where rounding errors compound.
Approach. We write down what your system must guarantee, then ask what could break those guarantees and how. The audit is manual review at its core, with formal reasoning applied where the math admits it.
Two angles, many questions. For every contract, we work along two axes: correctness under normal conditions, and resistance under adversarial ones. Within each, we probe the specific edge cases your protocol exposes. There is no fixed checklist, because every protocol breaks differently.
AI-assisted, human-led. We use AI tooling to accelerate code traversal, surface candidate issues, and pressure-test hypotheses. Every finding is verified by a human auditor through manual review and critical reasoning. AI changes our speed, not our judgment.
Real-time delivery. Findings are posted as labeled GitHub issues directly in your private repository as the audit progresses — impact, likelihood, and status visible from day one. No black-box audit followed by a surprise document.
"Cost from start to n, plus estimated cost from n to goal. The optimal path is found not by luck — but by exhaustive, principled search."
Our auditors have stress-tested and secured multi-million dollar DeFi protocols across premier competitive platforms (Sherlock, Cantina, Code4rena) and private engagements. Every finding is backed by executable proofs of concept and verified mathematical invariants.
| Protocol | Domain / Architecture | Duration | Verification Platform | Public Dossier |
|---|---|---|---|---|
| Aave V4 Next-Gen Lending & Unified Liquidity Architecture | Lending Protocol | 28 Days | Sherlock | Contest Dossier ↗ |
| Fluid DEX V2 Smart Collateral & Dynamic Debt Routing | DEX & Lending | 28 Days | Sherlock | Contest Dossier ↗ |
| Revert Finance Uniswap v4 StableSwap Hooks & Yield Auto-Compounder | AMM Hooks | 9 Days | Cantina | Contest Dossier ↗ |
| Reserve Governor Decentralized Asset-Backed Currency Governance | Governance & Tokenomics | 12 Days | Cantina | Contest Dossier ↗ |
| Flying Tulips Omnichain Fungible Yield Vault & LayerZero OFT | Yield Vault & OFT | 12 Days | Sherlock | Contest Dossier ↗ |
| Monetrix Synthetic Assets & Peer-to-Pool Backing | Lending & Synthetics | 10 Days | Code4rena | Contest Dossier ↗ |
| K2 Layer 2 Modular Execution & Restaking Invariants | L2 Restaking | 40 Days | Code4rena | Contest Dossier ↗ |
| Covenant On-chain Concentrated Liquidity & Leverage Trading | AMM & Leverage | 12 Days | Code4rena | Contest Dossier ↗ |
| Intuition Decentralized Trust Graph & Attestation Verification | Attestation System | 5 Days | Code4rena | Contest Dossier ↗ |
| Clear Macro by Superfluid Continuous Money Streaming & Real-time Settlement | Streaming Payments | 3 Days | Sherlock | Contest Dossier ↗ |
| Alignerz Decentralized Launchpad & Mathematical Token Vesting | Launchpad & Vesting | 6 Days | Dualguard | Verification Log ↗ |
| Megapot Verifiable On-chain Entropy & Lottery Execution | Onchain Lottery | 10 Days | Code4rena | Contest Dossier ↗ |
Deep-dives into non-trivial smart contract vulnerabilities, cross-chain settlement race conditions, and inductive invariant proofs authored by our research team. Originally published on @Astaraudit on X ↗.
A repay transaction lands after a liquidator reassigns the position — and pays a stranger's loan due to stale health factor evaluation and mempool transaction reordering.
ZeroLend stripped Aave's aToken fallback from liquidation, so normal borrowing can drain the collateral reserve and permanently block liquidators from seizing anything.
Wildcat's batched withdrawal lets lenders settle before the batch is fully populated, so early executors take more than their share and the last lender's funds get permanently stuck.
Standard security checklists miss complex composability-induced reentrancy and oracle manipulation bugs. A mathematical manifesto for treating smart contracts as finite state automata with inductive invariant boundaries.
Inspect our reference audit methodology and executive dossier. See firsthand how our research lab breaks down complex protocol architecture, identifies high-severity vulnerabilities, and verifies inductive invariants on AMM curves, lending markets, and yield vaults.
Target: Multi-asset yield accumulator, flash-loan reentrancy guards, and mathematical share price solvency invariants.
Vulnerability Summary: A malicious actor can execute a 1-wei initial deposit followed by a direct donation of 10,000 WETH to skew the vault's internal exchange rate (totalAssets / totalSupply). Subsequent victim deposits suffer catastrophic rounding down to zero shares, allowing the attacker to withdraw victim funds entirely.
// Invariant: Always introduce virtual shares and virtual assets to eliminate inflation asymmetry
function _decimalsOffset() internal view virtual returns (uint8) {
return 3; // Virtual liquidity offset protects early depositors
}Formal definition of inductive invariants ($\forall s \in \mathcal{S}, \text{Solvent}(s)$) ensuring zero state reachability to exploit conditions.
Every vulnerability report includes an executable test case proving the exploit on local fork before mainnet exposure.
Ready-to-merge remediation pull requests with exact line diffs, minimizing developer friction and patch turnaround time.
Commit-hash anchored digital verification sign-off published publicly with senior cryptographic researcher signatures.
We work with DeFi protocols, lending markets, AMMs, staking systems, and novel mechanism designs. If it handles user funds on-chain, we want to read it.
Typical engagements run 2–4 weeks. We do not rush. Contact us with a brief protocol overview and commit hash — we respond within 24 hours.