Blockchain Papers

Jakub Kacper Szeląg, Aydin Abadi, Mohammad Naseri

Decentralization as a concept in computer science has existed for over half a century. Despite its fundamental role across domains such as security, distributed computing, artificial intelligence, cloud infrastructures, and Internet of Things (IoT) architectures, there remains no universally accepted definition of decentralization applicable across computer communication systems. This has become increasingly problematic with the emergence of decentralized AI and machine learning paradigms, including collaborative training, distributed inference, blockchain-based, and agentic AI, where decentralization is often treated as a core design objective. Meanwhile, existing approaches frequently conflate decentralization with related notions such as distribution of trust or specific implementation paradigms. Such ambiguity creates inconsistencies in system analysis, limits comparability between works, and weakens the rigor of formal reasoning surrounding communication architectures and protocol design. In this work, we define this research gap as the Decentralization Problem. We analyze the formal-semantic, epistemological, and pragmatic foundations of decentralization and introduce a graph-based ontology defining it as both relational and subject-specific property of computer communication systems. The framework formally distinguishes decentralization from distribution and supports evaluation through two novel metrics: Void Tolerance and Imperviousness. We also provide a browser-based implementation that enables automated classification and metric computation of arbitrary systems. Instantiations to federated learning and blockchain architectures show consistent, comparable assessments where existing definitions produce incomplete or contradictory conclusions, providing a domain-independent foundation for analysing decentralization across heterogeneous systems.

Joseph Tafese, Karthik Nukala, Hassen Saïdi, Natarajan Shankar · 6 authors

We present a case study on proof-driven software understanding of mature, security-critical infrastructure. While formal methods are traditionally applied during the design phase, we present our experience applying formal reasoning onto a mature industrial C++ codebase. We focus on a formal analysis of the core algorithm that implements the Stellar blockchain's SDEX order book. By combining large language models (LLMs), Prototype Verification System (PVS), and SeaHorn, we are able to prove core properties of the production codebase. Our approach also identified an inconsistency in documentation related to the reachability of an exception location. Most importantly, however, we produce artifacts that make it easy for code changes to be checked against established invariants. This work demonstrates how the strategic combination of theorem proving and model checking provides a path for delivering robust assurance to legacy systems.

Luigi Usai

