lfglabs-dev/verity
Formally verified smart contracts gives mathematical certainty across all inputs and execution paths. We bet that agents will make full formal verification practical.
First Claude commit: Feb 12, 2026Last Claude commit: 1mo agoDiscovered: Apr 23, 2026
Recent Claude Commits
release: prepare v1.0.0
74d8fe21mo agoauthor_emailfix: remove vestigial match on backendProfile in defaultRewriteBundleIdFor
9a25a392mo agoauthor_emailchore: update issue link to lfglabs-dev org
3e4f62c2mo agoauthor_emailchore: retrigger CI
c6c0dc52mo agoauthor_emailfix: update verify sync spec for parity-pack extraction
b814fa22mo agoauthor_emailExtract Morpho-specific parity rules from core compiler
f4daaef2mo agoauthor_emailci: sync parity-pack threshold across spec, source, and docs
d9c28fc2mo agoauthor_emailmerge: resolve conflicts with main
37f4c582mo agoauthor_emailfix: resolve SourceSemantics eq_def derivation failure for ceilDiv
40b51922mo agoauthor_emailfix: remove duplicate ceilDiv match arms and fix proof
6c243d62mo agoauthor_emailfix: resolve ceilDiv proof errors for Lean 4.22.0
fbfaf772mo agoauthor_emailfix: repair ceilDiv proof lemmas for Lean 4.22.0
45ac7032mo agoauthor_emailfeat: add ceilDiv stdlib primitive matching Solidity's Math256.ceilDiv
000d5df2mo agoauthor_emaildocs: update verification status to reflect Layer 2 proof WIP
1c9137a2mo agoauthor_emailfix: exclude sorry'd theorems from PrintAxioms to avoid sorryAx in axiom audit
d2b1e212mo agoauthor_emailfix: regenerate PrintAxioms, update verification artifacts, allowlist exposed proofs
dadb8042mo agoauthor_emailfix: sorry pre-existing proof failures exposed by from-scratch CI build
3715bf52mo agoauthor_emailfix: make state an explicit parameter in execStmt/execStmtList to fix termination proofs
8ca5b872mo agoauthor_emailfix(maint): add transferOwnership end-to-end tests for Owned and OwnedCounter
77360293mo agoauthor_emailfix(maint): propagate terminal halt through if_ branches in evalTStmtsFuel
877b3423mo agoauthor_emailfix(maint): merge storageAddr into flat storage in mkIRStateFromTyped
7da213b3mo agoauthor_emailfix(maint): add SafeCounter compilation and end-to-end tests
b1964b83mo agoauthor_emailfix(maint): add require-path end-to-end tests for withdraw and owned increment
913809b3mo agoauthor_emailfix(maint): use switch in if_ lowering to evaluate condition once
c358cac3mo agoauthor_emailfix(maint): add compilation smoke tests for Ledger, OwnedCounter, SimpleToken
39fd5ea3mo agoauthor_emailfix(maint): support address return values in typed IR compiler
a8562fe3mo agoauthor_emailfix(maint): add bool→uint256 coercion in typed IR compiler
75eba743mo agoauthor_emailfix(maint): add missing Expr.eq case to typed IR compiler
25986973mo agoauthor_emailfix(maint): halt typed IR evaluation after stop/returnUint
0feb19a3mo agoauthor_emailfix(maint): preserve branch-created locals in compileBranch
2d9fe863mo agoauthor_emailfix(maint): remove temporary debug files from stashed work restore
28b94ab3mo agoauthor_emailfix: correct sorry count in README and rename ContractSpec references in ROADMAP
34ea3d83mo agoauthor_emailfix: use correct Field struct syntax in rawLog tests
73aed193mo agoauthor_emailfeat: add Stmt.rawLog for low-level log0–log4 emission (#930)
2887a823mo agoauthor_emailfix: deduplicate hexDigit, remove dead code, fix stale docs (#376)
427a4803mo agoauthor_emailfix: expose compiler internals for structural induction proofs (#358)
6330c833mo agoauthor_emaildocs: Fix stale theorem count (252→296) and contract count (7→9)
89de5a93mo agoauthor_emailcleanup: Consolidate selector validation into main CI workflow
0d6961e4mo agoauthor_emailcleanup: Remove stale compiler/yul-new/ directory
b04b4324mo agoauthor_emailfix: CI path filters, scripts docs, index.mdx contract count
1f1afb44mo agoauthor_emailfix: Correct stale test counts (311→290, 30→23 suites)
b4fb6534mo agoauthor_emailfix: CI seed consistency, local test script, and stale docs
f771dbb4mo agoauthor_emaildocs: Add contracts table to README and CI doc-count validation
8d868c14mo agoauthor_emailfix(ir-interpreter): Fix 5 critical bugs reported by Bugbot
83b40904mo agoauthor_emailfeat(proofs): Complete EDSL-side proofs for Owned contract
ecebdf14mo agoauthor_email