Skip to content

Navigation Menu

Appearance settings

View all features
- BY COMPANY SIZE
  Enterprises
  Small and medium teams
  Startups
  Nonprofits
- BY USE CASE
  App Modernization
  DevSecOps
  DevOps
  CI/CD
  View all use cases
- BY INDUSTRY
  Healthcare
  Financial services
  Manufacturing
  Government
  View all industries
View all solutions
- EXPLORE BY TOPIC
  AI
  Software Development
  DevOps
  Security
  View all topics
- EXPLORE BY TYPE
  Customer stories
  Events & webinars
  Ebooks & reports
  Business insights
  GitHub Skills
- SUPPORT & SERVICES
  Documentation
  Customer support
  Community forum
  Trust center
  Partners
View all resources
- COMMUNITY
  GitHub SponsorsFund open source developers
- PROGRAMS
  Security Lab
  Maintainer Community
  Accelerator
  GitHub Stars
  Archive Program
- REPOSITORIES
  Topics
  Trending
  Collections
- ENTERPRISE SOLUTIONS
  Enterprise platformAI-powered developer platform
- AVAILABLE ADD-ONS
  GitHub Advanced SecurityEnterprise-grade security features
  Copilot for BusinessEnterprise-grade AI features
  Premium SupportEnterprise-grade 24/7 support
Pricing

Search code, repositories, users, issues, pull requests...

Search

Clear

Search syntax tips

Provide feedback

We read every piece of feedback, and take your input very seriously.

Include my email address so I can be contacted

Saved searches

Use saved searches to filter your results more quickly

Name

Query

To see all available qualifiers, see our documentation.

Appearance settings

You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session.

Dismiss alert

lfglabs-dev / verity Public

Notifications You must be signed in to change notification settings
Fork 4
Star 69

Code
Issues 8
Pull requests 1
Discussions
Actions
Projects
Security and quality
Insights

Additional navigation options

Code
Issues
Pull requests
Discussions
Actions
Projects
Security and quality
Insights

proofs: expose native EVMYulLean transition target#1743

Open

Th0rgal wants to merge 162 commits intomainlfglabs-dev/verity:mainfrom

codex/native-evmyullean-transitionlfglabs-dev/verity:codex/native-evmyullean-transitionCopy head branch name to clipboard

Conversation Commits162 (162)Checks Files changed

Open

proofs: expose native EVMYulLean transition target#1743
Th0rgal wants to merge 162 commits intomainfrom
codex/native-evmyullean-transition

Commits

Commits on Apr 22, 2026

proofs: expose native EVMYulLean transition target
claude
committed
docs: clarify verity helper calls
claude
committed
proofs: track native transition blockers
claude
committed
proofs: harden native runtime smoke coverage
claude
committed
proofs: document native env defaults
claude
committed
proofs: pin native dispatch selector cases
claude
committed
proofs: pin native dispatch case bodies
claude
committed
proofs: pin native calldata bridge bytes
claude
committed
proofs: pin native dispatcher selector expression
claude
committed
docs: clarify native dispatcher execution blocker
claude
committed
proofs: pin native error rollback projection
claude
committed
proofs: require native observable slots
claude
committed
proofs: pin native observable sload
claude
committed
proofs: cover native IR entrypoint
claude
committed
proofs: cover native log projection arities
claude
committed
proofs: cover native transient storage
claude
committed
proofs: cover native stop halt projection
claude
committed
proofs: cover native value result projection
claude
committed
proofs: cover native return halt projection
claude
committed
proofs: pin native halt builtin lowering
claude
committed
proofs: cover native ok storage projection
claude
committed
proofs: pin native final mapping projection
claude
committed
proofs: pin native helper call partition
claude
committed
proofs: pin native initial state bridge
claude
committed
proofs: pin native nested helper rejection
claude
committed
proofs: pin native hard error rollback
claude
committed
proofs: pin native return dispatch lowering
claude
committed
proofs: pin native explicit storage slots
claude
committed
proofs: pin native revert rollback
claude
committed
proofs: pin native IR slot forwarding
claude
committed
proofs: pin native transaction environment
claude
committed
proofs: name native bridge invariants
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native projection outcomes
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native initial state invariants
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native storage seeding invariant
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native execution pipeline invariant
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native IR execution pipeline invariant
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native account installation invariant
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native environment defaults invariant
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native calldata size invariant
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native halt projection invariants
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name native event projection invariants
claude
committed
chore: auto-refresh derived artifacts
github-actions[bot]
committed
proofs: name omitted native storage invariant
claude
committed
proofs: name native finalMappings invariant
claude
committed
proofs: name native final storage invariants
claude
committed
proofs: name native result observable invariants
claude
committed
proofs: name missing native account storage invariant
claude
committed
proofs: name native missing slot result invariants
claude
committed
proofs: name native final mapping invariants
claude
committed
proofs: name native non-word return fallback
claude
committed
proofs: name native call lowering invariants
claude
committed
proofs: name native environment bridge fields
claude
committed
scripts: recognize partial defs in proof length check
claude
committed
scripts: test partial defs terminate proof spans
claude
committed
ci: include native harness in evmyullean probe
claude
committed
proofs: compare native env smoke with oracle
claude
committed
ci: guard native transition doc status
claude
committed
ci: guard native observable slot caveat
claude
committed
ci: guard native observable slot api
claude
committed
contracts: close evmyullean transition blockers
claude
committed
contracts: harden overload and env accessors
claude
committed
contracts: add migration parity surfaces
claude
committed
contracts: remove legacy internal call surface
claude
committed
contracts: fix overload review regressions
claude
committed
contracts: memoize tuple array element index
claude
committed
contracts: fail closed on ambiguous overload lookup
claude
committed
compiler: recurse trust surface through array element words
claude
committed
compiler: reject internal external name collisions
claude
committed
proofs: cover native selector bytes and new source cases
claude
committed
contracts: close tuple array element review gaps
claude
committed
proofs: add native dispatch oracle
claude
committed
contracts: harden overload generated names
claude
committed
proofs: cover memory return native oracle
claude
committed
compiler: document selector-keyed overload dispatch
claude
committed
proofs: cover native calldata argument oracle
claude
committed
evmyullean: lower native dispatch lazily
claude
committed
proofs: cover native mapping oracle shapes
claude
committed
evmyullean: scope lazy native dispatch
claude
committed
proofs: cover native packed mapping oracle
claude
committed
evmyullean: thread native switch ids
claude
committed
macro: accept qualified blobbasefee
claude
committed
evmyullean: guard native switch fallthrough
claude
committed
ci: guard native theorem transition target
claude
committed
ci: pin unbridged native env boundary
claude
committed
evmyullean: remove dead native stmt wrapper
claude
committed
compilation: split array element helper gates
claude
committed
macro: reject ABI-erased newtype overloads
claude
committed
proofs: expose native runtime preservation seam
claude
committed
evmyullean: validate native environment reads
claude
committed
evmyullean: freshen native switch temps
claude
committed
evmyullean: reserve function switch temps
claude
committed
proofs: align native bridge observables
claude
committed
evmyullean: validate native env on selected path
claude
committed
compiler: restrict plain arrayElement to word arrays
claude
committed
compiler: share array element usage traversal
claude
committed
proofs: add native bridge intro theorem
claude
committed