Author: Luigi Usai ORCID: https://orcid.org/0009-0003-3001-717X Location: Quartucciu (CA), Italy Date: June 26, 2026 Target: Zenodo / arXiv (cs.AI, cs.CL, cs.LO) Abstract Large Context Models (LCMs) exhibit an inherent vulnerability known as semantic hallucination, which stems directly from conditional likelihood maximization within discrete vector spaces. Traditional mitigation strategies operate predominantly post-hoc, managing errors after the stochastically generated token sequence has already mutated. This paper extends the Universal Cognitive Hypergraph (UKH) framework by introducing a discrete Alexandrov topology over knowledge hypergraphs to constrain the space of admissible states prior to token decoding. Utilizing the Monadic Neuro-Symbolic Verification and Synthesis Architecture (MNSVSA), probabilistic generation paths are intercepted and structurally validated against W3C SHACL constraints and axiomatic assertions verified by the Lean 4 kernel coupled with automated SMT solvers. Our theoretical results demonstrate the mathematical elimination of categorical deviations while fully preserving the model's syntactic fluency. 1. Introduction and Mathematical Formulation of the Problem Autoregressive language models estimate the probability distribution of the next token $w_t$ conditioned on the preceding context $w_{<t}$: $$P(w_t \mid w_{<t}) = \text{softmax}(W_{\text{unembed}} \cdot h_t)$$ where $h_t \in \mathbb{R}^d$ represents the final hidden state extracted by the Transformer architecture. Because the $\text{softmax}$ function maps scores to an open probability distribution, it inherently assigns non-zero probabilities to regions of the semantic space that violate real-world axiomatic constraints. Consequently, hallucination is not an accidental software bug but a structural property of the model's underlying stochasticity. The UKH framework bypasses the limitations of passive document retrieval (RAG) by integrating a topological-symbolic constraint directly into the sampling phase (speculative decoding). This setup actively prevents the model from exploring probabilistic trajectories linked to logically inconsistent states. 2. UKH Framework Architecture for Semantic Security The universe of discourse is mapped onto a directed hypergraph and serialized using the JSON-LD format. Let $\mathcal{H} = (V, E)$ be a cognitive hypergraph, where $V$ is the set of strongly typed nodes (conceptual entities) and $E \subseteq \mathcal{P}(V) \setminus \{\emptyset\}$ is the set of hyperedges representing multi-argument logical-functional relationships. 2.1. Alexandrov Topological Space and SHACL Constraints To establish geometric-structural rigor within a discrete domain, the hypergraph space is endowed with an Alexandrov topology, where open sets are defined as sub-hypergraphs closed upwards relative to a logical preorder relation ($\le$). W3C Shapes Constraint Language (SHACL) rules function as topological closure operators: $$\text{cl}(E_c) \subseteq \mathcal{H}_{\text{valid}}$$ If a candidate hyperedge $E_c$, derived from the semantic translation of the tokens proposed by the LLM, violates a structural Shape (e.g., assigning a physical property inconsistent with the primitive type of the node), the closure operator identifies a contradiction within the topological space. It subsequently invalidates the generation path before token rendering occurs. 2.2. Axiomatic Verification and Type Checking via Lean 4 While SHACL rules govern the macro-structural coherence of the graphs, the MNSVSA architecture executes formal verification of micro-logical assertions. The process follows a strict protocol: The semantic fragment generated by the LLM is isolated inside a logical monad. MNSVSA translates the assertion into a formal type within the evaluation language of Lean 4. Leveraging the Curry-Howard Isomorphism, the logical consistency of the statement is reduced to a Type Checking problem. To avoid the computational burden of generating complex mathematical proofs from scratch at inference runtime, the architecture delegates constraint satisfiability to an automated SMT solver (Z3) tightly integrated into the Lean 4 runtime kernel. 3. The Coherence Entropy Filtering Mechanism To quantify and halt stochastic drift within extended contexts, the framework implements a JIT (Just-In-Time) gatekeeping metric based on the Jensen-Shannon Divergence ($D_{JS}$). Let $P_{\text{LLM}}$ be the probability distribution over the next tokens generated by the model, and let $Q_{\text{UKH}}$ be the ontological adherence distribution derived from the allowed transition frequencies within the hypergraph $\mathcal{H}$. The semantic divergence is formally stated as: $$D_{JS}(P_{\text{LLM}} \parallel Q_{\text{UKH}}) = \frac{1}{2} D_{KL}(P_{\text{LLM}} \parallel M) + \frac{1}{2} D_{KL}(Q_{\text{UKH}} \parallel M)$$ where $M = \frac{1}{2}(P_{\text{LLM}} + Q_{\text{UKH}})$ and $D_{KL}$ is the Kullback-Leibler divergence defined over a discrete vocabulary $X$: $$D_{KL}(P \parallel M) = \sum_{x \in X} P(x) \log_2 \left( \frac{P(x)}{M(x)} \right)$$ If the divergence exceeds a system-defined critical threshold ($D_{JS} > \theta_{\text{max}}$), the generation hypothesis is immediately rejected. 4. Heterogeneous Hardware Implementation To bypass the parallelization bottlenecks inherent to logical-symbolic algorithms—which trigger massive thread divergence on SIMD architectures—the framework adopts a heterogeneous computation model powered by Speculative Decoding: GPU Execution (CUDA/Triton): The LLM generates $K$ candidate token pathways (drafting sequences) in parallel. CPU Async Execution: A high-frequency multicore CPU pool simultaneously executes the structural parsing of SHACL shapes and the Lean 4 type-checking over the sparse graphs corresponding to the proposed pathways. Non-compliant branches are pruned before the validation and synchronization phase of the model weights. 5. Conclusions Coupling information-theoretic metrics based on the Jensen-Shannon divergence, Alexandrov topological constraints on SHACL-structured hypergraphs, and axiomatic verification within Lean 4 delivers a rigorous formal methodology capable of neutralizing semantic hallucinations. Shifting control from post-hoc output filtering to a priori state space restriction sets a new benchmark for safety in Neuro-Symbolic Artificial Intelligence. Versione Italiana Unificazione Neuro-Simbolica mediante Ipergrafi Cognitivi: Mitigazione Quantitativa delle Allucinazioni nei Large Context Models a Monte della Generazione Autore: Luigi Usai ORCID: https://orcid.org/0009-0003-3001-717X Luogo: Quartucciu (CA), Italy Data: 26 Giugno 2026 Target: Zenodo / arXiv (cs.AI, cs.CL, cs.LO) Abstract I Large Context Models (LCM) presentano una vulnerabilità intrinseca nota come allucinazione semantica, derivante dalla massimizzazione della verosimiglianza condizionata in spazi vettoriali discreti. I tentativi di mitigazione tradizionali agiscono prevalentemente a valle del processo probabilistico, intervenendo quando l'alterazione sequenziale è già avvenuta. Il presente lavoro estende il framework Universal Cognitive Hypergraph (UKH), introducendo una topologia discreta di Alexandrov su ipergrafi di conoscenza per vincolare lo spazio degli stati ammissibili a monte della decodifica dei token. Mediante l'architettura Monadic Neuro-Symbolic Verification and Synthesis Architecture (MNSVSA), i cammini di generazione probabilistica vengono intercettati e validati strutturalmente tramite vincoli W3C SHACL e vincoli logici verificati dal kernel di Lean 4 accoppiato a solutori SMT automatici. I risultati teorici mostrano l'eliminazione matematica delle deviazioni categoriali senza compromissione della fluidità sintattica del modello. 1. Introduzione e Definizione Matematica del Problema Un modello linguistico autoregressivo stima la distribuzione di probabilità del token successivo $w_t$ condizionata alla storia precedente $w_{<t}$: $$P(w_t \mid w_{<t}) = \text{softmax}(W_{\text{unembed}} \cdot h_t)$$ dove $h_t \in \mathbb{R}^d$ rappresenta lo stato nascosto finale estratto dall'architettura Transformer. Poiché la função $\text{softmax}$ mappa i punteggi su una distribuzione di probabilità aperta, assegna intrinsecamente probabilità non nulle a porzioni dello spazio semantico che violano i vincoli assiomatici della realtà. Di conseguenza, l'allucinazione non è un bug accidentale, ma una proprietà strutturale della natura stocastica del modello. Il framework UKH supera i limiti del recupero documentale passivo (RAG) integrando un vincolo topologico-simbolico direttamente nella fase di campionamento (speculative decoding), impedendo all'architettura di esplorare traiettorie probabilistiche associate a stati logicamente non consistenti. 2. Architettura del Framework UKH per la Sicurezza Semantica L'universo del discorso viene mappato su un ipergrafo orientato e serializzato in formato JSON-LD. Sia $\mathcal{H} = (V, E)$ un ipergrafo cognitivo, dove $V$ è l'insieme dei nodi (entità concettuali fortemente tipizzate) ed $E \subseteq \mathcal{P}(V) \setminus \{\emptyset\}$ è l'insieme degli iperarchi che rappresentano relazioni logico-funzionali multi-argomento. 2.1. Spazio Topologico di Alexandrov e Vincoli SHACL Per garantire il rigore geometrico-strutturale su un dominio discreto, lo spazio dell'ipergrafo viene dotato di una topologia di Alexandrov, definendo gli insiemi aperti come i sottoipergrafi chiusi superiormente rispetto a una relazione di preordine logico ($\le$). I vincoli W3C Shapes Constraint Language (SHACL) operano come operatori di chiusura topologica: $$\text{cl}(E_c) \subseteq \mathcal{H}_{\text{valid}}$$ Se un iperarco candidato $E_c$, generato dalla traduzione semantica dei token proposti dall'LLM, viola una Shape strutturale (es. assegnazione di una proprietà fisica inconsistente con il ti

