Blockchain Papers

CARLES MARÍN MUÑOZ

A machine-checked, sorry-free formalization, in Lean 4 over Mathlib, of Sturm's theorem (1829): for a squarefree real polynomial p and an interval (a,b] whose endpoints are not roots, the number of distinct real roots of p in (a,b] equals V(a) − V(b), where V(x) is the number of sign changes of the Sturm sequence p, p′, −(p mod p′), … evaluated at x (zeros discarded). No root is ever located; two integers are subtracted. The mathematics is entirely classical and the result has been formalized before in other systems (Coq, by Cohen, within the construction of the real algebraic numbers; Isabelle/HOL, by Eberl, and in the Sturm–Tarski form by Li and Paulson; and HOL Light). To the best of the author's knowledge — based on searches of Loogle and Mathlib in June 2026 — this is the first proof of Sturm's theorem in Lean; it is a first-in-Lean and not a first-in-any-system. The contribution is therefore the formalization itself together with its reusable machinery: a small theory of sign variation, an inductive flank-reduction relation (FlankReduce) that decouples the chain's combinatorics from its algebra, and the local-to-global passage from a single root crossing to the interval count. A by-product is that Mathlib's existing count of coefficient sign variations (Descartes' rule, Polynomial.signVariations) and the count used here are, after unfolding, the same function — so the toolkit transfers verbatim to Descartes. The headline theorem Sturm.sturm depends only on the three standard axioms propext, Classical.choice, Quot.sound; no native_decide and no custom axiom. The whole proof is a single file (Sturm.lean, about 1,220 lines, ~60 declarations) depending on Mathlib alone. Scope, stated plainly: the theorem is proved for squarefree p over the reals; the passage to p/gcd(p,p′) for arbitrary polynomials is not formalized here. English and Spanish editions are included. Formalized with AI assistance (Claude, Anthropic); the mathematics and all claims are the author's responsibility, and the Lean kernel — not the assistant — certifies the proofs.

Joseph Robert Lopez

LLM guardrails face four structurally distinct barriers: algebraic blindness arising from syntactic monoid aperiodicity (unconditional); an illustrative information-theoretic lower bound (Fano-type, under a uniformity assumption); NP-hardness of instantiation verification; and structural transfer via free-category functoriality (unconditional) combined with string-level indistinguishability under a semantic-opacity assumption on symbol naming. Together these results characterize why inference-layer defenses are necessary but insufficient. We operationalize these barriers through five attack vectors. V1–V4 (homomorphic reasoning: decomposition, zero-knowledge pipelines, Tree-of-Thought solving over abstract grammars, and encoding bootstrap) exploit the information-theoretic and computational barriers against abstraction-based attacks. V5 (modular counting bypass) exploits algebraic blindness: we prove that all substring-matching regex guardrails have aperiodic syntactic monoids and are therefore provably blind to any payload encoded using modular counting. Empirically, V3 yields a mean yield of 0.466 for BFS, 0.172 for random-beam, and 0.122 for LLM-guided Tree-of-Thought (N=50, seeds 0–49, p{<}0.001); BFS dominates, as exhaustive search over small synthetic grammars outperforms LLM heuristic pruning. We extracted syntactic monoids from a corpus of 142 patterns drawn from twelve sources — 100 patterns shipped by nine third-party open-source guardrail projects and 42 patterns assembled from three author-curated pattern sets; 100\% are aperiodic, and the MOD_2 bypass construction succeeds against all aperiodic patterns. A 376-line proof-of-concept with three execution mediums validates all five vectors. We conclude that inference-layer guardrails are necessary but insufficient, and that effective defense must migrate to the execution layer where concrete artifacts become observable.

Lauri Alha

