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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Introduction: \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 \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. \n \nProcedure / Result: \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. \n \nResult: \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 \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 \nas well. \n \nIn a follow-up thesis, a compiler could be developed to compile Lazo programs into Bazo virtual machine instructions.
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.
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.
The concept of a Turing machine has been well defined. It would be sufficient to show that Bitcoin uses a dual stack architecture that acts as a dual counter machine. Such systems have already been demonstrated as being Turing complete. We demonstrate that Bitcoin script is a minimal family of which λ and R are members. Further using the compositional product rule and the iteration rule we demonstrate that Bitcoin scripting is Turing complete with the limitations imposed on any realworld computer. This limitation is that there cannot be an infinite tape. Iterations can be simulated using an âunrolledâ loop function with allocation to the âAltâ stack. As the product rule states that if A, B are machines, then A.B is also a machine. The iteration rule shows that if A is a machine then (A) is also a machine. Further the minimum power of A under which the observed square of the final configuration is blank. The consequence of these rules is that for every partial recursive function of in variables we can show that it can be evaluated by machine of the proposed family.
Eli BenâSasson, Alessandro Chiesa, Michael A. Forbes, Ariel Gabizon · 6 authors
We present the first constructions of single-prover proof systems that achieve perfect zero knowledge (PZK) for languages beyond NP, under no intractability assumptions: 1. The complexity class #P has PZK proofs in the model of Interactive PCPs (IPCPs) [KR08], where the verifier first receives from the prover a PCP and then engages with the prover in an Interactive Proof (IP). 2. The complexity class NEXP has PZK proofs in the model of Interactive Oracle Proofs (IOPs) [BCS16,RRR16], where the verifier, in every round of interaction, receives a PCP from the prover. Our constructions rely on succinct simulators that enable us to "simulate beyond NP", achieving exponential savings in efficiency over [BCGV16]. These simulators crucially rely on solving a problem that lies at the intersection of coding theory, linear algebra, and computational complexity, which we call the succinct constraint detection problem, and consists of detecting dual constraints with polynomial support size for codes of exponential block length. Our two results rely on solutions to this problem for fundamental classes of linear codes: * An algorithm to detect constraints for Reed--Muller codes of exponential length. * An algorithm to detect constraints for PCPs of Proximity of Reed--Solomon codes [BS08] of exponential degree. The first algorithm exploits the Raz--Shpilka [RS05] deterministic polynomial identity testing algorithm, and shows, to our knowledge, a first connection of algebraic complexity theory with zero knowledge. Along the way, we give a perfect zero knowledge analogue of the celebrated sumcheck protocol [LFKN92], by leveraging both succinct constraint detection and low-degree testing. The second algorithm exploits the recursive structure of the PCPs of Proximity to show that small-support constraints are "locally" spanned by a small number of small-support constraints.
The cipher (or athbash, under which name Web3 defines it) is a Hebrew substitution cipher which replaces the first letter of the Hebrew alphabet (aleph, 1\) by the last (tav, ) the second (beth, J) by the last but one (shin, IJI), and so on, unti I we get to the last (ta , n), which i replaced by the first (aleph, 1\). Jan Anderson described it in Fledge Ledge Edge (WW 8. 1997229). Naturally, the idea can be applied to our alphabet; following the precedent set by atbash I name it the azby cipher.
An investigation of interactive proof systems (IPSs) where the verifier is a 2-way probabilistic finite state automaton (2pfa) is initiated. In this model, it is shown: Additional results concern two other classes of verifiers: 2pfa's that halt in polynomial expected time, and 2-way probabilistic pushdown automata that halt in polynomial time. In particular, IPSs with verifiers in the latter class are as powerful as IPSs where verifiers are polynomial-time probabilistic Turing machines. In a companion paper [7], zero knowledge IPSs with 2pfa verifiers are investigated.
A Perfect Zero-Knowledge interactive proof system convinces a verifier that a string is in a language without revealing any additional knowledge in an information-theoretic sense. We show that for any language that has a perfect zero-knowledge proof system, its complement has a short interactive protocol. This result implies that there are not any perfect zero-knowledge protocols for NP-complete languages unless the polynomial time hierarchy collapses. This paper demonstrates that knowledge complexity can be used to show that a language is easy to prove.