DEV Community

Cover image for How We Built Complete Formal Verification for Chronos Vault
Chronos Vault
Chronos Vault

Posted on

How We Built Complete Formal Verification for Chronos Vault

#blockchain #security #web3 #opensource

The Problem
Most blockchain projects rely on audits smart humans looking for bugs. But humans miss things. We needed mathematical guarantees that certain vulnerabilities are impossible, not just "haven't been found yet."

Our Solution: 3 Layer Verification
Chronos Vault now has one of the most comprehensive formal verification systems in DeFi, combining three tools that work together:

Layer 1: Abstract Mathematics (Lean 4)
35 theorems proven covering:

  • Withdrawal safety
  • Time-lock enforcement
  • Supply conservation across chains
  • Byzantine fault tolerance
  • Trinity Protocol 2-of-3 consensus

Layer 2: Code Analysis (Certora)
34 rules analyzing actual Solidity code:

  • ChronosVault.sol (9 rules, 5 invariants)
  • CVTBridgeV3.sol (11 rules, 2 invariants)
  • CrossChainBridgeV3.sol (14 rules, 2 invariants) Certora proves our deployed contracts implement the abstract theorems correctly.

Layer 3: Distributed Systems (TLA+)
5 consensus properties proven for Trinity Protocol:

  • 2-of-3 chain consensus requirement
  • Byzantine fault tolerance (secure even if 1 chain compromised)
  • Liveness under majority
  • No single point of failure

What Makes This Different
Integration: We don't just have proofs - we have a traceability matrix connecting:

  • Lean theorem → Certora rule → Actual Solidity code line Example: theorem timelock_enforcement (Lean) → ownerCannotBypassTimelock (Certora) → ChronosVault.sol:245-280 This means we can mathematically prove that specific lines of deployed code implement specific security properties. “Trust Math, Not Humans" Our tagline is now verifiable:
  • ✅ Time-locks provably cannot be bypassed (even by vault owner)
  • ✅ Cross-chain bridges provably conserve token supply
  • ✅ Trinity Protocol provably requires 2-of-3 chain consensus
  • ✅ All proofs are open source - verify yourself

Repository & Transparency
Everything is public:

Why This Matters
Traditional audit: "We looked for bugs and didn't find any"

Formal verification: "This type of bug is mathematically impossible"
Our verification proves:

  • Withdrawals before time-lock expiry: impossible
  • Double-spending on bridge: impossible
  • Bypassing 2-of-3 consensus: impossible
  • Reentrancy attacks: impossible Not "unlikely" - mathematically impossible. ## Automated Verification GitHub Actions runs all 3 layers on every commit:
  • Verifies 35 Lean theorems still hold
  • Runs Certora on all contracts
  • Model-checks TLA+ consensus properties
  • Validates theorem-to-code mappings If verification fails, the commit is blocked.

What's Next
We're expanding verification to:

  • Solana programs (Rust verification)
  • TON contracts (FunC verification)
  • Zero-knowledge circuits (Circom verification)

Developer Guide: Verifying Chronos Vault Smart Contracts

Want to verify our security claims yourself? Here's how.

Quick Start

Install Tools 

# Lean 4 (abstract proofs)
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

# Certora (Solidity verification)
pip install certora-cli

# TLA+ (consensus modeling)
wget https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
Enter fullscreen mode Exit fullscreen mode

Clone Repository


git clone https://github.com/Chronos-Vault/chronos-vault-contracts
cd chronos-vault-contracts
Enter fullscreen mode Exit fullscreen mode

Run Verification


# Layer 1: Verify abstract theorems
cd formal-proofs && lake build

# Layer 2: Verify Solidity contracts
certoraRun certora/conf/ChronosVault.conf
certoraRun certora/conf/CVTBridgeV3.conf  
certoraRun certora/conf/CrossChainBridgeV3.conf