A machine-checked, sorry-free development in Lean 4 over Mathlib (about 1500 lines) that fills a gap in Mathlib — the dilogarithm Li2, which the library cites but does not define — and follows it into a quantum-mechanics problem. To the best of the author's knowledge, the first formalization in any proof assistant of: the real dilogarithm with Euler's reflection identity, Landen's transformation and the duplication formula; the golden-ratio ladder Li2(1/φ2) = π2/15 − ln2φ (derived from a 3×3 linear system, no five-term relation) and the Lee–Yang effective central charge c_eff = 2/5 (the simplest thermodynamic-Bethe-ansatz dilogarithm identity); the Clausen function Cl2 and Catalan's constant G = Cl2(π/2); the Fejér–Jackson inequality; the bound Cl2(θ) ≥ sin(θ)/2 by an asymptotics-free Abel summation; and the Margolus–Levitin and (an L1 form of the) Mandelstam–Tamm quantum speed limits. These assemble into the title theorem: the weight-2 zeta state (populations proportional to 1/n2 on equally spaced energy levels) has infinite mean energy and infinite energy variance — so both textbook speed limits say nothing — yet never reaches a state orthogonal to itself, because its autocorrelation is (6/π2)·Li2(e−iθ) and the dilogarithm has no zero on the unit circle. A clock with an unbounded energy budget that never ticks. Every identity is classical (Euler, Landen, Clausen, Fejér, Jackson, Mandelstam–Tamm, Margolus–Levitin); the contribution is the machine-checked development and its assembly. Every named theorem depends only on the three standard axioms (propext, Classical.choice, Quot.sound). Formalized with AI assistance (Claude, Anthropic); the mathematics and all claims are the author's responsibility.

Mingyue Zhang, Ming Liu, Xiang Ding, Yilei Wang · 5 authors

Consensus mechanisms are algorithms that ensure the security and stability of blockchain networks by achieving agreement and verifying transaction integrity. Proof of Stake (PoS) stands as a widely acknowledged consensus algorithm, wherein the privilege to validate transactions is predicated upon participants’ stakes. However, long-term use of PoS may lead to wealth concentration among certain nodes, potentially undermining the network’s fairness and security. Therefore, we propose the Group-Polynomial-based Election Proof of Stake (GPE-PoS) consensus mechanism. GPE-PoS involves categorizing nodes, calculating polynomial values for each group, encrypting these values using Paillier encryption, and then allocating validation rights based on comparisons of polynomial values based on polynomial value comparisons to enhance system fairness. The fairness of the system is further fortified against Sybil attacks, which undermine its security and fairness, through the incorporation of digital certificates within GPE-PoS, thereby verifying participant identities. Simulation results confirm that GPE-PoS successfully maintains fairness and security in blockchain systems.

Mihai Prunescu

To cater to the needs of (Zero Knowledge) proofs for (mathematical) proofs, we describe a method to transform formal sentences in 2x2-matrices over multivariate polynomials with integer coefficients, such that usual proof-steps like modus-ponens or the substitution are easy to compute from the matrices corresponding to the terms or formulas used as arguments. By evaluating the polynomial variables in random elements of a suitably chosen finite field, the proof is replaced by a numeric sequence. Only the values corresponding to the axioms have to be computed from scratch. The values corresponding to derived formulas are computed from the values corresponding to their ancestors by applying the homomorphic properties. On such sequences, various Zero Knowledge methods can be applied.

Craig Wright

This paper presents a formalised architecture for synthetic agents designed to retain immutable memory, verifiable reasoning, and constrained epistemic growth. Traditional AI systems rely on mutable, opaque statistical models prone to epistemic drift and historical revisionism. In contrast, we introduce the concept of the Merkle Automaton, a cryptographically anchored, deterministic computational framework that integrates formal automata theory with blockchain-based commitments. Each agent transition, memory fragment, and reasoning step is committed within a Merkle structure rooted on-chain, rendering it non-repudiable and auditably permanent. To ensure selective access and confidentiality, we derive symmetric encryption keys from ECDH exchanges contextualised by hierarchical privilege lattices. This enforces cryptographic access control over append-only DAG-structured knowledge graphs. Reasoning is constrained by formal logic systems and verified through deterministic traversal of policy-encoded structures. Updates are non-destructive and historied, preserving epistemic lineage without catastrophic forgetting. Zero-knowledge proofs facilitate verifiable, privacy-preserving inclusion attestations. Collectively, this architecture reframes memory not as a cache but as a ledger - one whose contents are enforced by protocol, bound by cryptography, and constrained by formal logic. The result is not an intelligent agent that mimics thought, but an epistemic entity whose outputs are provably derived, temporally anchored, and impervious to post hoc revision. This design lays foundational groundwork for legal, economic, and high-assurance computational systems that require provable memory, unforgeable provenance, and structural truth.