Luigi Usai

Author: Luigi UsaiORCID: 0009-0003-3001-717XLocation: Quartucciu (CA), ItalyDate: June 26, 2026Target: Zenodo / arXiv (cs.AI, cs.CL, cs.LO) Abstract Large Context Models (LCMs) exhibit an inherent vulnerability known as semantic hallucination, arising from conditional likelihood maximization within discrete vector spaces. While the Universal Cognitive Hypergraph (UKH) framework was initially proposed as a theoretical model to constrain the space of admissible states prior to token decoding, this paper presents its first formal empirical and quantitative validation. We detail a software runtime implementation of the Monadic Neuro-Symbolic Verification and Synthesis Architecture (MNSVSA) using discrete Alexandrov topologies, W3C SHACL shapes as topological closure operators, and a Just-In-Time (JIT) Jensen-Shannon Divergence (DJSDJS) Coherence Entropy Filter. Through Monte Carlo simulations (N=150N=150 runs per configuration), we demonstrate that tightening the coherence threshold (θmax=0.05θmax=0.05) mathematically eliminates semantic hallucinations (reducing the rate from 36.7% to 0.0%) while preserving syntactic fluency. Crucially, by leveraging speculative decoding with parallel validation, we show that the processing latency remains identical to the unconstrained baseline (90.0 µs), bypassing the massive execution overhead (174.8 µs) of post-hoc verification. The complete open-source verification suite and interactive visualization dashboard accompany this publication. 1. Introduction and Problem Statement Autoregressive language models estimate the probability distribution of the next token wtwt conditioned on the preceding context w<tw<t: P(wt∣w<t)=softmax(Wunembed⋅ht)P(wt∣w<t)=softmax(Wunembed⋅ht) where ht∈Rdht∈Rd is the final hidden state of the Transformer. Because the softmaxsoftmax function assigns non-zero probabilities across the entire vocabulary, autoregressive generation naturally drifts into regions of the semantic space that violate axiomatic truth, resulting in hallucinations. The UKH framework mitigates this by introducing a priori symbolic constraints directly into the token sampling phase via speculative decoding. Rather than validating output sequences post-generation, candidate pathways are parsed and filtered prior to token rendering. 2. Experimental Validation Engine (UKH-Eval) To validate the theoretical claims of the UKH and MNSVSA frameworks, we developed UKH-Eval, a complete Python and JavaScript simulation engine that implements the mathematical and topological constraints described in the original work. 2.1. Discrete Alexandrov Topology The knowledge base of the universe of discourse is modeled as a directed hypergraph H=(V,E)H=(V,E). To enforce geometric-structural constraints, we endow the space with a discrete Alexandrov topology, where open sets are sub-hypergraphs closed upwards relative to a logical preorder relation (≤≤). Let the preorder relation be defined by a preorder index mapping: alexandrovPreorderIndex:V→NalexandrovPreorderIndex:V→N A subset of nodes U⊆VU⊆V is open if and only if: ∀x∈U,∀y∈V:(alexandrovPreorderIndex(x)≤alexandrovPreorderIndex(y))⟹y∈U∀x∈U,∀y∈V:(alexandrovPreorderIndex(x)≤alexandrovPreorderIndex(y))⟹y∈U If a candidate token proposes a node transition that violates this upward-closure property, the transition is marked as topologically invalid. 2.2. SHACL Constraints as Closure Operators W3C Shape Constraint Language (SHACL) rules govern the macro-structural properties of the generated hyperedges: cl(Ec)⊆Hvalidcl(Ec)⊆Hvalid If a proposed hyperedge EcEc violates target class properties, minimum/maximum node counts, or axiomatic validity flags, the closure operator fails, and the branch is pruned. 2.3. MNSVSA Micro-Logical Type Checking For micro-logical validation, assertions are encapsulated in a monadic container (LogicalMonad). Levering the Curry-Howard Isomorphism, consistency verification is reduced to a Type Checking and propositional satisfiability problem. The engine compiles the proposed semantic statement into a formal SymPy expression and checks its consistency against the background theory axioms: conjunction=Axioms∧Expressionconjunction=Axioms∧Expression If conjunctionconjunction is unsatisfiable (i.e. evaluates to False), a logical contradiction is detected and the path is rejected. 2.4. Coherence Entropy JIT Filtering At each generation step, the JIT filter computes the Jensen-Shannon Divergence (DJSDJS) between the stochastically proposed LLM distribution PLLMPLLM and the ontological adherence distribution QUKHQUKH: DJS(PLLM∥QUKH)=12DKL(PLLM∥M)+12DKL(QUKH∥M)DJS(PLLM∥QUKH)=21DKL(PLLM∥M)+21DKL(QUKH∥M) where M=12(PLLM+QUKH)M=21(PLLM+QUKH) and DKLDKL is the Kullback-Leibler divergence defined over vocabulary XX: DKL(P∥M)=∑x∈XP(x)log⁡2(P(x)M(x))DKL(P∥M)=∑x∈XP(x)log2(M(x)P(x)) If DJS>θmaxDJS>θmax, stochastically proposed drift tokens are pruned, and the probability distribution is projected onto the compliant space. 3. Software Architecture & File Manifest The open-source validation package is organized into modular components to ensure reproducibility and maintainability: text ukh-evaluator/ ├── ukh_engine.py # Core verification engine and classes ├── test_harness.py # Automated unit test suite ├── benchmark.py # Monte Carlo comparative simulation runner └── dashboard/ # Interactive web UI and visualization ├── index.html # UI structure ├── style.css # Sleek dark-mode styling ├── app.js # In-browser real-time simulation and canvas graph └── results.json # Compiled benchmark data 3.1. File Descriptions 1. ukh_engine.py The core engine containing: LogicalMonad: Implements monadic binding and SymPy-based SAT solving. CognitiveHypergraph: Models nodes, hyperedges, Alexandrov open sets, and validates SHACL shapes. CoherenceFilter: Contains static methods for DKLDKL and DJSDJS calculations. UKHSystemSimulator: Links all subcomponents and handles the JIT filtering during next-token generation. 2. test_harness.py The automated test suite. It uses unittest to verify: Upward closure calculations under the Alexandrov topology. SHACL shape violations. Monadic consistency solving under the Curry-Howard isomorphism. Divergence math calculations. Coherence Entropy Filter rejections. 3. benchmark.py The empirical execution suite. It implements a Monte Carlo simulation running 150 independent generation steps per architecture (Baseline, Post-Hoc, and UKH) and sweeps the threshold parameter θmaxθmax from 0.050.05 to 0.950.95. It evaluates hallucination rates, perplexity, and latency, saving the outputs to results.json. 4. dashboard/ An interactive web-based dashboard built with HTML5 Canvas and CSS. index.html: Layout for control sliders (θmaxθmax, KK, drift), live token sequences, and visualization cards. style.css: Sleek glassmorphism theme, glowing neon accents, and custom micro-animations. app.js: Connects to results.json, renders interactive force-directed nodes on the canvas, and runs the entire simulation locally in JavaScript. 4. Quantitative Results & Discussion The benchmark results compiled under Monte Carlo testing demonstrate the trade-offs between safety, fluency, and system latency: 4.1. Hallucination Rates vs. Threshold θθ The unconstrained baseline model suffers a hallucination rate of 36.7%. As the UKH JIT threshold θθ is tightened, safety guarantees scale: At θ≥0.50θ≥0.50, the filter is relaxed, and the model behaves like the baseline. At θ=0.10θ=0.10, the hallucination rate is reduced to 3.3%. At θ=0.05θ=0.05, the hallucination rate is successfully reduced to exactly 0.0%. 4.2. Latency Profiles and Speculative Efficiency Post-hoc validation (checking the sequence after generation and regenerating if unsafe) achieves a low hallucination rate (3.3%) but introduces a massive latency penalty (174.8 µs, a 94% overhead compared to the baseline's 90.0 µs). By contrast, the UKH framework utilizing parallel speculative drafting and asynchronous verification maintains a latency profile of 90.0 µs, matching the unconstrained baseline. 4.3. Syntactic Perplexity Tightening the symbolic constraints does not degrade fluency. The average perplexity remains stable (∼6.18∼6.18 for θ=0.05θ=0.05 vs ∼6.83∼6.83 for baseline), showing that restricting the space of admissible states prior to token decoding steers the model toward logical paths without harming syntactic structure. 5. Peer Review Assessment & Future Work This empirical validation verifies the internal consistency and theoretical correctness of the paper's claims. However, scaling this framework to production Large Language Models requires addressing three primary engineering areas: Semantic Translation Robustness: Building high-speed, deterministic parsers to map raw tokens to JSON-LD graphs in real-time without introducing new failure modes. Dynamic Knowledge Bases: Compiling massive, real-world ontologies into Alexandrov preorders dynamically as context windows expand. Hardware Accelerators: Developing specialized kernels (e.g., in Triton or CUDA) to execute SHACL checks and SAT solving directly on GPU cores alongside tensor multiplication. 6. Conclusion The implementation of the UKH and MNSVSA verification engine provides the first empirical proof that coupling discrete topological constraints, SHACL shapes, and monadic type checking can completely eliminate stochastically induced hallucinations. Shifting control from post-hoc output filtering to a priori state space restriction establishes a new, verified paradigm for safety in Neuro-Symbolic Artificial Intelligence.

