Skip to content

Releases: lfglabs-dev/verity

0.1.0

16 Feb 07:55
@Th0rgal Th0rgal
v0.1.0
fed95f5
This commit was created on GitHub.com and signed with GitHub’s verified signature.
GPG key ID: B5690EEEBB952194
Verified
Learn about vigilant mode.

Choose a tag to compare

View all tags
0.1.0 Latest
Latest

Verity v0.1.0 - Initial Release

Verity is a Lean 4 formal verification framework for smart contracts that provides end-to-end correctness proofs from high-level specifications to compiled Yul/EVM bytecode.

Verification Status

  • 300 theorems across 9 categories (288 fully proven, 12 sorry placeholders in Ledger sum proofs)
  • 4 documented axioms (see AXIOMS.md)
  • Three-layer verification: EDSL → ContractSpec → IR → Yul

Compiler

  • 7 example contracts: Counter, SafeCounter, SimpleStorage, Owned, OwnedCounter, Ledger, SimpleToken
  • Yul code generation with callvalue() and calldatasize() guards
  • Linker support for external library integration (CryptoHash)

Testing

  • 349 Foundry tests across 25 test suites
  • Multi-seed differential testing (7 seeds: 0, 1, 42, 123, 999, 12345, 67890)
  • 8-shard parallel CI pipeline
  • Yul-vs-Solidity differential tests for all contracts

Getting Started

# Build and verify all proofs
lake build

# Run property tests
FOUNDRY_PROFILE=difftest forge test

See README.md for full documentation.

Assets 2
Loading