LICITRA Technical Report Series, Report No. LICITRA-TR-2026-01, Version 0.2. This report documents LICITRA-MMR, an open-source ledger primitive that combines a Merkle Mountain Range (MMR) data structure with per-organization epoch anchoring, a versioned canonical JSON specification, and an atomic two-phase commit pipeline for cryptographic audit integrity in agentic AI systems. At a block size of 1,000 events, LICITRA-MMR produces inclusion proofs requiring 14 SHA-256 operations and verifies a full epoch chain of 1,000 epochs in under 1 ms. The system is a single-operator forensic integrity primitive providing no Byzantine fault tolerance, no distributed consensus, and no confidentiality guarantees. Part of the LICITRA Technical Report Series. Companion report: LICITRA-TR-2026-02 (LICITRA-SENTRY, DOI: 10.5281/zenodo.18843784).
Rong Fu, Jia Yee Tan, Ziyu Kong, Shuning Zhang · 8 authors
Zero-knowledge circuits enable privacy-preserving and scalable systems but are difficult to implement correctly due to the tight coupling between witness computation and circuit constraints. We present zkCraft, a practical framework that combines deterministic, R1CS-aware localization with proof-bearing search to detect semantic inconsistencies. zkCraft encodes candidate constraint edits into a single Row-Vortex polynomial and replaces repeated solver queries with a Violation IOP that certifies the existence of edits together with a succinct proof. Deterministic LLM-driven mutation templates bias exploration toward edge cases while preserving auditable algebraic verification. Evaluation on real Circom code shows that proof-bearing localization detects diverse under- and over-constrained faults with low false positives and reduces costly solver interaction. Our approach bridges formal verification and automated debugging, offering a scalable path for robust ZK circuit development.
Open access
2 source records
Physical Unclonable Functions (PUFs) and Hardware Security
Blockchain Technology has presented a tamperproof and secure structure that supports the modern digital environment. Among the many consensus blockchain systems, the Proof of Stake (PoS) has emerged as an extensively used protocol due to its lower energy consumption and high security. However, the staking mechanism and creation of the validator process are the main parts of the PoS network, and any flaw in these processes can cause financial loss and breach the system's security. Therefore, we use formal verification methods for the verification and validation of the staking mechanism. In this study, we presented a formal model of staking processes in a PoS-based system, emphasizing the verification of accurate signer, stake allocation, creation of a validator with an NFT minted, and update timeline. The CSP\# language is used to specify these processes, and Linear Temporal Logics (LTL) are used to define the properties against these specifications. To verify that the system satisfies the critical properties, like verification of an authentic signer, secure stake registration, and deadlock-free validator creation using the Process Analysis Toolkit (PAT) model checker, and ensure the system's liveness and safety. Our results describe the importance of formal verification in enhancing the Polygon Blockchain's integrity by ensuring the staking mechanism in the stake manager contract is secure and reliable.
Zero-Knowledge (ZK) proof systems are cryptographic protocols that can (with overwhelming probability) demonstrate that the pair $(X, W)$ is in a relation $R$ without revealing information about the private input $W$. This membership checking is captured by a complex arithmetic circuit: a set of polynomial equations over a finite field. ZK programming languages, like Noir, have been proposed to simplify the description of these circuits. A developer can write a Noir program using traditional high-level constructs that can be compiled into a lower-level ACIR (Abstract Circuit Intermediate Representation), which is essentially a high-level description of an arithmetic circuit. In this paper, we formalise some of the ACIR language using SMT-LIB and its extended theory of finite fields. We use this formalisation to create an open-source formal verifier for the Noir language using the SMT solver cvc5. Our verifier can be used to check whether Noir programs behave appropriately. For instance, it can be used to check whether a Noir program has been properly constrained, that is, the finite-field polynomial equations generated truly capture the intended relation. We evaluate our verifier over 4 distinct sets of Noir programs, demonstrating its practical applicability and identifying a hard-to-check constraint type that charts an improvement path for our verification framework.
Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, Emilio Tuosto
The companion paper proposes a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. The model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. A toolchain supports formal model validation, Solidity code generation (extensible to other smart contract languages), and automated test synthesis. Although targeting blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. The expressiveness and practicality of the approach are demonstrated through modelling and realising coordination patterns in smart contracts. This artifact accompanies our paper [Elvis Konjoh Selabi et al., 2026]. It provides a toolchain for generating smart contract code from EDAM (Extended Data-Aware Machines) specifications. The artifact includes the complete source code, a Docker image for easy deployment, pre-generated experiment data (generated code, automated tests, and mutation testing results), and reproduction scripts.
Abstract Program verification provides stronger guarantees of correctness than standard testing. The verification process takes a program as input and derives a mathematical formula. Proving that a program is correct then reduces to establishing that this derived formula is unsatisfiable. Traditionally, automated reasoning tools can be used to determine unsatisfiability automatically. Furthermore, modern solvers can also produce a proof of unsatisfiability. However, these techniques typically rely on the proof and the underlying code being publicly available, which may not be desirable for certain applications. This work shows how to address this problem. Our team initially developed a protocol for validating the unsatisfiability of Boolean formulas in privacy-preserving settings. Building on these initial results, we devised ZKSMT, a virtual machine for validating unsatisfiability results produced by SMT solvers in zero-knowledge settings. In this paper we describe the theoretical foundations of such virtual machines and demonstrate how they can be applied to the theories of uninterpreted functions and linear integer arithmetic, two of the most widely used theories in verification. We conclude by outlining how the full formal verification workflow can be adapted to operate in privacy-preserving settings.
The Hamiltonian cycle problem is a well-known NP-complete problem in graph theory. This problem relates to lots of practical problems such as designing very large scale integration (VLSI) and travel-ling salesman problem (TSP). Since it is NP-complete, there is no efficient algorithm to solve the Hamiltonian cycle problem, and hence, its solution is valuable. In this paper, we propose new physical zero-knowledge proof protocols for the Hamiltonian cycle problem, whereby an entity can prove its knowledge of a solution to another entity without leaking any information about the valuable solution. Our protocols are more efficient than the previous protocols. We also propose a physical zero-knowledge proof protocol for TSP, one of whose building blocks is a new representation of an integer commitment with a secure addition protocol.
Elvis Konjoh Selabi, Maurizio Murgia, António Ravara, Emilio Tuosto
We propose a formal approach for specifying and implementing decentralised coordination in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralised workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contract languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalise to other service-oriented and distributed architectures. We demonstrate the expressiveness and practicality of the approach by modelling and realising some coordination patterns in smart contracts.
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.
Open access
4 source records
cs.LO
Formal Methods in Verification
Physical Unclonable Functions (PUFs) and Hardware Security
Proof-of-Stake (PoS) consensus protocols commonly employ epochs as temporal abstractions to simplify validator accounting, reward distribution, and slashing enforcement. These designs assume clean and synchronized state transitions across epoch boundaries. In practice, distributed systems exhibit asynchronous execution, delayed finality, and implementation divergence.This paper introduces and analyzes <b><i>Validator Epoch Reset Collisions</i></b>, a class of temporal desynchronization vulnerabilities in which validator state resets, reward counters, slashing windows, or participation flags become inconsistently applied across epoch boundaries. We demonstrate how such collisions create exploitable enforcement gaps that can be leveraged to evade penalties, duplicate rewards, or bypass participation requirements—without violating protocol rules. We argue that epoch-based accounting introduces structural risks to economic security unless continuity-enforcing safeguards are applied.
GLYPH is a transparent verification layer for Ethereum for trustless on-chain verification of heterogeneous proof systems. It unifies upstream SNARK and STARK settlement through a single packed arity-8 sumcheck verifier over p = 2^128 - 159, while preserving upstream assumptions. The design centers on a universal adapter surface, UCIR compilation, and a chain-bound artifact interface for stateless verification. Benchmark evidence in the whitepaper reports 29.45k total transaction gas in recorded testnet receipts. This record includes the whitepaper and the formal proof appendix.
Sungmin Lee, Kichang Lee, Gyeongmin Han, JeongGil Ko
Many location-based services rely on a point-in-polygon test ( PiP ), checking whether a point or a trajectory lies inside a geographic zone. Since geometric operations are expensive in zero-knowledge proofs, privately performing the PiP test is challenging. In this paper, we answer the research questions of how different ways of encoding zones affect accuracy and proof cost by exploiting grid-based lookup tables under a fixed STARK execution model. Beyond a Boolean grid-based baseline that marks cells as in- or outside, we explore a distance-aware encoding approach that stores how far each cell is from a zone boundary and uses interpolation to reason within a cell. % Our experiments on real-world data demonstrate that the proposed distance-aware approach achieves higher accuracy on coarse grids with only a moderate verification overhead, making zone encoding the key lever for efficient zero-knowledge spatial checks. Our experiments on real-world data demonstrate that the proposed distance-aware approach achieves higher accuracy on coarse grids (max. % 60%p 60%p accuracy gain) with only a moderate verification overhead (approximately 1.4×), making zone encoding the key lever for efficient zero-knowledge spatial checks.
Arthur Ramos, Anjolina Grisi de Oliveira, Ruy de Queiroz, Tiago M. L. de Veras
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting systems using three classical proof techniques: the diamond property, Newmans lemma, and the Hindley-Rosen lemma. These are instantiated across six case studies including untyped lambda calculus, combinatory logic, term rewriting, simply typed lambda calculus, and STLC with products and sums. All theorems are fully mechanized with zero axioms or sorry statements. We provide complete proofs of de Bruijn substitution infrastructure and demonstrate strong normalization via logical relations. To our knowledge, this is the first comprehensive confluence and normalization framework for Lean 4.
In this paper, I prove that sublinear regret across the environment Class C requires six functional properties, that these properties are mutually independent, and that they compose into a directed informational chain closing back on itself — a six-link cycle whose final link is grounded in an explicit Doob martingale construction over cycles of play. All six properties are defined functionally — as conditions on the distributions a decision-maker induces over actions and canonical summaries — so the results are invariant under implementation and apply to any decision-making system that can be modelled within the class: a person, an institution, or a machine. Every theorem in this paper, without exception, is checked line by line in the Lean 4 proof assistant against Mathlib: the formalization (~12,700 lines) contains zero `sorry`, zero custom axioms, and zero opaque definitions. Class C is the union of all POMDPs satisfying at least one of six structural properties covering the fundamental qualitative dimensions of adaptive hardness: reward ambiguity (P1), absorbing traps (P2), local optima (P3), deterministic optimality (P4), constrained feasibility (P5), and nonstationarity (P6). * Part I (Necessity). I define six primitives X1–X6 as purely functional properties of decision rules: Objective Tracking, Cross-Context Safety Transfer, Global Attractor Exploration, Policy Simplification, Feasibility Projection, and Feedback Adaptation. For each, I construct an explicit environment in C and prove an unconditional Ω(T) regret lower bound for any decision-maker lacking that primitive.* Part II (Independence). For every ordered pair (i,j) with i≠j, I exhibit an explicit decision rule possessing Xj but lacking Xi that suffers Ω(T) regret on the matching environment. All thirty directed-pair results are shown to follow from one master theorem, verified on a single compound environment with full non-interference analysis.* Part III (Sequential Dependence). Necessity is domain-invariant — a structural failure is a structural failure no matter what "success" means to the decision-maker — which is why Parts I and II hold unconditionally. Sufficiency is not: what counts as success is supplied by the domain, not by the theorem, so a single closed-form sufficiency result covering every domain at once would have to either fix one arbitrary notion of success and stop being general, or say nothing of substance. Part III proves exactly what generalizes. I prove six Information Enhancement Theorems establishing that the six primitives compose into a directed information chain: possessing Xi strictly increases the mutual information available toward any goal variable at Xi+1's task. Each of the six links is established outright — a forward theorem, a reverse theorem, and a non-reversibility result — with the exact point where a domain's own definition of success enters the chain named explicitly, as an Implementation Obligation, rather than assumed away. The closing link, X6→X1, is grounded in an actual Doob martingale construction: given that the cycle-indexed posterior is a martingale, it converges almost surely to the truth across cycles — the precise sense in which the chain accumulates rather than resets. To this paper's knowledge, no prior formalization unifies this many independently-proven-necessary structural properties into a single machine-checked class with proven mutual independence across all of them. All mathematical work is provided in full transparency and independent verification is highly encouraged: the complete Lean formalization, with a passing build and every theorem cross-referenced to its exact identifier, is at github.com/M-Ismail-ZA/IsmailsPrimitives. For any feedback or collaboration, please contact me via the email address listed on the paper. Updated: 3 July 2026 (V6.1).
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.
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.
Andrea Esposito, Francesco Rossi, Marco Bernardo, Francesco Fabris · 5 authors
Algorand is a scalable and secure permissionless blockchain that achieves proof-of-stake consensus via cryptographic self-sortition and binary Byzantine agreement. In this paper we present a process algebraic model of the Algorand consensus protocol with the aim of enabling formal verification. Our model captures the behavior of participants in terms of the structured alternation of consensus steps toward a committee-based agreement. We validate the correctness of the protocol in the absence of adversaries and then extend our model to assess the influence of coordinated malicious nodes that can force the commit of an empty block instead of the proposed one. The adversarial scenario is analyzed through an equivalence-checking-based noninterference framework that we have implemented in the CADP verification toolkit. In addition to highlighting both the robustness and the limitations of the Algorand protocol under adversarial assumptions, this work illustrates the added value of using formal methods for the analysis of consensus algorithms within blockchains.
Meihua Xiao, Y. P. Xu, Yongtuo Zhang, Ke Yang · 6 authors
Smart contracts, as a critical application of blockchain technology, significantly enhance its programmability and scalability, offering broad application prospects. However, frequent security incidents have resulted in substantial economic losses and diminished user trust, making security issues a key challenge for further development. Since smart contracts cannot be modified after deployment, flaws in their design or implementation may lead to severe consequences. Therefore, rigorous pre-deployment verification of their correctness is particularly crucial. This paper explores the symmetry in control flows and state transitions of Solidity smart contracts and leverages this inherent structural symmetry to develop a normalized state transition model based on a finite state machine. The FSM model is subsequently formalized into a Promela model with the Spin model checker. By integrating manually defined Linear Temporal Logic formulas with those generated by Smart Pulse, the Promela model is formally verified in Spin to ensure the correctness and security of smart contracts. This approach establishes a systematic verification framework, providing effective support to enhance the reliability and security of smart contracts.
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.
We describe the design and implementation of MicroNova, a folding-based recursive argument for producing proofs of incremental computations of the form$y=F^{(\ell)}(x)$, where$F$is a possibly non-deterministic computation (encoded using a constraint system such as R1CS),$x$is the initial input,$y$is the output, and$\ell > 0$The proof of an$e$-step computation is produced step-by-step such that the proof size nor the time to verify it depends on$e$. The proof at the final iteration is then compressed, to achieve further succinctness in terms of proof size and verification time. Compared to prior folding-based arguments, a distinguishing aspect of MicroNova is the concrete efficiency of the verifier-even in a resource-constrained environment such as Ethereum's blockchain. In particular, the compressed proof consists of O(log N) group elements and it can be verified with O(log N) group scalar multiplications and two pairing operations, where$N$is the number of constraints for a single invocation of$F$MicroNova requires a universal trusted setup and can employ any existing setup material created for the popular KZG univariate polynomial commitment scheme. Finally, we implement and experimentally evaluate MicroNova. We find that MicroNova's proofs can be efficiently verified on the Ethereum blockchain with ≈2.2M gas. Furthermore, MicroNova's prover incurs minimal overheads atop its baseline Nova's prover.