Jeremy Avigad, Anat Ganor, Lior Goldberg, David Levit · 7 authors

StarkWare's S-two prover provides an efficient means for establishing, on blockchain, that a program written in the Cairo virtual machine language runs to completion. The latter claim is encoded by an algebraic intermediate representation (AIR) that captures the semantics of the Cairo language. The AIR asserts the existence of tables of values from a finite field satisfying certain algebraic constraints. A cryptographic interactive proof system, circle STARK, provides an efficiently-checked certificate that the AIR is satisfied. We describe our verification, using the Lean 4 proof assistant, that the AIR encoding is sound, which is to say, the satisfiability of the AIR implies the computational claim.

Ray Iskander

We present the first machine-checked correctness proof of the OpenZeppelin reentrancy-guard pattern against a Lean 4 state-machine model of production-deployed Solidity source. All thirteen theorems are machine-checked with zero sorry, zero user-introduced axioms, and an axiom footprint bounded by [propext] (a standard mathlib4 axiom), gated under continuous integration. Smart contract reentrancy has caused over US$500M in documented losses since 2016, with the DAO 2016 attack draining ~3.6M ETH and forcing the hard fork that split Ethereum. The OpenZeppelin ReentrancyGuard pattern is the de facto defense across production DeFi, yet no prior work has established its discriminating power: that the guard blocks attacks on vulnerable instances, preserves correct execution for non-attacking transactions, and distinguishes adjacent safe and vulnerable variants. Prior efforts formalized either guard correctness on toy contracts or attack feasibility on isolated instances - not both directions plus boundary cases against production source. We verify three production instantiations - DAO 2016, Compound v2, and Aave V3 flashLoan - plus a minimal-diff mutant of Aave V3's flashLoan (flashLoanVulnerable) isolating one security-critical difference, via mutation testing. The tridirectional structure pairs (a) attack reproduction of the DAO 2016 pattern, (b) a correctness proof for Compound v2, and (c) a boundary-case proof distinguishing Aave V3's CEI-correct flashLoan from the mutant. A capstone meta-theorem composes the three under a no-retrofit discipline, demonstrated at the first cross-protocol stress test (Compound v2 to Aave V3); broader-family portability is future work. Full Lean 4 source, CI config and reproduction commands are at https://github.com/rayiskander2406/qanary-contracts, reproducible at v1.6-phase7-closure (substrate: v1.3-layer6-closure).

