Harden formal audit trust gates

[Th0rgal]

Summary

• replace the inline CI axiom grep with the repository axiom registry checker, extend discovery to optional Benchmark/ and Contracts/ trees, and wire the shared checks into make check / verify-sync
• add trust-surface and benchmark metadata registry checks for formal-audit publication boundaries, including native_decide, @[implemented_by], partial def, and ECM axioms := [...] strings
• clean up Bugbot findings by removing the unused trust-surface ECM regex/helper and sharing benchmark case.yaml discovery between CLI output and validation
• harden ECM/codegen surfaces: bind ABI static-array length once, tighten Keccak padding preconditions, allocate callback calldata from the Solidity free-memory pointer, and document/gate the expanded hashing/call trust assumptions
• add/refresh smoke coverage and docs for mapping-word shapes, arithmetic panic lowering, hashing helpers, EIP-712 digest helpers, callback helpers, Solmate-style ERC-20 helpers, and the Osaka/Fusaka intrinsic fork naming

Verification

• make check
• lake build Compiler.CompilationModelFeatureTest Compiler.Keccak.Sponge Compiler.Keccak.SpongeTest Compiler.Modules.Hashing Compiler.Modules.ERC20 Compiler.Modules.Callbacks
• python3 scripts/check_trust_surface_registry.py && python3 scripts/check_axioms.py
• python3 -m unittest scripts/test_check_benchmark_cases.py scripts/test_check_trust_surface_registry.py scripts/test_check_axioms.py -v

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	May 27, 2026 9:12am

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit 18468af. Configure here.}