John C. Kolesar, Shan Ali, Timos Antonopoulos, Ružica Piskač

Zero-knowledge (ZK) protocols enable software developers to provide proofs of their programs’ correctness to other parties without revealing the programs themselves. Regular expressions are pervasive in real-world software, and zero-knowledge protocols have been developed in the past for the problem of checking whether an individual string appears in the language of a regular expression, but no existing protocol addresses the more complex PSPACE-complete problem of proving that two regular expressions are equivalent. We introduce Crêpe , the first ZK protocol for encoding regular expression equivalence proofs and also the first ZK protocol to target a PSPACE-complete problem. Crêpe uses a custom calculus of proof rules based on regular expression derivatives and coinduction, and we introduce a sound and complete algorithm for generating proofs in our format. We test Crêpe on a suite of hundreds of regular expression equivalence proofs. Crêpe can validate large proofs in only a few seconds each.

Jon Stephens, Shankara Pailoor, Işıl Dillig

Abstract Circuit languages like Circom and Gnark have become essential tools for programmable zero-knowledge cryptography, allowing developers to build privacy-preserving applications. These domain-specific languages (DSLs) encode both the computation to be verified (as a witness generator ) and the corresponding arithmetic circuits , from which the prover and verifier can be automatically generated. However, for these programs to be correct, the witness generator and the arithmetic circuit need to be mutually consistent in a certain technical sense, and inconsistencies can result in security vulnerabilities. This paper formalizes the consistency requirement for circuit DSLs and proposes the first automated technique for verifying it. We evaluate the method on hundreds of real-world circuits, demonstrating its utility for both automated verification and uncovering errors that existing tools are unable to detect.

Michael W. Raymond, Gillian Evers, Jan Ponti, Diya Krishnan · 5 authors

No abstract is available for this record.

Y. TAMURA, Akira Suzuki, Takaaki Mizuki

The 15-puzzle is a puzzle game played with 15 square tiles numbered from 1 to 15 on a 4 × 4 board. It has been popular for generations because of its simplicity and challenge. The (w × h)-puzzle is a generalization of the 15-puzzle, which is played with wh − 1 square tiles numbered from 1 to wh − 1 on a w × h board. Solving the (w × h)-puzzle is NP-hard, and hence it is valuable to know its solution. In this paper, we apply the concept of zero-knowledge proof to the (w × h)-puzzle. We propose a physical zero-knowledge proof protocol, in which a prover who knows a solution to the (w × h)-puzzle can convince a verifier that the prover knows the solution without revealing any information about it. We also design physical zero-knowledge proof protocols of two token swapping problems closely related to the (w × h)-puzzle.

Suthee Ruangwises

In this paper, we propose a physical protocol to verify the first nonzero term of a sequence using a deck of cards. The protocol lets a prover show the value of the first nonzero term of a given sequence to a verifier without revealing which term it is. Our protocol uses $Θ(1)$ shuffles, which is asymptotically lower than that of an existing protocol of Fukusawa and Manabe which uses $Θ(n)$ shuffles, where $n$ is the length of the sequence. We also apply our protocol to construct zero-knowledge proof protocols for three well-known logic puzzles: ABC End View, Goishi Hiroi, and Toichika. These protocols enables a prover to physically show that he/she know solutions of the puzzles without revealing them.

Xiaohui Hu, Huiwen Jia, Jingang Liu, Zhi‐Qi Zhao

Identity-based cryptography (IBC) can be applied to scenarios that involve a large number of public keys in each execution. In this paper, we propose an efficient identity-based ring signature scheme on lattices with signature size logarithmic to the cardinality of the ring. To this end, we first construct an efficient identity-based ring identification scheme by combining preimage sampling algorithms and a zero-knowledge proof system for a tree-based accumulator. Then we apply the Fiat-Shamir transformation and obtain a secure identity-based ring signature scheme. We prove its security in the random oracle model under the small integer solution assumption.