Commits on Apr 23, 2026

proofs: expose lowered native dispatcher bridge
claude
committed
compiler: preserve shadowed context accessors
claude
committed
compiler: include package roots for module imports
claude
committed
compiler: simplify array element usage detection
claude
committed
tests: cover context accessor shadow smoke
claude
committed
proofs: expose native runtime lowering equations
claude
committed
evmyullean: normalize native dispatch selector
claude
committed
macro: track tuple array return temp
claude
committed
evmyullean: expose statement native lowering equations
claude
committed
macro: resolve declared context-name shadows
claude
committed
proofs: expose native dispatcher block bridge
claude
committed
proofs: target lowered dispatcher block
claude
committed
proofs: expose raw native dispatcher exec
claude
committed
proofs: narrow native dispatcher agreement
claude
committed
compiler: allow namespaced internal helper names
claude
committed
proofs: expose native selector evaluation
claude
committed
compiler: lower storage words in typed ir
claude
committed
proofs: expose native selector recomposition
claude
committed
proofs: reduce native selector byte decoding
claude
committed
semantics: execute setStorageWord in source model
claude
committed
proofs: reduce native selector read bridge
claude
committed
proofs: prove native selector evaluation
claude
committed
runtime: mirror packed address word writes
claude
committed
proofs: expose native switch guard execution
claude
committed
semantics: mirror raw storage word writes
claude
committed
compiler: scan nested array helper usage
claude
committed
proofs: expose native switch selected case
claude
committed
compiler: scope duplicate signatures to dispatch
claude
committed
proofs: skip matched native switch cases
claude
committed
runtime: ignore user functions in native builtin scan
claude
committed
compiler: clarify array element word offsets
claude
committed
proofs: package marked native switch case
claude
committed
ci: register packed address macro smoke
claude
committed
ci: sync evmyullean fork audit pin
claude
committed
proofs: package native switch prefix
claude
committed
compiler: wrap storage word slots
claude
committed
proofs: package native switch freshness
claude
committed
proofs: package native switch default guard
claude
committed
proofs: package native switch case miss
claude
committed
proofs: generalize native switch guard fuel
claude
committed
proofs: prove native switch case chains
claude
committed
proofs: package native switch defaults
claude
committed
macro: erase ADTs in ABI overload keys
claude
committed
proofs: bridge native switch selector lookup
claude
committed
checks: address native transition review findings
claude
committed
proofs: factor native switch body preservation
claude
committed
typed-ir: reject ambiguous signature lookup
claude
committed
proofs: compose native switch defaults
claude
committed
proofs: preserve native switch case lookup
claude
committed
proofs: parameterize native switch prefix
claude
committed
proofs: expose native switch block parts
claude
committed
proofs: bridge raw native switch blocks
claude
committed
proofs: trim native switch proof guard
claude
committed
native: reject unbridged header builtins
claude
committed
proofs: package native assignment preservation
claude
committed

Footer

© 2026 GitHub, Inc.

Footer navigation

Terms
Privacy
Security
Status
Community
Docs
Contact

You can’t perform that action at this time.