Natalia Klaus, Juan Conejero, Palina Tolmach

We describe a verification pipeline that takes production Rust cryptographic code and produces machine-checked correctness proofs in Lean 4. The pipeline combines three components: symbolic extraction tools (Charon and Aeneas, or Hax) that lift Rust into Lean 4; formal cryptographic specification libraries (ArkLib and CompPoly, from the Verified zkEVM project) that provide the mathematical targets; and AI provers (Aristotle from Harmonic AI and Aleph from Logical Intelligence) that close the resulting proof obligations. Every proof is checked by the Lean kernel, so AI output cannot compromise soundness. Within the scope of the Ethereum Foundation's zkEVM Verification Project, we applied the pipeline to cryptographic primitives in Plonky3 (FRI folding, Mersenne31 and KoalaBear field arithmetic, Horner polynomial evaluation) and RISC Zero (Merkle inclusion verification). In addition, Aleph authored proofs of two bounds-style theorems in Plonky3's compute_log_arity_for_round that previously stood as sorry. The paper describes the architecture, walks through a running example based on Aleph's two proofs, reports which classes of proof obligations AI closed and which required manual work, and discusses the engineering gaps we encountered: Lean 4 toolchain drift across tools and specific Aeneas/Hax extraction limits. We also document concrete missing lemmas, tactic gaps, and code-generation friction points discovered during proof development. We hope this contribution lowers the barrier to adoption of formal verification and facilitates more effective use of AI in this pipeline. The result is a working pipeline for formal verification of Rust, with kernel-checked proofs and reproducible artefacts.

Wolfgang Grieskamp, Teng Zhang, Vineeth Kashyap, Jake Silverman