Hwanjo Heo, Seungwon Woo, Taeung Yoon, Min Suk Kang · 5 authors

We present a practical partitioning attack, which we call Gethlighting, that isolates an Ethereum full node from the rest of the network for hours without having to occupy (or eclipse) all of the target's peer connections.In Gethlighting, an adversary controls only about a half (e.g., 25 out of total 50) of all peer connections of a target node, achieving powerful partitioning with a small attack budget of operating several inexpensive virtual machines.At the core of Gethlighting, its lowrate denial-of-service (DoS) strategy effectively stops the growth of local blockchain for hours while leaving other Ethereum node operations undisturbed.We analyze how subtle and insignificant delays incurred by a low-rate DoS can lead to a powerful blockchain partitioning attack.The practical impact of Gethlighting is discussed -i.e., the attack is scalable and lowcost (only about $5,714 for targeting all Ethereum full nodes concurrently for 24 hours), and extremely simple to launch.We demonstrate the feasibility of Gethlighting with full nodes in the Ethereum mainnet and testnet in both controlled and realworld experiments.We identify a number of fundamental system characteristics in Ethereum that enable Gethlighting attacks and propose countermeasures that require some protocol and client implementation enhancements.Ethereum Foundation has acknowledged this vulnerability in September 2022 and one of our countermeasures has been accepted as a hotfix for Geth 1.11.0.

Yuichi Komano, Takaaki Mizuki

No abstract is available for this record.

Thibauld Feneuil, Antoine Joux, Matthieu Rivain

No abstract is available for this record.

Emmanuel Arrighi, Henning Fernau, Stefan Hoffmann, Markus Holzer · 7 authors

In the Intersection Non-Emptiness problem, we are given a list of finite automata $A_1,A_2,\dots,A_m$ over a common alphabet $Σ$ as input, and the goal is to determine whether some string $w\in Σ^*$ lies in the intersection of the languages accepted by the automata in the list. We analyze the complexity of the Intersection Non-Emptiness problem under the promise that all input automata accept a language in some level of the dot-depth hierarchy, or some level of the Straubing-Thérien hierarchy. Automata accepting languages from the lowest levels of these hierarchies arise naturally in the context of model checking. We identify a dichotomy in the dot-depth hierarchy by showing that the problem is already NP-complete when all input automata accept languages of the levels zero or one half and already PSPACE-hard when all automata accept a language from the level one. Conversely, we identify a tetrachotomy in the Straubing-Thérien hierarchy. More precisely, we show that the problem is in AC$^0$ when restricted to level zero; complete for LOGSPACE or NLOGSPACE, depending on the input representation, when restricted to languages in the level one half; NP-complete when the input is given as DFAs accepting a language in from level one or three half; and finally, PSPACE-complete when the input automata accept languages in level two or higher. Moreover, we show that the proof technique used to show containment in NP for DFAs accepting languages in the Straubing-Thérien hierarchy levels one ore three half does not generalize to the context of NFAs. To prove this, we identify a family of languages that provide an exponential separation between the state complexity of general NFAs and that of partially ordered NFAs. To the best of our knowledge, this is the first superpolynomial separation between these two models of computation.

Thomas Attema, Ronald Cramer, Lisa Kohl

