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: 3mo agoDiscovered: Apr 23, 2026
Recent Claude Commits
release: prepare v1.0.0
74d8fe23mo agoauthor_emailfix: remove vestigial match on backendProfile in defaultRewriteBundleIdFor
9a25a393mo agoauthor_emailchore: update issue link to lfglabs-dev org
3e4f62c3mo agoauthor_emailchore: retrigger CI
c6c0dc53mo agoauthor_emailfix: update verify sync spec for parity-pack extraction
b814fa23mo agoauthor_emailExtract Morpho-specific parity rules from core compiler
f4daaef3mo agoauthor_emailci: sync parity-pack threshold across spec, source, and docs
d9c28fc4mo agoauthor_emailmerge: resolve conflicts with main
37f4c584mo agoauthor_emailfix: resolve SourceSemantics eq_def derivation failure for ceilDiv
40b51924mo agoauthor_emailfix: remove duplicate ceilDiv match arms and fix proof
6c243d64mo agoauthor_emailfix: resolve ceilDiv proof errors for Lean 4.22.0
fbfaf774mo agoauthor_emailfix: repair ceilDiv proof lemmas for Lean 4.22.0
45ac7034mo agoauthor_emailfeat: add ceilDiv stdlib primitive matching Solidity's Math256.ceilDiv
000d5df4mo agoauthor_emaildocs: update verification status to reflect Layer 2 proof WIP
1c9137a4mo agoauthor_emailfix: exclude sorry'd theorems from PrintAxioms to avoid sorryAx in axiom audit
d2b1e214mo agoauthor_emailfix: regenerate PrintAxioms, update verification artifacts, allowlist exposed proofs
dadb8044mo agoauthor_emailfix: sorry pre-existing proof failures exposed by from-scratch CI build
3715bf54mo agoauthor_emailfix: make state an explicit parameter in execStmt/execStmtList to fix termination proofs
8ca5b874mo agoauthor_emailfix(maint): add transferOwnership end-to-end tests for Owned and OwnedCounter
77360295mo agoauthor_emailfix(maint): propagate terminal halt through if_ branches in evalTStmtsFuel
877b3425mo agoauthor_emailfix(maint): merge storageAddr into flat storage in mkIRStateFromTyped
7da213b5mo agoauthor_emailfix(maint): add SafeCounter compilation and end-to-end tests
b1964b85mo agoauthor_emailfix(maint): add require-path end-to-end tests for withdraw and owned increment
913809b5mo agoauthor_emailfix(maint): use switch in if_ lowering to evaluate condition once
c358cac5mo agoauthor_emailfix(maint): add compilation smoke tests for Ledger, OwnedCounter, SimpleToken
39fd5ea5mo agoauthor_emailfix(maint): support address return values in typed IR compiler
a8562fe5mo agoauthor_emailfix(maint): add bool→uint256 coercion in typed IR compiler
75eba745mo agoauthor_emailfix(maint): add missing Expr.eq case to typed IR compiler
25986975mo agoauthor_emailfix(maint): halt typed IR evaluation after stop/returnUint
0feb19a5mo agoauthor_emailfix(maint): preserve branch-created locals in compileBranch
2d9fe865mo agoauthor_emailfix(maint): remove temporary debug files from stashed work restore
28b94ab5mo agoauthor_emailfix: correct sorry count in README and rename ContractSpec references in ROADMAP
34ea3d85mo agoauthor_emailfix: use correct Field struct syntax in rawLog tests
73aed195mo agoauthor_emailfeat: add Stmt.rawLog for low-level log0–log4 emission (#930)
2887a825mo agoauthor_emailfix: deduplicate hexDigit, remove dead code, fix stale docs (#376)
427a4805mo agoauthor_emailfix: expose compiler internals for structural induction proofs (#358)
6330c835mo agoauthor_emaildocs: Fix stale theorem count (252→296) and contract count (7→9)
89de5a95mo agoauthor_emailcleanup: Consolidate selector validation into main CI workflow
0d6961e5mo agoauthor_emailcleanup: Remove stale compiler/yul-new/ directory
b04b4325mo agoauthor_emailfix: CI path filters, scripts docs, index.mdx contract count
1f1afb45mo agoauthor_emailfix: Correct stale test counts (311→290, 30→23 suites)
b4fb6535mo agoauthor_emailfix: CI seed consistency, local test script, and stale docs
f771dbb5mo agoauthor_emaildocs: Add contracts table to README and CI doc-count validation
8d868c15mo agoauthor_emailfix(ir-interpreter): Fix 5 critical bugs reported by Bugbot
83b40905mo agoauthor_emailfeat(proofs): Complete EDSL-side proofs for Owned contract
ecebdf15mo agoauthor_email