The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. Recently, Move on Aptos was extended with higher-order functions: imperative functions as first-class values that can be passed around, stored in data structs, and kept in persistent storage, enabling dynamic dispatch. This paper describes the representation of function values in the Move specification language and their implementation in MVP. We introduce behavioral predicates which characterize Move functions (aborts and pre/post conditions) by single-state or two-state predicates. We also introduce state labels for naming intermediate memory states in which expressions are evaluated and which allow to compose behavioral predicates to describe sequences of state transitions. On SMT level, function values are encoded by discriminating over the possible function values reaching a call site: when the concrete function is known, its effect is accounted for directly; when it is unknown (for example, a function parameter, or a closure loaded from storage), its behavioral predicates describe the effect. Our approach goes beyond, for example, Dafny, by supporting imperative first-class functions which can modify state via Rust-style references and global variables, and leads to more efficient SMT encodings than separation logic because of the static separation of memory enabled by Move. We further extend MVP's specification inference tool to work with function values: given arbitrary higher-order Move code, weakest-precondition analysis semi-automatically derives behavioral-predicate-based specifications, reducing the annotation burden and providing a validation pipeline for the new specification constructs.

Pascal Berrang, Mirco Giacobbe, Jacob Swales, Xiao Yang

We introduce a technology to formally verify that a software system satisfies a temporal specification of functional correctness, without revealing the system itself. Our method combines a deductive approach to model checking to obtain a formal certificate of correctness for the system, with zero-knowledge proofs to convince an external verifier that the system -- kept secret -- complies with its specification of correctness -- made public. We consider proof certificates represented as ranking functions, and introduce both an explicit-state and a symbolic scheme for model checking in zero knowledge. Our explicit-state scheme assumes systems represented as transition graphs. We use polynomial commitments to convince the verifier that the public proof certificates correspond to the secret transition relation. Our symbolic scheme assumes systems specified as linear guarded commands and uses piecewise-linear ranking functions. We apply Farkas' lemma to obtain a witness for the validity of the ranking function with public and secret components, and employ sigma protocols for matrix multiplication and range proofs to convince the verifier of the witness's existence. We built a prototype to demonstrate the practical efficacy of our two schemes on linear temporal logic verification examples. Our technology enables formal verification in domains where both the safety and the confidentiality of the system under analysis are critical.

Miguel Isabel, Enric Rodríguez-Carbonell, Clara Rodríguez-Núñez, Albert Rubio

