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: 8d agoDiscovered: Apr 23, 2026
Recent Claude Commits
release: prepare v1.0.0
74d8fe28d agoauthor_emailfix: remove vestigial match on backendProfile in defaultRewriteBundleIdFor
9a25a3923d agoauthor_emailchore: update issue link to lfglabs-dev org
3e4f62c23d agoauthor_emailchore: retrigger CI
c6c0dc523d agoauthor_emailfix: update verify sync spec for parity-pack extraction
b814fa223d agoauthor_emailExtract Morpho-specific parity rules from core compiler
f4daaef23d agoauthor_emailci: sync parity-pack threshold across spec, source, and docs
d9c28fc1mo agoauthor_emailmerge: resolve conflicts with main
37f4c581mo agoauthor_emailfix: resolve SourceSemantics eq_def derivation failure for ceilDiv
40b51921mo agoauthor_emailfix: remove duplicate ceilDiv match arms and fix proof
6c243d61mo agoauthor_emailfix: resolve ceilDiv proof errors for Lean 4.22.0
fbfaf771mo agoauthor_emailfix: repair ceilDiv proof lemmas for Lean 4.22.0
45ac7031mo agoauthor_emailfeat: add ceilDiv stdlib primitive matching Solidity's Math256.ceilDiv
000d5df1mo agoauthor_emaildocs: update verification status to reflect Layer 2 proof WIP
1c9137a1mo agoauthor_emailfix: exclude sorry'd theorems from PrintAxioms to avoid sorryAx in axiom audit
d2b1e211mo agoauthor_emailfix: regenerate PrintAxioms, update verification artifacts, allowlist exposed proofs
dadb8041mo agoauthor_emailfix: sorry pre-existing proof failures exposed by from-scratch CI build
3715bf51mo agoauthor_emailfix: make state an explicit parameter in execStmt/execStmtList to fix termination proofs
8ca5b871mo agoauthor_emailfix(maint): add transferOwnership end-to-end tests for Owned and OwnedCounter
77360291mo agoauthor_emailfix(maint): propagate terminal halt through if_ branches in evalTStmtsFuel
877b3421mo agoauthor_emailfix(maint): merge storageAddr into flat storage in mkIRStateFromTyped
7da213b1mo agoauthor_emailfix(maint): add SafeCounter compilation and end-to-end tests
b1964b81mo agoauthor_emailfix(maint): add require-path end-to-end tests for withdraw and owned increment
913809b1mo agoauthor_emailfix(maint): use switch in if_ lowering to evaluate condition once
c358cac1mo agoauthor_emailfix(maint): add compilation smoke tests for Ledger, OwnedCounter, SimpleToken
39fd5ea1mo agoauthor_emailfix(maint): support address return values in typed IR compiler
a8562fe1mo agoauthor_emailfix(maint): add bool→uint256 coercion in typed IR compiler
75eba741mo agoauthor_emailfix(maint): add missing Expr.eq case to typed IR compiler
25986971mo agoauthor_emailfix(maint): halt typed IR evaluation after stop/returnUint
0feb19a1mo agoauthor_emailfix(maint): preserve branch-created locals in compileBranch
2d9fe861mo agoauthor_emailfix(maint): remove temporary debug files from stashed work restore
28b94ab1mo agoauthor_emailfix: correct sorry count in README and rename ContractSpec references in ROADMAP
34ea3d82mo agoauthor_emailfix: use correct Field struct syntax in rawLog tests
73aed192mo agoauthor_emailfeat: add Stmt.rawLog for low-level log0–log4 emission (#930)
2887a822mo agoauthor_emailfix: deduplicate hexDigit, remove dead code, fix stale docs (#376)
427a4802mo agoauthor_emailfix: expose compiler internals for structural induction proofs (#358)
6330c832mo agoauthor_emaildocs: Fix stale theorem count (252→296) and contract count (7→9)
89de5a92mo agoauthor_emailcleanup: Consolidate selector validation into main CI workflow
0d6961e2mo agoauthor_emailcleanup: Remove stale compiler/yul-new/ directory
b04b4322mo agoauthor_emailfix: CI path filters, scripts docs, index.mdx contract count
1f1afb42mo agoauthor_emailfix: Correct stale test counts (311→290, 30→23 suites)
b4fb6532mo agoauthor_emailfix: CI seed consistency, local test script, and stale docs
f771dbb2mo agoauthor_emaildocs: Add contracts table to README and CI doc-count validation
8d868c12mo agoauthor_emailfix(ir-interpreter): Fix 5 critical bugs reported by Bugbot
83b40902mo agoauthor_emailfeat(proofs): Complete EDSL-side proofs for Owned contract
ecebdf12mo agoauthor_email