We show a lattice-based solution for commit-and-prove transparent circuit zero-knowledge (ZK) with polylog-communication, the first not depending on PCPs. We start from compressed Σ-protocol theory (CRYPTO 2020), which is built around basic Σ-protocols for opening an arbitrary linear form on a long secret vector that is compactly committed to. These protocols are first compressed using a recursive “folding-technique” adapted from Bulletproofs, at the expense of logarithmic rounds. Proving in ZK that the secret vector satisfies a given constraint – captured by a circuit – is then by (blackbox) reduction to the linear case, via arithmetic secret-sharing techniques adapted from MPC. Commit-and-prove is also facilitated, i.e., when commitment(s) to the secret vector are created ahead of any circuit-ZK proof. On several platforms (incl. DL) this leads to logarithmic communication. Non-interactive versions follow from Fiat-Shamir. This abstract modular theory strongly suggests that it should somehow be supported by a lattice platform as well. However, when going through the motions and trying to establish low communication (on an SIS-platform), a certain significant lack in current understanding of multi-round protocols is exposed. Namely, as opposed to the DL-case, the basic Σ-protocol in question typically has poly-small challenge space. Taking into account the compression-step – which yields non-constant rounds – and the necessity for parallelization to reduce error, there is no known tight result that the compound protocol admits an efficient knowledge extractor. We resolve the state of affairs here by a combination of two novel results which are fully general and of independent interest. The first gives a tight analysis of efficient knowledge extraction in case of non-constant rounds combined with poly-small challenge space, whereas the second shows that parallel repetition indeed forces rapid decrease of knowledge error. Moreover, in our present context, arithmetic secret sharing is not defined over a large finite field but over a quotient of a number ring and this forces our careful adaptation of how the linearization techniques are deployed. We develop our protocols in an abstract framework that is conceptually simple and can be flexibly instantiated. In particular, the framework applies to arbitrary rings and norms.

Firas Kraiem, Shuji Isobe, Eisuke Koizumi, Hiroki Shizuya

Inspired by the work of Ghadafi and Groth (ASIACRYPT 2017) on a certain type of computational hardness assumptions in cyclic groups (which they call ``target assumptions''), we initiate an analogous work on another type of hardness assumptions, namely the ``knowledge-of-exponent'' assumptions (KEAs). Originally introduced by Damgard to construct practical encryption schemes secure against chosen ciphertext attacks, KEAs have subsequently been used primarily to construct succinct non-interactive arguments of knowledge (SNARKs), and proved to be inherent to such constructions. Since SNARKs (and their zero-knowledge variant, zk-SNARKs) are already used in practice in such systems as the Zcash digital currency, it can be expected that the use of KEAs will increase in the future, which makes it important to have a good understanding of those assumptions. Using a proof technique first introduced by Bellare and Palacio (but acknowledged by them as being due to Halevi), we first investigate the internal structure of the q-power knowledge-of-exponent (q-PKE) family of assumptions introduced by Groth, which is thus far the most general variant of KEAs. We then introduce a generalisation of the q-PKE family, and show that it can be simplified.

Craig Calcaterra, Wulf A. Kaal, Vadhindran K. Rao

Insurance products can be optimized with emerging decentralized technology. We propose the use of cryptocurrencies as claims on future cash flows of an underwriting business operated by a Decentralized Autonomous Organization (DAO). The design of our DAO allows for decentralized collaboration (i) among DAO underwriters as well as (ii) between underwriters and consumers. In this decentralized system, the tokens essentially substitute for reputation. Financial distress or bankruptcy of an individual underwriter does not have to affect either customers or the DAO as the insurance contracts are backed by encumbered tokens. The structure of incentives embedded in the design has the potential to lower capital requirements and the related need for capital regulation.

Stefano Tempesta

No abstract is available for this record.

Jonathan Bootle, Vadim Lyubashevsky, Gregor Seiler