# Layer 3: Verify Trinity Protocol consensus
java -jar tla2tools.jar tlaplus/specs/TrinityProtocol.tla
Enter fullscreen mode Exit fullscreen mode

Time: ~15-30 minutes for all layers

What Gets Verified
ChronosVault.sol
Proven properties:

  • Only owner can withdraw after time-lock expires

  • Time-locks cannot be bypassed (even by owner)

  • Balance never goes negative

  • No reentrancy attacks possible

  • Multi-signature thresholds enforced
    See: certora/specs/ChronosVault.spec

CVTBridgeV3.sol
Proven properties:

  • Total token supply conserved across chains

  • Each bridge nonce processed exactly once (no double-spend)

  • Bridge operations are atomic (all-or-nothing)

  • Circuit breaker triggers on anomalies
    See: certora/specs/CVTBridgeV3.spec

CrossChainBridgeV3.sol (Trinity Protocol)
Proven properties:

  • 2-of-3 chain consensus required for operations

  • Operations can be completed OR canceled, never both

  • Valid cryptographic proofs required

  • Timeout mechanisms work correctly

  • Byzantine fault tolerance (1 compromised chain doesn't break system)
    **See: **certora/specs/CrossChainBridgeV3.spec, tlaplus/specs/TrinityProtocol.tla

Reading Certora Reports
After running Certora, view your report:


https://prover.certora.com/output/%5Byour-job-id%5D
Enter fullscreen mode Exit fullscreen mode

  • ✅ Green = Property proven mathematically

  • ❌ Red = Counterexample found (potential bug)

  • ⚠️ Yellow = Timeout/inconclusive
    Example: Time-Lock Safety Proof
    Abstract Theorem (Lean 4)

Example: Time-Lock Safety Proof
Abstract Theorem (Lean 4)


theorem timelock_enforcement (vault : VaultState) :
    vault.locked = true → currentTime < vault.unlockTime → 
    ∀ (tx : Transaction), tx.amount = 0
Enter fullscreen mode Exit fullscreen mode

Code Verification (Certora)


rule ownerCannotBypassTimelock(uint256 amount) {
    env e;
    require e.msg.sender == owner();
    require e.block.timestamp < unlockTime();

    withdraw@withrevert(e, amount, owner(), owner());

    // This MUST revert - even for owner
    assert lastReverted;
}
Enter fullscreen mode Exit fullscreen mode

Actual Solidity (ChronosVault.sol)


function withdraw(uint256 assets, address receiver, address owner)
    public
    override
    nonReentrant
    onlyWhenUnlocked  // ← This modifier enforces time-lock
    returns (uint256)
{
    // ... withdrawal logic
}
Enter fullscreen mode Exit fullscreen mode

Proven: The onlyWhenUnlocked modifier makes pre-timelock withdrawals impossible.

Traceability Matrix
See how theorems map to code:


cat integration/mappings/theorem-to-code.json
Enter fullscreen mode Exit fullscreen mode

Example mapping:


{
  "theoremId": "3",
  "theoremName": "timelock_enforcement",
  "leanFile": "formal-proofs/Contracts/ChronosVault.lean",
  "certoraRule": "ownerCannotBypassTimelock",
  "solidityContract": "ChronosVault.sol",
  "solidityFunction": "withdraw",
  "solidityLines": [245, 280],
  "status": "PROVEN"
}
Enter fullscreen mode Exit fullscreen mode

Contributing
Want to add verification?

1.Write Lean theorem in formal-proofs/
2.Write Certora rule in certora/specs/
3.Add mapping to integration/mappings/theorem-to-code.json
4.Run all verifications
5.Submit PR with proof artifacts

See: https://github.com/Chronos-Vault/chronos-vault-contracts/blob/main/docs/verification/DEVELOPER_GUIDE.md

Questions?
GitHub Issues: Report bugs or ask questions
Email: chronosvault@chronosvault.org

Join us in building provably secure cross-chain infrastructure.

Contact:
Doc
GitHub
Discord
X

Top comments (0)