Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation
当前主流神经网络推理依赖存放在高带宽显存中的稠密浮点权重矩阵，既受严重的内存墙瓶颈制约，也无法在以太坊虚拟机（EVM）等确定性虚拟机上原生执行。而在 Blum-Shub-Smale 模型下，对连续域上递归动力系统的终止性与算术不变量做验证一
#lean4
共收录 4 条相关情报。
← 返回所有主题Hydrozoan: Latency-Adaptive DAG Consensus under Mixed Byzantine and Crash Faults
本文提出 Hydrozoan，一个面向混合故障模型的 DAG（有向无环图）共识协议。背景是：基于 DAG 的共识可达很高吞吐，并在 n=3f+1 的经典设定下达到最优的三消息延迟下界；已有的两消息延迟协议要么靠牺牲容错度（例如需要 5f+1
Formal verification of the S-two AIR
本文介绍了使用Lean 4证明助手对StarkWare的S-two证明器中的代数中间表示（AIR）进行形式化验证的工作。S-two证明器用于在区块链上高效地证明用Cairo虚拟机语言编写的程序能够运行完成。该证明器通过一个代数中间表示（AI
Tridirectional Discriminating-Power Formal Verification of Smart Contract Reentrancy Defense Against Production-Deployed Solidity Source
本文提出了首个经过机器检查的OpenZeppelin重入防护模式正确性证明，该证明针对生产部署的Solidity源代码的Lean 4状态机模型。所有十三个定理都经过了机器检查，没有使用任何“sorry”或用户引入的公理，公理足迹仅由[pro