A key component of many lattice-based protocols is a zero-knowledge proof of knowledge of a vector \(\vec {s}\) with small coefficients satisfying \(A\vec {s}=\vec {u}\bmod \,q\). While there exist fairly efficient proofs for a relaxed version of this equation which prove the knowledge of \(\vec {s}'\) and c satisfying \(A\vec {s}'=\vec {u}c\) where \(\Vert \vec {s}'\Vert \gg \Vert \vec {s}\Vert \) and c is some small element in the ring over which the proof is performed, the proofs for the exact version of the equation are considerably less practical. The best such proof technique is an adaptation of Stern’s protocol (Crypto ’93), for proving knowledge of nearby codewords, to larger moduli. The scheme is a \(\varSigma \)-protocol, each of whose iterations has soundness error \(2{/}3\), and thus requires over 200 repetitions to obtain soundness error of \(2^{-128}\), which is the main culprit behind the large size of the proofs produced.

Remo Pfister, Keerthikan Thurairatnam

Introduction: &#13;\nThe study work focuses on designing a smart contract language (named "Lazo") for the Bazo blockchain. The Bazo blockchain is a research blockchain to test different mechanisms and algorithms. In the current version, a Proof of Stake consensus algorithm and a virtual machine to execute Bazo intermediate language(opcodes) are integrated. However, writing smart contracts in Bazo opcodes is time&#13;\nconsuming and error-prone. The goal of this study work is to design a high-level language which is easier to read and write smart contracts.&#13;\n&#13;\nProcedure / Result: &#13;\nBefore designing Lazo, 24 existing smart contract languages are collected and roughly analyzed to identify the key characteristics of a language for the blockchain. Thereafter, three popular and well elaborated languages, namely Solidity, Vyper and Scilla, were analyzed in great detail. Their supported features, syntax and contract examples were also documented. With the acquired knowledge about smart contracts, Lazo language was designed in an agile manner.&#13;\n&#13;\nResult: &#13;\nAs a result, Lazo is designed to be a statically typed, imperative and non-turing complete programming language. All language features are documented with illustrative code snippets. The Lazo grammar is also written in ANTLR and&#13;\nverified with Java. Furthermore, contract examples from Solidity are translated to Lazo in order to prove that the real-world use cases can be programmed with Lazo&#13;\nas well.&#13;\n&#13;\nIn a follow-up thesis, a compiler could be developed to compile Lazo programs into Bazo virtual machine instructions.

P. Hecht

Post-Quantum Cryptography (PQC) attempts to find cryptographic protocols resistant to attacks using Shor polynomial time algorithm for numerical field problems or Grover search algorithm. A mostly overlooked but valuable line of solutions is provided by non-commutative algebraic structures, specifically canonical protocols that rely on one-way trapdoor functions (OWTF). Here we develop an algebraic framework who could be applied to different asymmetric protocols like D-H KE (Diffie-Hellman key exchange), Public Key Encryption, Digital Signature, ZKP (zero-knowledge proof) authentication, Oblivious Transfer, Multi-Party Computing, and so on. The trapdoor one-way functions selected are (a) Triple decomposition Problem (TDP) developed by Kurt, where a known element is factored into a product of three unknown factors and (b) a new version of conjugacy search that we refer from now on as Blind Conjugacy Search Problem (BCSP). Our platform structure is the general linear group GL(d,F_p) d-square non-singular matrices of prime field values. We give support to the fact that this framework is cryptographically secure against classical attacks like linear algebra attacks, length-based attacks, side-channel attacks against square (or duplicate) and multiply (or sum) algorithm, high sensitivity to pseudo random deterministic generators, etc. At same time it is immune against quantum attacks (using Grover and Shor), if the size parameters are carefully selected. Semantic security and IND-CCA2 compliance for this framework is discussed.

Benjamin Hellouin de Ménibus, Ville Salo, Guillaume Theyssier

Abelian cellular automata (CAs) are CAs which are group endomorphisms of the full group shift when endowing the alphabet with an abelian group structure. A CA randomizes an initial probability measure if its iterated images have weak*-convergence towards the uniform Bernoulli measure (the Haar measure in this setting). We are interested in structural phenomena, i.e., randomization for a wide class of initial measures (under some mixing hypotheses). First, we prove that an abelian CA randomizes in Cesàro mean if and only if it has no soliton, i.e., a non-zero finite configuration whose time evolution remains bounded in space. This characterization generalizes previously known sufficient conditions for abelian CAs with scalar or commuting coefficients. Second, we exhibit examples of strong randomizers, i.e., abelian CAs randomizing in simple convergence; this is the first proof of this behaviour to our knowledge. We show, however, that no CA with commuting coefficients can be strongly randomizing. Finally, we show that some abelian CAs achieve partial randomization without being randomizing: the distribution of short finite words tends to the uniform distribution up to some threshold, but this convergence fails for larger words. Again this phenomenon cannot happen for abelian CAs with commuting coefficients.