Ethereum block building has traditionally been approached using greedy algorithms that prioritize transactions with the highest fee per unit of gas. This work proposes an alternative that considers semantic interactions among transactions and operational constraints to define the utility of transaction combinations. Through a utility model that assigns bonuses and penalties to pairs and triples of transactions, we design algorithms capable of constructing blocks more valuable than those obtained by traditional methods. In experiments with 1,000 real transactions extracted from the network, two algorithms were implemented and evaluated, both grounded in a formulation inspired by job scheduling theory: a classic greedy baseline and the proposed heuristic. The base heuristic achieved approximately 86 % of the utility of the greedy approach ($6.78 \times 10^{20}$vs.$7.81 \times 10^{20}$) while including only 23 transactions. The extended version with greedy fill reached up to 120 % of the reference utility ($1.73 \times 10^{21}$), incorporating 268 transactions compared to 212 for the greedy, while maintaining execution times below 2 seconds. These preliminary results demonstrate the feasibility of capturing additional semantic value within time windows compatible with Ethereum block-building intervals, based on isolated experiments with bounded transaction sets.
Ziyang Liu, Kenneth MacKenzie, Roman Kireev, Michael Peyton Jones · 6 authors
The Cardano blockchain is the first to use proof of stake, offers native support for multiple currencies and is evolving toward a distributed governance model. It supports smart contracts through Plutus, a language based on System Fω with recursion. About half a dozen languages compile into Plutus, the first of which is Plinth (formerly Plutus Tx) — a language that reuses a subset of the Haskell syntax, and has been in commercial use since 2021.
Antoine Bak, Guilhem Jazeron, Pierre Galissant, Léo Perrin
In recent years, many hash functions have been introduced to satisfy the pressing need of some zero-knowledge protocols for such primitives allowing a low degree verification of their round function when arithmetized over a large field.While this can be achieved by restricting their sub-components to low-degree functions (and their inverse), the newest primitives in this category also leverage the intricacies of some proof systems to use “Split-and-Lookup” non-linear functions that essentially apply a small S-box in parallel over the binary representation of a field element.Such components excel at hindering attacks relying on polynomial system solving, but they offer poor security against statistical attacks. On the other hand, low degree monomials offer the opposite guarantees, being strong against statistical attacks. Several primitives have recently been proposed that combine such components in different ways in order to get the best from both.In this paper, we target such primitives by relying on the low degree components to allow a low-cost polynomial solving step. The weakness of Split-and-Lookups against linear attacks is used to simplify these systems, and their weakness against differential attacks is then used to propagate across many rounds the differential patterns obtained during polynomial solving. We instantiate this general approach by attacking round-reduced Monolith, and providing a distinguisher on full-round Skyscraper. These result then shed some light on how to best combine the different types of components to achieve the highest security.
IntroductionIn mathematics and theoretical computer science, a fixed point of an operator $F$ is an entity $x$ such that $F(x) = x$. Fixed-point results appear across many domains: for example, Banach’s Fixed-Point Theorem guarantees a unique fixed point for any contraction mapping on a complete metric space, and the Knaster–Tarski Theorem ensures that every monotone function on a complete lattice has a fixed point. These classical theorems establish existence (and sometimes uniqueness) of solutions to $x = F(x)$ under various conditions. In recursive and computational settings, fixed points enable self-referential definitions – a recursive function can be seen as a fixed point of a functional that “unwinds” one step of the recursion. For instance, the Y-combinator in lambda calculus provides a fixed-point combinator $Y$ such that for any function $W$, $Y(W)$ is a term satisfying $Y(W) = W(Y(W))$. This yields recursive definitions (like the factorial function) as solutions to self-referential equations.This article develops a fully formal framework for recursive fixed points – fixed points obtained via an iterative or recursive process. We focus on the convergence of a sequence (possibly transfinite) of transformations to a self-consistent state. Intuitively, we start with an initial approximation and repeatedly apply a transformation $\phi$; if this process approaches a stable state that no longer changes under $\phi$, we have reached a fixed point. Formally, one may consider an iterative sequence $x_0, x_1 = \phi(x_0), x_2 = \phi(x_1), \dots$ and seek a limit $x_{\infty}$ such that $\phi(x_{\infty}) = x_{\infty}$. Such a limit, if it exists, is a recursive fixed point – the result of infinitely (or transfinitely) many applications of $\phi$. This idea can be generalized beyond simple sequences, using the machinery of ordinal-indexed recursion and category theory to rigorously construct $\phi^\infty$, the outcome of transfinitely many iterations of $\phi$.Recent research by Alpay (2025) introduced Alpay Algebra, a category-theoretic framework where transfinite recursive fixed points play a central role. In this framework, an endofunctor $\phi$ (an operator on objects in a category) can be iterated through ordinal numbers to yield a stable initial fixed point denoted $\phi^{\infty}$. The existence of $\phi^{\infty}$ under broad conditions and its universal properties have been proven with mathematical rigor. The fixed point $\phi^{\infty}$ is recursive in that it is obtained as the limit of an ordinal-indexed chain of iterative approximants (often called the initial chain). Notably, this $\phi^{\infty}$ is not just any solution to $X \cong \phi(X)$; it is the smallest or initial solution, meaning it is generated by the recursive process itself and any other fixed point admits a unique morphism from $\phi^{\infty}$. In other words, $\phi^{\infty}$ encapsulates the “ultimate outcome” of the transformation $\phi$ applied repeatedly without end – a self-consistent structure that remains invariant under $\phi$.This manuscript provides a formal exposition of recursive fixed points. We begin by establishing the mathematical preliminaries (category-theoretic foundations and definitions of transfinite iteration). We then prove the existence and uniqueness of the transfinite fixed point $\phi^{\infty}$ under appropriate conditions, drawing on recent developments in Alpay Algebra. We illustrate these concepts with examples ranging from classical structures (natural numbers, infinite streams) to logic (fixed-point semantics of recursive theories) and AI systems (iterative embedding alignment) to demonstrate the ubiquity of recursive fixed points in theory and practice. Throughout, we use a formal style with symbolic notation – emphasizing symbols over prose – to maximize precision and semantic weight. By the end, we will see that recursive fixed points not only exist, but in fact serve as universal invariants in many self-referential systems, providing a rigorous backbone for understanding phenomena like emergent consistency, identity of processes, and convergence of iterative algorithms.Preliminaries: Category-Theoretic FrameworkOur development uses the language of category theory to formalize recursive processes. We briefly summarize the needed notions (for a comprehensive background, see Mac Lane, 1971). We assume a category $\mathcal{A}$ with an initial object $\varnothing$ (an object with a unique morphism from it to any other object). An endofunctor $\phi: \mathcal{A} \to \mathcal{A}$ is an operator that maps objects to objects and morphisms to morphisms within $\mathcal{A}$. Intuitively, $\phi$ represents one step of a generative or transformative process on the structures in $\mathcal{A}$. We are interested in objects $X$ that satisfy an isomorphism $X \cong \phi(X)$ – such objects are fixed points of the functor $\phi$ (also called $\phi$-algebras that are self-consistent).Transfinite Ordinals and Chains: To capture recursive (potentially infinite) iteration, we consider ordinal numbers $0, 1, 2, \dots, \omega, \omega+1, \dots$ which extend the natural numbers into the transfinite. An ordinal-indexed chain(or transfinite sequence) in $\mathcal{A}$ is a family of objects ${X_{\alpha}}{\alpha < \lambda}$ for some ordinal $\lambda$, together with morphisms connecting them, such that $X{0} = \varnothing$ (the initial object), and for each ordinal $\beta < \lambda$:Successor step: If $\beta = \alpha+1$ is a successor, then $X_{\beta} = \phi(X_{\alpha})$. In other words, each step applies the functor $\phi$ to the previous object.Limit step: If $\beta$ is a limit ordinal (zero is the minimal ordinal, any non-zero ordinal with no immediate predecessor is a limit), then $X_{\beta}$ is defined as the colimit (categorical limit of the diagram) of all earlier $X_{\alpha}$ for $\alpha < \beta$. Intuitively, at a limit stage, $X_{\beta}$ is the “union” or limit of the prior approximations $X_{0}, X_{1}, ..., X_{\alpha}, (\alpha<\beta)$.This process yields an initial chain:X0→ X1=ϕ(X0)→ X2=ϕ2(X0)→ ⋯→ Xω=colim{Xn:n<ω}→ Xω+1=ϕ(Xω)→ ⋯Each stage $X_{\alpha}$ is built “recursively” from the previous ones. We say $\phi$ is continuous (or $\kappa$-accessible) if it preserves colimits of chains of length $<\kappa$ for some regular cardinal $\kappa$ (for example, $\omega$-continuous means it preserves countable colimits). Under such conditions, one can show that the initial chain eventually reaches a stage where applying $\phi$ does not produce a new object. Formally, there exists some ordinal $\mu$ (often $\mu = \kappa$ or earlier) such that $X_{\mu} \cong X_{\mu+1} = \phi(X_{\mu})$. When this first occurs, $X_{\mu}$ is a fixed point of $\phi$. By construction, it is the minimal or initial fixed point, since it arose from the smallest starting object by iterative application of $\phi$. We denote this object as $\mu \phi$ or $\phi^{\infty}$ (Alpay’s notation). It is also called the initial $\phi$-algebra in category-theoretic terms.Definition: The recursive fixed point of $\phi$, denoted $\phi^{\infty}$, is the object (if it exists) at which the transfinite iterative chain stabilizes. Concretely, $\phi^{\infty}$ is an object such that $\phi(\phi^{\infty}) \cong \phi^{\infty}$ and for some ordinal $\mu$, $\phi^{\infty} = X_{\mu}$ with $X_{\mu} \cong \phi(X_{\mu})$, where ${X_{\alpha}}$ is the initial chain defined above.Because $\phi^{\infty}$ arises by iterating $\phi$ starting from the smallest object, it intuitively represents the “limit of applying $\phi$ forever.” This aligns with the idea of a recursive process converging to a fixed point. The existence of $\phi^{\infty}$ is not automatic in every category or for every functor $\phi$; it typically requires conditions like completeness of the category or continuity of $\phi$ as mentioned. The Alpay Algebra framework explicitly assumes such conditions (e.g., working in well-behaved categories with transfinite colimits and $\phi$ preserving those colimits). In fact, Alpay Algebra I establishes that $\phi^{\infty}$ exists for every initial object under ZFC set theory assumptions without additional axioms. All proofs are carried out within standard category-theoretic foundations (following Mac Lane’s paradigm).Existence of the Recursive Fixed Point ($\phi^{\infty}$)We now state and prove (in outline) the Existence Theorem for recursive fixed points. This corresponds to the fixed-point existence results found in Alpay’s work and is analogous to the classical results (Knaster-Tarski, etc.) but in a transfinite categorical setting.Theorem 1 (Existence of $\phi^{\infty}$): Let $\phi: \mathcal{A} \to \mathcal{A}$ be an endofunctor on a category $\mathcal{A}$ that admits all colimits of chains of length up to some regular ordinal $\Lambda$, and assume $\phi$ preserves these colimits (i.e. $\phi$ is $\Lambda$-continuous). If $\mathcal{A}$ has an initial object $X_0$, then the initial chain $(X_{\alpha}){\alpha < \Lambda}$ defined by $X{0} = \varnothing$ and $X_{\alpha+1} = \phi(X_{\alpha})$ (with $X_{\lambda} = \mathrm{colim}{\alpha<\lambda} X{\alpha}$ for limit ordinals $\lambda < \Lambda$) will converge to a fixed point. In other words, there exists some ordinal $\mu < \Lambda$ such that $X_{\mu} \cong \phi(X_{\mu})$. This object $X_{\mu}$ is the recursive fixed point $\phi^{\infty}$. Moreover, $\phi^{\infty}$ is an initial algebra for $\phi$: the unique $\phi$-algebra generated by this transfinite iteration.Proof Sketch: Because $\Lambda$ is regular and $\phi$ preserves colimits of chains of length $<\Lambda$, the chain cannot continue to produce strictly larger (non-isomorphic) objects at every stage without end; if it did, one could take the colimit at stage $\Lambda$ (contradicting regularity or continuity). Thus there must be some stage where stabilization occurs. Formally, consider the sequence of inclusions (morphisms) $X_0 \to X_1 \to X_2 \to \cdots$. Either this sequence continues strictly (no stabilization) for all ordinals $<\Lambda$, or else there is a stage $\mu$ where $X_{\mu} \to X_{\mu+1}$ is an isomorphism. The former scenario is ruled out by a cardinality/cumulativity argument: if no stabilization occurs before $\Lambda$, then $X_{\Lambda} = \mathrm{colim}{\alpha<\Lambda} X{\alpha}$ is a fixed point of $\phi$ at stage $\Lambda$, because $\phi(X_{\Lambda}) = \phi(\mathrm{colim}{\alpha<\Lambda} X{\alpha}) \cong \mathrm{colim}{\alpha<\Lambda} \phi(X{\alpha}) = \mathrm{colim}{\alpha<\Lambda} X{\alpha+1} = \mathrm{colim}{\alpha<\Lambda} X{\alpha} = X_{\Lambda}$ (using continuity of $\phi$). Thus $X_{\Lambda}$ itself would be a fixed point, effectively $X_{\Lambda} \cong \phi(X_{\Lambda})$, achieving stabilization at $\Lambda`. In either case, we obtain some least ordinal $\mu$ (possibly $\mu=\Lambda$ if no earlier stage) such that $X_{\mu} \cong \phi(X_{\mu})$. Define $\phi^{\infty} := X_{\mu}$. By construction, $\phi^{\infty}$ satisfies $\phi(\phi^{\infty}) \cong \phi^{\infty}$. Furthermore, for any $\phi$-algebra $(X,\alpha: \phi(X)\to X)$ (any other fixed structure), we have by initiality of the chain that there is a unique homomorphism from each $X_{\alpha}$ into $X$ commuting with the $\phi$-action; at the limit, this yields a homomorphism $h: \phi^{\infty} \to X$. Thus $\phi^{\infty}$ is the initial object among all solutions of $X \cong \phi(X)$. ∎This theorem formalizes the existence of a transfinitely attained fixed point. In plainer terms, if one keeps applying $\phi$ starting from the simplest object, eventually (perhaps after an infinite number of steps) one stops getting new structures and hits a self-consistent one. That endpoint is $\phi^{\infty}$. All the intermediate steps $X_0 \to X_1 \to \cdots \to X_{\mu}=\phi^{\infty}$ are essentially building up a solution to the equation $X = \phi(X)$ piece by piece (like successive approximations). The condition of $\phi$ preserving colimits ensures that no information is lost in the limit process and that $\phi^{\infty}$ truly is a fixed point.In the context of Alpay Algebra (a formal system introduced by Faruk Alpay), Theorem 1 is a central pillar: it guarantees that for the self-referential processes defined in that framework, a stable identity emerges as a fixed point. Specifically, Alpay Algebra treats $\phi^\infty$ as representing the intrinsic identity of a generative process, since it is the unique invariant state that the process converges to. The existence theorem above matches statements in Alpay’s work such as: “We prove that the fixed point $\phi^\infty$ exists for every initial object ... and [that] $\phi$-iterates converge under regular cardinals”. The iterative construction of $\phi^\infty$ is sometimes called an ordinal-indexed fold or transfinite induction on the functor.It is worth noting that this categorical result generalizes classical fixed-point constructions. For example, in domain theory (a branch of theoretical computer science and math), a special case of this theorem states that any continuous endofunction on a complete partial order has a least fixed point (by taking the $\omega$-chain of iterates starting from the bottom element). That is essentially the $\omega$-continuous case of the above, corresponding to Kleene’s Fixed-Point Theorem for monotone operators on CPOs (which is itself an instance of Tarski’s theorem for lattices). Our transfinite approach extends this idea: even if $\omega$ steps are not enough, one allows transfinite steps until convergence. The result is a powerful guarantee: if the process can keep going without inconsistency, it will find a fixed point. In practical terms, this means any self-referential or recursive definition, under broad conditions, “bottoms out” at a well-defined semantics or structure that does not further change under the defining transformation.Uniqueness and Universal PropertyHaving established existence, we examine the uniqueness and universal property of the recursive fixed point $\phi^{\infty}$. Uniqueness here means $\phi^{\infty}$ is essentially the only fixed point that can be obtained through the recursive construction – if there were another built in the it would be to $\phi^{\infty}$. $\phi^{\infty}$ is the smallest fixed point, and every other fixed point of $\phi$ out” of $\phi^{\infty}$ in a unique and In the of Theorem 1, the recursive fixed point $\phi^{\infty}$ is unique up to isomorphism. Moreover, $\phi^{\infty}$ has the initiality for any object $X$ with an isomorphism \cong \phi(X)$ (i.e. any other fixed point of there exists a unique morphism \phi^{\infty} \to (a the appropriate In any other fixed-point object $X$ admits a unique from $\phi^{\infty}$, which is an isomorphism if $X$ is also obtained via a iterative Sketch: Uniqueness up to isomorphism is a standard category-theoretic argument: if and are initial $\phi$-algebras fixed then by initiality of there is a unique homomorphism I \to and by initiality of a unique homomorphism \to The I \to must the identity on (by uniqueness of the on and = Thus and are \cong This any solutions of the transfinite recursion are we can of the $\phi^{\infty}$ up to the universal any other fixed point we can $X$ with a $\phi$-algebra structure and to Specifically, \to can serve as the structure on \cong is there is a unique $\phi$-algebra homomorphism \phi^{\infty} \to such that = Intuitively, maps the fixed into any fixed structure $X$ in the only with $\phi$. If $X$ itself built by a iterative limit process (e.g., another chain that also a fixed then will be an isomorphism $\phi^{\infty}$, cannot into a end up the and formal terms, there is only one smallest self-consistent structure generated by $\phi$, and any other self-consistent structure a from this smallest one. This $\phi^{\infty}$ the universal fixed point or the identity of the process $\phi$. other solution of $X \cong \phi(X)$ through $\phi^{\infty}$ in a unique The morphism \phi^{\infty} \to can be seen as the or the fixed point $\phi^{\infty}$ into the fixed point If $X$ is not not be or but it exists and is universal property that $\phi^{\infty}$ the of all of the recursive process. In Alpay’s terms, $\phi^{\infty}$ as the of the a fixed point that every other fixed point in a This is analogous to the least fixed point in a lattice is in (or maps every other fixed point in that of Recursive Fixed illustrate the theory with recursive fixed points in various the functor = 1 on the category is a $\phi$-algebra is \to which provides a point (the of the and a function \to (the on the $X$ $X \cong 1 in yields the result that $X$ must be a infinite set to the natural numbers (with the point corresponding to and the function corresponding to the starting from the initial object and iterating $\phi$: $X_0 = = 1 \cong (a = 1 1 \cong = 1 \cong ... one \cong and the colimit as \to is \cong $\omega$ we have \cong 1 has a point and the is to is a fixed point of $\phi$. This is $\phi^{\infty}$ in this case – the recursive fixed point representing the defined natural number It is the smallest solution of $X = and any other of has a unique embedding from Let = for some fixed set $\phi$-algebra is \to which is like an on $X \cong in yields no solution the (if is there is no $X$ satisfying = if we infinite the equation $X \cong is by an infinite set of satisfying = In fact, the for this functor is to the set of all infinite over with the initial algebra solution in a complete category of infinite would the solution – in this case, there a solution in the because keeps if we work in a category of or consider partial one can obtain an initial solution representing but This that some functor yield infinite structures as fixed and the transfinite construction would a fixed point only in the limit the $\omega$-chain yields a of length which is The theory of with fixed points (like focus on initial fixed points yields defined structures (like In either case, the idea of a structure a fixed point of a functor is and Fixed In logic and the meaning of a set of recursive (a for is by the least fixed point of an operator on of (the immediate denoted for For a new from a set of assumptions starting from the set and iterating one approaches a limit where applying yields no new This limit is a fixed = By construction it is the least of the and complete the In categorical of = as an operator on the lattice of is and the theorem guarantees a least fixed point. The iterative in (the etc.) is building the chain = = and which satisfies = This is the recursive fixed point. by theory one is the one to – the of a fixed point of the This semantic convergence to a fixed point the of recursive the theory is a point where the process of stabilizes. It is also a case where transfinite steps are not needed $\omega$ or even steps if the theory is but one could consider transfinite for infinitely recursive in work by and Alpay a in language where a (the can an of semantic a process $\phi$ that represents $\phi$ an and or (like to semantic By applying $\phi$ to a piece of step it that the meaning converges to a stable of the In other words, if is a and then = it and as \to = approaches a fixed point where applying $\phi$ changes This is a a fixed point of the The $\phi^{\infty}$ (using the notation for the operator applied transfinitely many to denote the endpoint of this process. that a can recursive semantic and under infinite recursive the generative process converges to a fixed-point of $\phi^{\infty}$ here represents a semantic invariant of the – the meaning that remains after all self-referential is The existence of this fixed point and as a to by of This is a practical of a recursive fixed point in the transformation $\phi$ (a symbolic on or can be repeatedly applied to eventually yield a that $\phi$ Notably, the convergence to a fixed point provides guarantees of semantic in AI via Fixed In Alpay Algebra and Alpay a scenario where an AI and a until as a transfinite fixed-point The an state of a and the as an The transformation $\phi$ the AI its understanding on the and the (or in in a prove that by iterating this a functor on the state the system converges to a unique fixed a state where the of the is stable and the This fixed point is an essentially the understanding of the that change further Formally, if $\phi$ encapsulates one of for the is the limit of infinite a that satisfies = The show this convergence is and unique under category-theoretic conditions. This is a application of recursive fixed it provides a rigorous for AI by it as a fixed point in the semantic state of the The fixed point here an invariant meaning that the AI and the In terms, this at AI systems identity is a fixed point of – connecting to from theoretical computer science and that an identity could be defined as a stable fixed point of its self-referential from classical mathematics and AI demonstrate the of recursive fixed points. it is the of the natural number the semantics of a or the stable of an the is the a process that itself eventually reaches a point of that point, we have a fixed point that encapsulates the is to the of the fixed-point In the fixed point reached in $\omega$ steps iteration). In one a transfinite sequence of if the process is but the theory guarantees existence by transfinite The transfinite approach is a powerful – it even if a process as as each stage is built in a there is a fixed point at some ordinal work has even theory with transfinite fixed points Algebra to Banach’s contraction to transfinite In that a of an AI is to have an that is essentially a fixed point of a found via transfinite By Banach’s theorem to transfinite ordinal convergence to a unique semantic which is a recursive fixed point in a have a formal of recursive fixed emphasizing a rigorous By category theory and transfinite we an operator $\phi$ can a unique fixed point $\phi^{\infty}$ reached by an infinite recursive process. This fixed point exists under broad conditions or of and as a universal invariant for the process by $\phi$. We that $\phi^{\infty}$ is the smallest solution to $X = \phi(X)$ and that every other solution through its universal Our examples from mathematics numbers as fixed point, as fixed logic fixed point semantics of recursive and (iterative and semantic to stable In each case, the idea of a self-consistent fixed point of a recursive transformation provides and a on the of recursive fixed points and continuous processes. It a a system can be in of or self-referential one for the fixed point that represents the identity or Alpay’s recent further to that even an identity or a state can be as such a fixed point of its This a within formal mathematics – it that by the chain of transformations and one ensures the existence of a fixed point that encapsulates In practical terms, if every step of or transformation preserves or meaning without then as one iterates one approaches a state that cannot be further That state is the recursive fixed the point that and remains by its defining recursive fixed points are not just are the backbone of in self-referential By them, we that symbolic chains – as as are in a – will into a of This ensures that of symbols can be every is for in the limit, an fixed The mathematical here this in but the is through an recursive process, meaning and structure converge to an invariant fixed point, a on which further can Alpay Universal Alpay Algebra as Fixed-Point in and the of the in Alpay Algebra and the Fixed-Point of Alpay Algebra and Fixed-Point Lane, for the theorem and its of
The recent machine learning requires huge machine resources and is often hard for users with limited resources. Although there are DPT, these are unsuitable for a situation where a trained model should be unrevealed from other users. In this paper, we first propose a new learning method, aggregated zero-knowledge deep learning (AZKDL), whereby even a user with a limited resource contributes to the learning process without revealing its model. Our main idea is to utilize aggregated zero-knowledge proofs where individual zero-knowledge proofs are aggregated into a single proof. Loosely speaking, users generate proofs for their training of parts of models and then aggregate both the models and the proofs to verify the entire models without revealing them. We also prove that AZKDL can detect malicious training. When we conduct experiments to evaluate AZKDL, we identify that even a client with the largest model parameters can finish the computation within a second. Furthermore, we propose the distributed proof-of-deep-learning (DPoDL) that rewards users who contribute to the learning process by applying AZKDL to a mining process of blockchains. DPoDL can detect malicious users by AZKDL.
Efficiently verifying mathematical proofs and computations has been a heavily researched topic within Computer Science. Particularly, even repetitive steps within a proof become much more complex and inefficient to validate as proof sizes grow. To solve this problem, we suggest viewing it through the lens of Incrementally Verifiable Computation (IVC). However, many IVC methods, including the state-of-the-art Nova recursive SNARKs, require proofs to be linear and for each proof step to be identical. This paper proposes Lova, a novel framework to verify mathematical proofs end-to-end that solves these problems. Particularly, our approach achieves a few novelties alongside the first-of-its-kind implementation of Nova: (i) an innovative proof splicing mechanism to generate independent proof sequences, (ii) a system of linear algorithms to verify a variety of mathematical logic rules, and (iii) a novel multiplexing circuit allowing non-homogeneous proof sequences to be verified together in a single Nova proof. The resulting Lova pipeline has linear prover time, constant verifying capability, dynamic/easy modification, and optional zero-knowledge privacy to efficiently validate mathematical proofs. We offer potential use cases for Lova to secure entire Cyber-Physical Systems (CPS) pipelines, as well as localized CPS systems in automotive and healthcare devices. Code is available at https://github.com/noelkelias/lova.
Theorem proving serves as a major testbed for evaluating complex reasoning abilities in large language models (LLMs). However, traditional automated theorem proving (ATP) approaches rely heavily on formal proof systems that poorly align with LLMs' strength derived from informal, natural language knowledge acquired during pre-training. In this work, we propose DeepTheorem, a comprehensive informal theorem-proving framework exploiting natural language to enhance LLM mathematical reasoning. DeepTheorem includes a large-scale benchmark dataset consisting of 121K high-quality IMO-level informal theorems and proofs spanning diverse mathematical domains, rigorously annotated for correctness, difficulty, and topic categories, accompanied by systematically constructed verifiable theorem variants. We devise a novel reinforcement learning strategy (RL-Zero) explicitly tailored to informal theorem proving, leveraging the verified theorem variants to incentivize robust mathematical inference. Additionally, we propose comprehensive outcome and process evaluation metrics examining proof correctness and the quality of reasoning steps. Extensive experimental analyses demonstrate DeepTheorem significantly improves LLM theorem-proving performance compared to existing datasets and supervised fine-tuning protocols, achieving state-of-the-art accuracy and reasoning quality. Our findings highlight DeepTheorem's potential to fundamentally advance automated informal theorem proving and mathematical exploration.
Type systems are routinely employed in many modern programming languages to statically ensure various notions of runtime safety. We explore issues of typability and notions of safety in two different fields: Firstly, we focus on process calculi with composite channel names, where the type of a channel must somehow be derived from the types of its constituents. This collection of results includes a simple type system for the -calculus, along with some results of expressivity w.r.t. the -calculus; a generic type system for the Higher-Order Ψ-calculus, extending a similar type system for the ‘first-order’ Ψ-calculus; and a simple type system for , which aims to highlight a connexion to type structures from class-based/object-oriented languages. Secondly, we focus on the language TinySol, which models core features of the smart-contract language Solidity. Smart contracts are immutable programs with publicly visible code, that run atop a blockchain and are used to manage financial assets of users. Guided by insights from our work in process calculi, we develop type systems for ensuring three different properties: non-interference, call-integrity, and absence of out-of-gas exceptions. Lastly, we seek to tackle some of the shortcomings of the conventional, syntactic approach to type soundness, which had become evident in our previous developments. In particular, we study a peculiar construct in Solidity, known as the fallback function, which is untypable by syntactic type rules. Hence, we turn to a semantic approach to type soundness which allows type safety to be shown, even in cases where well-typedness cannot be proved by ordinary syntactic type rules. We use this approach to propose a method by which type safety may be recovered, even for contracts containing fallback functions, by allowing the programmer to supply a manual proof of type-safety for untypable pieces of code. This method does not depend on specific features of the fallback function, or even of TinySol or Solidity, and it may therefore also be developed for other smart-contract languages.
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.
Zero Knowledge (ZK) proofs are protocols with growing applications in fields such as cryptography. They can be particularly difficult to design and thus have multiple domain-specific languages (DSLs) to aid a programmer in their construction. Analysis methods for these protocols are then typically language-specific, greatly limiting their utility. Most languages compile user code into a midpoint polynomial-circuit called a rank one constraint system (R1CS). We provide tools to analyse these R1CS circuits which hence have much broader applicability than existing tools. Specifically, we design and implement a tool for equivalence up to renaming and scaling, useful to avoid repeating a laborious step of the ZK process. As implemented, the tool can handle circuits on the order of millions of constraints. Additionally, we provide methods to extract a directed acyclic hierarchical structure via clustering to guide an automated property prover with recursive proving. Such a structure typically exists in DSL code but is lost when compiled to R1CS and is required to make larger circuits feasible to pass to a property prover. The guidance given by our clustering methods to the property prover Civer gave comparable results to the guidance of the original structure present in the code and finished in faster time.
Computer programs control vital infrastructure, safeguard national security, and process all financialtransactions, making their correctness and security paramount. Formal verification is a key tool for program trust and assurance. However, as the complexity of computer systems grows, the complexity of their properties does as well. While traditional verification has focused on proving safety, the same techniques do not extend to other properties of interest, such as liveness, correct execution, and cryptographic properties, like zero-knowledge security. While these properties are valuable in cloud computing, where execution is outsourced to untrusted third-party providers, they remain understudied. This dissertation presents new languages, proof systems, and techniques targeting the verifica-tion of programs and their executions. Domain-specific languages (DSLs) are key in this effort. By restricting program syntax to a mathematically well-understood subset, we prove important proper- ties. This dissertation introduces four new languages and proof systems: Ticl, a structural temporal logic for modularly proving complex liveness specifications for infinite, nondeterministic programs; Reef, a system for verifiable regular expression matching that keeps matched text confidential; Otti, a framework for proving correct execution of optimization problems like machine learning training; and Zippel, a language for implementing and automatically verifying properties of non-interactive zero-knowledge protocols. Each one of those works shows that, by carefully designing languages and proof systems for specificdomains, we can have both expressive languages, and practical verification of complex properties which were previously difficult, or impossible to prove. We demonstrate this through case studies in distributed systems, secure computation, and cryptographic protocols.
Succinct non-interactive zero-knowledge proofs (zk-SNARKs) are a powerful cryptographic primitive that allow a prover to convince a verifier of the truth of a statement without revealing any additional information. Due to the high computational cost associated with proof generation in existing zk-SNARKs, distributed zero-knowledge proving has emerged as a promising outsourcing approach, where the prover delegates heavy computation to multiple servers across different locations, as seen in systems like Siniel and zkSaaS. However, existing distributed zkSNARKs still rely on large prime fields, which increase computational overhead, and they often suffer from unavoidable network bandwidth bottlenecks. In this paper, we propose FDzkS, a flexible and efficient collaborative proving distributed protocol constructed using group signatures and binary fields. Our protocol allows the prover to delegate computation to multiple workers without revealing any part of the witness. Most importantly, compared with existing distributed zkSNARK schemes, FDzkS enables both the prover and the workers to perform their tasks almost entirely offline, and it avoids complex interactions among the workers. We benchmark FDzkS against the most advanced protocols such as Siniel, Eos, zkSaaS, and Pianist, covering both semi-honest and malicious worker settings. Experimental results show that under low bandwidth conditions (64 Mbps), FDzkS reduces total proving time by up to 300 under high bandwidth conditions (4 Gbps), it still achieves up to 200% improvement in efficiency.
Elizaveta Pertseva, Alex Ozdemir, Shankara Pailoor, Alp Bassa · 7 authors
Abstract This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different constants, are challenging for existing solvers due to their inability to exploit multimodular structure. To address this issue, our method partitions constraints by modulus and uses lifting and lowering techniques to share information across subsystems, supported by algebraic tools like weighted Gr bner bases. Our experiments show that the proposed method outperforms existing state-of-the-art solvers in verifying cryptographic implementations related to Montgomery arithmetic and zero-knowledge proofs.
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.
Weihan Li, Zongyang Zhang, Yanpei Guo, Sherman S. M. Chow · 5 authors
Zero-knowledge range proof (ZKRP) asserts that a committed integerVlies in a given range like$[{0, 2^{n}-1}]$without other leakages ofV. It is vital in various privacy-preserving systems. Moving forward, the quest for post-quantum security is still in its infancy; the proof size of state-of-the-art lattice-based ZKRP (Lyubashevsky et al., CCS 20 and Couteau et al., Eurocrypt 21) remains linear inn, directly impacting the long-term sustainability in applications such as immutable ledgers. Confronting this unresolved impasse, we propose SHARP-PQ,i.e., succinct hash-based arbitrary-range proof with post-quantum security. SHARP-PQ offers proof size poly-logarithmic ton, optimized batch proofs, and versatile (new) capabilities. Its success stems from the improved inner product argument and exploitation of homomorphism. Empirically, SHARP-PQ features at least$10\times $smaller proof size for multiple ranges over lattice-based ZKRPs while maintaining competitive prover and verifier times. SHARP-PQ also outperforms ZKRPs directly constructed from hash-based generic zero-knowledge proofs at most$10 \times $.
Cardano is a Proof-of-Stake cryptocurrency with a market capitalisation in the tens of billions of USD and a daily volume of hundreds of millions of USD. In this paper we reflect on applying formal methods, functional architecture and Haskell to building Cardano. We describe our strategy, projects, lessons learned, the challenges we face, and how we propose to meet them.
Bruno Farias, Rafael Menezes, Eddie B. de Lima Filho, Youcheng Sun · 5 authors
This paper introduces a tool for verifying Python programs, which, using type annotation and front-end processing, can harness the capabilities of a bounded model-checking (BMC) pipeline. It transforms an input program into an abstract syntax tree to infer and add type information. Then, it translates Python expressions and statements into an intermediate representation. Finally, it converts this description into formulae evaluated with satisfiability modulo theories (SMT) solvers. The proposed approach was realized with the efficient SMT-based bounded model checker (ESBMC), which resulted in a tool called ESBMC-Python, the first BMC-based Python-code verifier. Experimental results, with a test suite specifically developed for this purpose, showed its effectiveness, where successful and failed tests were correctly evaluated. Moreover, it found a real problem in the Ethereum Consensus Specification.
Treballs Finals de Grau de Matemàtiques, Facultat de Matemàtiques, Universitat de Barcelona, Any: 2024, Director: Bruno Mazorra i Luis Victor Dieulefait
Marco Stronati, Denis Firsov, Antonio Locascio, Benjamin Livshits
Plonkish is a popular circuit format for developing zero-knowledge proof systems that powers a number of major projects in the blockchain space, responsible for holding billions of dollars and processing millions of transactions per day. These projects, including zero-knowledge rollups, rely on highly hand-optimized circuits whose correctness comes at the cost of time-consuming testing and auditing. In this paper, we present Clap, the first Rust eDSL with a proof system agnostic circuit format, facilitating extensibility, automatic optimizations, and formal assurances for the resultant constraint system. Clap casts the problem of producing Plonkish constraint systems and their witness generators as a semantic-preserving compilation problem. Soundness and completeness of the transformation guarantees the absence of subtle bugs caused by under- or over-constraining. Our experimental evaluation shows that its automatic optimizations achieve better performance compared to manual circuit optimization. The optimizer can also be used to automatically derive custom gates from circuit descriptions.
Inner product arguments (IPA) are arguments of knowledge that two committed vectors satisfy an inner product relation. With the recursive proof technique by Bootle et al. 2016, the size of IPA proofs only grows logarithmically in the length of the vectors, without a trusted setup. The succinct proof makes IPAs well suited for blockchain applications. However, current IPA can only handle a vector with length a power of 2, which limits the application of the argument. One direct solution is to pad the vectors with zeros, which incurs additional overhead. We propose Springproofs, a new framework deriving IPAs from many existing IPA schemes. Springproofs are natively compatible with vectors of arbitrary length. With a novel recursive compression structure, Springproofs achieve the same proof size as the original IPA but with more efficient computation. In particular, we instantiate Springproofs with Bulletproofs and find the optimal recursive structure for the IPA. First, we experimentally show that Springproofs are almost twice as fast as Bulletproofs for range proof, when the vector length is slightly larger than a power of 2. Afterwards, we incorporate the Springproofs into Monero, a popular cryptocurrency supporting privacy in transactions, revealing that the Springproofs based Monero outperforms Bulletproofs based Monero both in generating and verifying transactions. Moreover, we apply the Springproofs to the general arithmetic circuit, including SHA256, Merkle tree, and typical statistics, the performances on which are better than the performances by using Bulletproofs. Interestingly, Springproofs increase the range of parameters on which the performance of Bulletproofs exceeds that of Groth16, meanwhile naturally inherit the advantages of Bulletproofs, e.g., without initial trusted setup, aggregation, and batch verification. As a result, Springproofs have many promising applications, including confidential transactions in cryptocurrency and privacy computing for specific arithmetic circuits in smart contracts.
Alexandr Kuznetsov, Alex Rusnak, Anton Yezhov, Dzianis Kanonik · 6 authors
Zero-knowledge proofs have emerged as a powerful tool for enhancing privacy and security in blockchain applications. However, the efficiency and scalability of proof systems remain a significant challenge, particularly in the context of Merkle tree inclusion proofs. Traditional proof aggregation techniques based on AND logic suffer from a high verification complexity and data communication overhead, limiting their practicality for large-scale applications. In this paper, we propose a novel proof aggregation approach based on OR logic, which enables the generation of compact and universally verifiable proofs for Merkle tree inclusion. By adapting and extending the concept of OR composition from Sigma protocols, we achieve a proof size that is independent of the number of leaves in the tree, and verification can be performed using any single valid leaf hash. This represents a significant improvement over AND aggregation, which requires the verifier to process all leaf hashes. We formally define the OR aggregation logic; describe the process of generating universal proofs; and provide a comparative analysis that demonstrates the advantages of our approach in terms of proof size, verification data, and universality. Furthermore, we discuss the potential of combining OR and AND aggregation logics to create complex acceptance functions, enabling the development of expressive and efficient proof systems for various blockchain applications. The proposed techniques have the potential to significantly enhance the scalability, efficiency, and flexibility of zero-knowledge proof systems, paving the way for more practical and adaptive solutions in large-scale blockchain ecosystems.
The recent MIP*=RE theorem of Ji, Natarajan, Vidick, Wright, and Yuen shows that the complexity class MIP* of multiprover proof systems with entangled provers contains all recursively enumerable languages. Prior work of Grilo, Slofstra, and Yuen [FOCS '19] further shows (via a technique called simulatable codes) that every language in MIP* has a perfect zero knowledge (PZK) MIP* protocol. The MIP*=RE theorem uses two-prover one-round proof systems, and hence such systems are complete for MIP*. However, the construction in Grilo, Slofstra, and Yuen uses six provers, and there is no obvious way to get perfect zero knowledge with two provers via simulatable codes. This leads to a natural question: are there two-prover PZK-MIP* protocols for all of MIP*? In this paper, we show that every language in MIP* has a two-prover one-round PZK-MIP* protocol, answering the question in the affirmative. For the proof, we use a new method based on a key consequence of the MIP*=RE theorem, which is that every MIP* protocol can be turned into a family of boolean constraint system (BCS) nonlocal games. This makes it possible to work with MIP* protocols as boolean constraint systems, and in particular allows us to use a variant of a construction due to Dwork, Feige, Kilian, Naor, and Safra [Crypto '92] which gives a classical MIP protocol for 3SAT with perfect zero knowledge. To show quantum soundness of this classical construction, we develop a toolkit for analyzing quantum soundness of reductions between BCS games, which we expect to be useful more broadly. This toolkit also applies to commuting operator strategies, and our argument shows that every language with a commuting operator BCS protocol has a two prover PZK commuting operator protocol.