Search results

Proof: model IR internal helper composition for the generic Layer 2 theorem

Status: Open.

#1638 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Support ite (if/then/else) with storage writes in Layer 2 SupportedStmtFragment

enhancementNew feature or requestNew feature or request

Status: Open.

#1637 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Support event emission (emit/rawLog) in Layer 2 proofs

enhancementNew feature or requestNew feature or request

Status: Open.

#1636 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Support external calls with return values (staticcall/call) in EDSL

enhancementNew feature or requestNew feature or request

Status: Open.

#1635 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Support internal function composition in verity_contract macro

enhancementNew feature or requestNew feature or request

Status: Open.

#1634 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Layer 2 follow-on: replace SupportedSpec feature exclusions with compositional proof interfaces and widen coverage toward the full EDSL image

Status: Open.

#1630 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Contracts: add safeTransferFrom to ERC-721 implementation

enhancementNew feature or requestNew feature or request

P4: nice-to-haveLow priority improvementLow priority improvement

Status: Open.

#1629 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Language: add ETH balance tracking to ContractState

enhancementNew feature or requestNew feature or request

P2: importantBlocks specific contract categoriesBlocks specific contract categories

Status: Open.

#1628 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Proof: add delegatecall semantics to proof interpreter

enhancementNew feature or requestNew feature or request

P2: importantBlocks specific contract categoriesBlocks specific contract categories

Status: Open.

#1627 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Language: add create/create2 opcodes for factory contracts

enhancementNew feature or requestNew feature or request

P2: importantBlocks specific contract categoriesBlocks specific contract categories

Status: Open.

#1626 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Specs: cross-contract invariant proofs via postcondition hypotheses + assume-guarantee interfaces

enhancementNew feature or requestNew feature or request

P3: deferredBuilds on P0-P2 workBuilds on P0-P2 work

Status: Open.

#1625 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026

Math: create verity-math package with verified exp, ln, pow, WAD/RAY helpers

enhancementNew feature or requestNew feature or request

P3: deferredBuilds on P0-P2 workBuilds on P0-P2 work

Status: Open.

#1624 In lfglabs-dev/verity;

· Th0rgal opened on Mar 11, 2026