@Wongssh web3 reading list. A reading list for solidity, web3 and Dapp programmers. We use Chinese and English language.
First high-severity Solidity compiler bug since 2016 — identified by Hexens
Hexens has identified a HIGH severity vulnerability in the Solidity compiler itself.
Not in a specific project. In Solidity.
The issue, TSTORE Poison, can silently corrupt contract storage and introduce critical vulnerabilities without obvious indicators. This makes it particularly dangerous for developers and auditors who rely on compiler-level guarantees.
To assess the ecosystem-wide impact, we used Glider to scan integrated chains and evaluate the potential blast radius. Cross-chain impact analysis at this scale is exactly what Glider is designed for.
🔎 Technical write-up:
https://hexens.io/research/solidity-compiler-bug-tstore-poison
📢 Official announcement:
https://x.com/solidity_lang/status/2024181697168945228?s=46
If you develop or audit Solidity smart contracts, we strongly recommend reviewing the report
Hexens has identified a HIGH severity vulnerability in the Solidity compiler itself.
Not in a specific project. In Solidity.
The issue, TSTORE Poison, can silently corrupt contract storage and introduce critical vulnerabilities without obvious indicators. This makes it particularly dangerous for developers and auditors who rely on compiler-level guarantees.
To assess the ecosystem-wide impact, we used Glider to scan integrated chains and evaluate the potential blast radius. Cross-chain impact analysis at this scale is exactly what Glider is designed for.
🔎 Technical write-up:
https://hexens.io/research/solidity-compiler-bug-tstore-poison
📢 Official announcement:
https://x.com/solidity_lang/status/2024181697168945228?s=46
If you develop or audit Solidity smart contracts, we strongly recommend reviewing the report
https://blog.lambdaclass.com/amo-lean-towards-formally-verified-optimization-via-equality-saturation-in-lean-4/
形式化证明 #formalVerify 密码学优化
形式化证明 #formalVerify 密码学优化
LambdaClass Blog
AMO-Lean: Towards Formally Verified Optimization via Equality Saturation in Lean 4
Our experiments with Lean and formal verification continue to bear fruit.
To further our knowhow and experience, we set out to see if we could apply Lean's strengths to a more advanced topic: compiler optimizations.
Traditional verified compilers focus…
To further our knowhow and experience, we set out to see if we could apply Lean's strengths to a more advanced topic: compiler optimizations.
Traditional verified compilers focus…
https://blog.lambdaclass.com/building-a-minimalist-post-quantum-ethereum-client-ethlambdas-architecture/
构建最小的 #pq 以太坊客户端
构建最小的 #pq 以太坊客户端
LambdaClass Blog
Building a Minimalist Post-Quantum Ethereum Client: ethlambda's Architecture
This is a follow-up to our post on building a post-quantum Ethereum client. Here we detail ethlambda's minimalist architecture.
https://ethpandaops.io/posts/evm-gas-profiling/
EthPandaOps 新推出的数据集 #dataAnalysis 与数据分析面板
EthPandaOps 新推出的数据集 #dataAnalysis 与数据分析面板
ethPandaOps
EVM Gas Profiling: New Execution Trace Data
New EVM execution trace data in the Xatu dataset, a Gas Profiler in The Lab, and a Gas Repricing Simulator for testing gas schedule changes against real blocks.
https://blog.lambdaclass.com/engineering-ethereums-speed-how-we-made-ethrex-20x-faster/
ethrex 性能优化
ethrex 性能优化
LambdaClass Blog
Engineering Ethereum's Speed: How we made Ethrex 20x faster
Over the past months, the ethrex team has been relentlessly focused on performance optimization. Through systematic profiling, targeted improvements, and architectural changes, we've achieved a 20x improvement in block execution throughput.
https://www.potuz.net/posts/gloas-annotated-forkchoice/
#ethereum #POS 共识规范解析
#ethereum #POS 共识规范解析
Canonical Reorgs & Reflections
Gloas Annotated: Forkchoice
This is the third post on the series of annotating the Gloas fork. In this post we will go over the forkchoice changes. Some final details are still missing in forkchoice, particularly dealing with PTC dual deadlines and how to handle the data available boolean…
https://jbecker.dev/research/prediction-market-microstructure
Kalshi 预测市场数据分析
Kalshi 预测市场数据分析
www.jbecker.dev
The Microstructure of Wealth Transfer in Prediction Markets
Slot machines on the Las Vegas Strip return about 93 cents on the dollar. This is widely considered some of the worst odds in gambling. Yet on Kalshi, a CFTC-regulated prediction market, traders have wagered vast sums on longshot contracts with historical…
https://formal.land/blog/2026/01/14/formal-verification-keccak-plonky3
使用 Rocq 证明 #zk 电路内函数正确性
使用 Rocq 证明 #zk 电路内函数正确性
formal.land
🥷 Formal verification of the Keccak precompile from Plonky3 | Formal Land
In this blog post, we present our work to formally verify the determinism of the Keccak precompile ZK circuits in Plonky3 using our 🍀 Garden framework.
https://muellerberndt.medium.com/finding-soundness-bugs-in-zk-circuits-ea23387a0e1e
#zk #security 安全研究和案例
#zk #security 安全研究和案例
Medium
A Practical Guide to Finding Soundness Bugs in ZK Circuits.
Zero-knowledge proofs are a core building block for blockchain scaling and privacy. In real-world deployments, the fragile part is usually…