Zero-knowledge proofs (ZKPs) are an emerging technology that has become the solution to efficiently provide security and privacy along with the transparency requirement of blockchains. ZKPs are usually expressed by means of arithmetic circuits and, more generally, systems of polynomial equations in a large prime field (commonly ranging from 64-bit to 256-bit values). An increasing interest to apply formal verification techniques to ensure soundness and completeness properties of ZKP protocols has shown the need of developing powerful SMT solvers able to handle such constraint systems. In this paper we consider the problem of deciding the satisfiability of existentially quantified first-order formulas defined over polynomial equations on a prime field. We present a new DPLL($T$)-based approach in which the theory solver orchestrates several modules with different trade-offs between completeness and efficiency. We have implemented the proposed techniques in a prototype that already shows better results than existing state-of-the-art tools on both benchmarks from the domain of ZKP compiler correctness and new benchmarks coming from the verification of arithmetic circuits for ZKPs. \keywords{SMT \and Finite field \and Polynomials \and Zero-Knowledge Proofs.

Massimo Bartoletti, Angelo Ferrando, E. Lipparini, Vadim Malvone

Smart contracts deployed on blockchains such as Ethereum routinely manage large amounts of assets, making their security critical. Empirical studies show that real-world attacks often exploit flaws in the business logic of contracts that unfold across multiple transactions, such as liquidity or front-running attacks. Detecting these attacks requires reasoning about expressive temporal properties beyond the capabilities of existing analysis tools. In this paper, we present an automated approach to the formal verification of smart contracts, enabling the specification and verification of complex temporal properties. Our approach provides a fully automated encoding into Lustre -- the specification language supported by the Kind 2 model checker -- of an expressive subset of Solidity contracts and temporal specifications based on first-order Hennessy-Milner Logic. This encoding allows us to leverage Kind 2 to determine whether the contract respects the specification or not. We implement our approach in a toolchain that integrates the translation and verification steps, and we evaluate its effectiveness and performance on a benchmark of smart contracts and temporal properties capturing complex attack scenarios. Our results show that the proposed approach can effectively verify non-trivial temporal properties of smart contracts and detect violations that are beyond the reach of existing analysis tools.

Hubert Garavel

LNT is a modern language for the formal description of concurrent systems. It generalizes traditional process calculi and overcomes their known limitations by incorporating features such as an imperative programming style with direct assignments to variables, symmetric sequential composition, and explicit loop operators. The present article examines how these features can be taken advantage of to obtain LNT models as concise and readable as possible. The study is illustrated with a running example, the consensus protocol of the Algorand blockchain, a formal model of which was recently developed at the University of Urbino. It is shown that, using well-chosen transformations, the number of lines of LNT code can be divided by three, while improving readability. Also, various properties of the formal model are expressed and verified using visual checking, equivalence checking, and model checking.

Jinwook Kim

Tokenized assets increasingly operate across heterogeneous blockchain networks and off-chain ledgers, where a regulatory action (a freeze, a seizure, a confiscation) must take effect atomically and consistently across every domain holding the asset. We mechanize, in Isabelle/HOL, cross-domain state preservation as a functor: state machines are objects, structure-preserving synchronization maps are morphisms, and the category laws (identity, composition, associativity) hold as theorems. On this base we establish four results. Safety: a regulatory transition on one domain is faithfully reflected across all connected domains, with bidirectional roundtrip preservation, N-domain consistency, per-asset isolation, and terminal states preserved. Liveness: under f = 3f+1 shown to make that assumption inhabitable rather than vacuous. Convergence: from an arbitrary unlocked configuration, with no initial cross-chain consistency assumed, synchronization reaches a valid state in a bounded number of steps along a terminal-faithful recovery path. Hierarchy: a tower of synchronization-degree functors connected by natural transformations closed under composition, with a genuinely one-directional degree monotonicity. We couple the functor to Lochbihler and Maric's authenticated data structure at the global-state level, instantiated on a recursive model of the Canton transaction tree with a declared consensus-scope limit. The synchronization model is atomic; its lift to a partially synchronous network is future work. The application is a regulatory state transition model distilled from the RCP framework (arXiv:2603.29278). All ten Isabelle/HOL theory files build without sorry or oops and are submitted to the Archive of Formal Proofs.

Murilo de Souza Neves, Adilson Luiz Bonifacio

Smart contracts are tools with self-execution capabilities that provide enhanced security compared to traditional contracts; however, their immutability makes post-deployment fault correction extremely complex, highlighting the need for a verification layer prior to this stage. Although formalisms such as Contract Language (CL) enable logical analyses, they prove limited in attributing responsibilities within complex multilateral scenarios. This work presents a proof of concept using the Relativized Contract Language (RCL) and the RECALL tool for the specification and verification of a purchase and sale contract involving multiple agents. The study demonstrates the tool's capability to detect normative conflicts during the modeling phase. After correcting logical inconsistencies, the contract was translated into Solidity and functionally validated within the Remix IDE environment, confirming that prior formal verification is fundamental to ensuring the reliability and security of the final code.

Sirui Shen, Zunchen Huang, Chenglu Jin

The modern integrated circuit ecosystem is increasingly reliant on third-party intellectual property integration, which introduces security risks, including hardware Trojans and security vulnerabilities. Addressing the resulting trust deadlock between IP vendors and system integrators without exposing proprietary designs requires novel privacy-preserving verification techniques. However, existing privacy-preserving hardware verification methods are all simulation-based and fail to offer formal guarantees. In this paper, we propose ZK-CEC, the first privacy-preserving framework for hardware formal verification. By combining formal verification and zero-knowledge proof (ZKP), ZK-CEC establishes a foundation for formally verifying IP correctness and security without compromising the confidentiality of the designs. We observe that existing zero-knowledge protocols for formal verification are designed to prove statements of public formulas. However, in a privacy-preserving verification context where the formula is secret, these protocols cannot prevent a malicious prover from forging the formula, thereby compromising the soundness of the verification. To address these gaps, we first propose a blueprint for proving the unsatisfiability of a secret design against a public constraint, which is widely applicable to proving properties in software, hardware, and cyber-physical systems. Based on the proposed blueprint, we construct ZK-CEC, which enables a prover to convince the verifier that a secret IP's functionality aligns perfectly with the public specification in zero knowledge, revealing only the length and width of the proof. We implement ZK-CEC and evaluate its performance across various circuits, including arithmetic units and cryptographic components. Experimental results show that ZK-CEC successfully verifies practical designs, such as the AES S-Box, within practical time limits.

Elizaveta Pertseva, Valentin Robert, Clark Barrett, James Parker

Efforts to verify Zero-Knowledge Proof circuit encodings have highlighted the challenge of proving the correctness of quantifier-free statements that make use of both bitvector and finite field operations. Existing verification workflows are either manual or rely on SMT solvers, which scale poorly on some classes of problems for reasons that include difficulties with conversion operators and challenges reasoning about inequalities. To address these limitations, we present a novel Lean tactic BitModEq that leverages range lemmas and case analysis to produce verified translations from finite fields to bitvectors. Our approach, combined with bit-blasting, outperforms state-of-the-art SMT solvers, solving 19% more ZKP arithmetization benchmarks.

Tranquilli, Julius, Gupta, Naman

Concentrated-liquidity automated market makers (CLAMMs), as exemplified by Uniswap v3, are now a common primitive in decentralized finance frameworks. Their design combines continuous trading on constant-function curves with discrete tick boundaries at which liquidity positions change and rounding effects accumulate. While there is a body of economic and game-theoretic analysis of CLAMMs, there is negligible work that treats Uniswap v3 at the level of formal state machines amenable to model checking or theorem proving. In this paper we propose a formal modeling approach for Uniswap v3-style CLAMMs using (i) networks of priced timed automata (PTA), and (ii) finite-state transducers (FST) over discrete ticks. Positions are treated as stateful objects that transition only when the pool price crosses the ticks that bound their active range. We show how to encode the piecewise constant-product invariant, fee-growth variables, and tick-crossing rules in a PTA suitable for tools such as UPPAAL, and how to derive a tick-level FST abstraction for specification in TLA+. We define an explicit tick-wise invariant for a discretized, single-tick CLAMM model and prove that it is preserved up to a tight additive rounding bound under fee-free swaps. This provides a formal justification for the "$ε$-slack" used in invariance properties and shows how rounding enters as a controlled perturbation. We then instantiate these models in TLA+ and use TLC to exhaustively check the resulting invariants on structurally faithful instances, including a three-tick concentrated-liquidity configuration and a bounded no-rounding-only-arbitrage property in a bidirectional single-tick model. We discuss how these constructions lift to the tick-wise structure of Uniswap v3 via virtual reserves, and how the resulting properties can be phrased as PTA/TLA+ invariants about cross-tick behaviour and rounding safety.

Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel, Ning Luo

Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-knowledge (ZK) protocols for PSPACE-complete statements by enabling ZK proofs of QBF (Quantified Boolean Formula) evaluation. The core idea is to validate quantified resolution proofs (Q-Res) in ZK. We develop an efficient polynomial encoding of Q-Res proofs, enabling proof validation through low-overhead arithmetic checks. We also design a ZK protocol to prove knowledge of a winning strategy related to the QBF, which is often equally important in practice. We implement our protocols and evaluate them on QBFEVAL. The results show that our protocols can verify 72% of QBF evaluations via Q-Res proof and 82% of instances' winning strategies within 100 seconds, for instances where such proofs or strategies can be obtained.

Evgeny Ukhanov

The proliferation of decentralized financial (DeFi) systems and smart contracts has underscored the critical need for software correctness. Bugs in such systems can lead to catastrophic financial losses. Formal verification offers a path to achieving mathematical certainty about software behavior. This paper presents the formal verification of the core logic for a token sale launchpad, implemented and proven correct using the Dafny programming language and verification system. We detail a compositional, bottom-up verification strategy, beginning with the proof of fundamental non-linear integer arithmetic properties, and building upon them to verify complex business logic, including asset conversion, time-based discounts, and capped-sale refund mechanics. The principal contributions are the formal proofs of critical safety and lifecycle properties. Most notably, we prove that refunds in a capped sale can never exceed the user's original deposit amount, and that the precision loss in round-trip financial calculations is strictly bounded. Furthermore, we verify the complete lifecycle logic, including user withdrawals under various sale mechanics and the correctness of post-sale token allocation, vesting, and claiming. This work serves as a comprehensive case study in applying rigorous verification techniques to build high-assurance financial software.

René Dávila, Everardo Bárcenas, Rocío Aldeco-Pérez

Formal verification entails testing software to ensure it operates as specified. Smart contracts are self-executing contracts with the terms of the agreement directly written into lines of code. They run on blockchain platforms and automatically enforce and execute the terms of an agreement when meeting predefined conditions. However, Smart Contracts, as software models, often contain notable errors in their operation or specifications. This observation prompts us to conduct a focused study examining related works published across various sources. These publications detail specifications, verification tools, and relevant experiments. Subsequently, this survey proposes an alternative formal verification based on description logic.

Chad E. Brown, Cezary Kaliszyk, Josef Urban

The fundamental building blocks of the Bitcoin lightning network are bidirectional payment channels. We describe an extension of payment channels in the Proofgold network which allow the two parties to bet on whether a proposition will be proven by a certain time. These provide the foundation for a Proofgold lightning network that would allow parties to request proofs (by betting there will be no proof by a certain time) and other parties to provide proofs (and be rewarded by betting there will be a proof). The bets may also provide a way to approximate the probability that a certain proposition is provable (in the given amount of time). We describe the implementation of payment channels supporting proofs in Proofgold and discuss a potential lightning network that could be built as a result. One application of such lightning network would be a large decentralized infrastructure for fast collaborative formalization projects.

Chad E. Brown, Cezary Kaliszyk, Josef Urban

Proofgold is a blockchain that supports formalized mathematics alongside standard cryptocurrency functionality. It incorporates logical constructs into the blockchain, including declarations of formal theories, definitions, propositions and proofs. It also supports placing and collecting bounties on proving these propositions, incentivizing the development of the formal libraries contained in Proofgold. In this paper, we present a web-based blockchain explorer for Proofgold. The system exposes not only the usual transactional data but also the formal mathematical components embedded in the chain and allows some interaction with them. The explorer allows users to inspect blocks, transactions, and addresses, as well as formal objects: theories, definitions, theorems and their proofs. We also support the submission of transactions to the blockchain using our interface. We describe the system architecture and its integration with the Proofgold Lava software, highlighting how the explorer supports navigation of formal content and facilitates mathematical knowledge management in a decentralized setting, as well as a number of formalizations in category theory done in the system.

Alessandro Coglio, Eric McCarthy

Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transformations to Yul code. To help ensure the correctness of these transformations and their sequencing, we used the ACL2 theorem prover to develop a formalization of the syntax and semantics of Yul, proofs relating static and dynamic semantics, a formalization of some Yul code transformations, and correctness proofs for these transformations.

Russell O'Connor, Andrew Poelstra

The modular inverse is an essential piece of computation required for elliptic curve operations used for digital signatures in Bitcoin and other applications. A novel approach to the extended Euclidean algorithm has been developed by Bernstein and Yang within the last few years and incorporated into the libsecp256k1 cryptographic library used by Bitcoin. However, novel algorithms introduce new risks of errors. To address this we have completed a computer verified proof of the correctness of (one of) libsecp256k1's modular inverse implementations with the Coq proof assistant using the Verifiable C's implementation of separation logic.