Guoqiang Li

Stateless UTXO-style execution validates transactions using local and referenced data, enabling parallel validation and predictable serialized-size/weight accounting. However, multi-step workflows must thread state across outputs, and a prepared next-step transaction may become stale when another valid spend confirms first. Explicit state threading therefore shifts consistency maintenance, off-chain tracking, and transaction rebuilding onto the protocol boundary, potentially increasing coordination cost and latency. Recursive invariants (RIs), our proposed transaction-level logic and toolchain, address this gap by expressing workflow rules as transaction-level predicates over a transaction's inputs and indexed successor positions referenced by the RI. Modeled this way, an accepted transaction that realizes such a successor position re-checks the predecessor's RI one step later, carrying the workflow rule forward without introducing application-level shared mutable state or executable logic attached to outputs. Accordingly, multi-step protocol rules preserve validation-time locality and admit explicit cost accounting, while cross-transaction guarantees arise from repeated one-step checking. Not all successor clauses are checkable when the current transaction is validated, so our small statically typed domain-specific language (DSL) uses three-valued semantics over true, false, unknown to defer future-dependent obligations until they become checkable. Co-designed with this DSL, our framework formalizes UTXO validation and ledger extension, identifies the validation-time-evaluable one-step fragment, and proves the deduction system sound with respect to the three-valued semantics. Here, we also give validation and ledger-extension algorithms corresponding to the formal model. On the systems side, we implement a prototype RI interpreter and benchmarking toolchain for the six reported workloads. With six practice-motivated case studies, the reported benchmark traces exhibit approximately linear cumulative validation-cost proxy growth, while illustrating staged workflow constraints without committing each step to a preconstructed successor transaction.

The optimization of Deep Neural Networks (DNNs) for resource-constrained environments through quantization and pruning necessitates efficient re-verification to ensure safety. However, existing incremental verification methods are primarily designed for numerical parameter perturbations and often struggle to handle the discrete structural changes introduced by network pruning. Moreover, traditional approaches verify each model variant from scratch, discarding the significant computational effort invested in the original model’s proof. In this paper, we present MUC-G4 , an incremental verification framework that accelerates the certification of compressed DNNs via search space pruning. Inspired by the principles of residual reasoning and conflict-driven learning , MUC-G4 identifies Minimal UNSAT Cores (MUCs) as robust proof artifacts that capture the local logical reasons for safety. Our work is grounded in the insight of Locality of Conflicts : the logical contradictions that guarantee safety are often independent of the redundant neurons and connections targeted by compression algorithms. MUC-G4 extracts these MUCs from the original network’s proof and utilizes them as a warm-start mechanism to identify and prune stable infeasible regions in the compressed network’s search space. Experimental results on the ACAS Xu and MNIST benchmarks demonstrate that safety proofs exhibit high structural resilience. Crucially, the framework maintains full completeness through a residual solving phase, ensuring that all newly exposed search paths are rigorously verified. Our findings suggest that formal proofs can effectively evolve alongside optimized network variants, providing a scalable foundation for the continuous certification of safety-critical machine learning systems.

Zero-knowledge proof (ZKP) systems have surged attention and held a fundamental role in contemporary cryptography. Zero-knowledge succinct non-interactive argument of knowledge (zk-SNARK) protocols dominate the ZKP usage, implemented through arithmetic circuit programming paradigm. However, underconstrained or overconstrained circuits may lead to bugs. The former refers to circuits that lack the necessary constraints, resulting in unexpected solutions and causing the verifier to accept a bogus witness, and the latter refers to circuits that are constrained excessively, resulting in lacking necessary solutions and causing the verifier to accept no witness. This article introduces a novel approach for pinpointing two distinct types of bugs in ZKP circuits. The method involves encoding the arithmetic circuit constraints to polynomial equation systems and solving them over finite fields by the computer algebra system . The classification of verification results is refined, greatly enhancing the expressive power of the system. A tool, AC ⁴ , is proposed to represent the implementation of the method. Experiments show that AC ⁴ demonstrates an increase in the solved rate, showing a 36.7% improvement over Picus and CIVER, and a slight improvement over halo2-analyzer, a checker for halo2 circuits. Within a solvable range, the checking time has also exhibited noticeable improvement, demonstrating a magnitude increase compared to previous efforts.

In the realm of blockchains, synchronization challenges are two-folded. First, smart contracts from different blockchains cannot communicate with each other, making it hard to establish a trustworthy communication channel to share and maintain a universal state between each other. Second, transactions on different blockchains can hardly be ordered. Hence interference is expected. We need a novel way to handle interference. Traditional solutions involving third parties have safety and liveness issues and thus compromise between safety, permissionless, and liveness. ZK Multi-Blockchain Aggregatoris a multi-blockchain execution layer that leverages the power of zero-knowledge proof to minimize the trust base of multi-blockchain communication, which does not compromise safety, liveness, permissionless, and atomicity. In contrast to traditional blockchain bridges performing transactions on different blockchains separately and using a relay system to enforce the order of transactions and prevent interference, our method uses an entirely new approach, such that for each multi-blockchain transaction, it simulates the multi-blockchain transaction in its aggregator chain. Our aggregator uses zero-knowledge proofs of the simulation to convince involved blockchains to update their local state accordingly. On top of this layer, rich applications over multi-blockchains can run safely and efficiently.