Blockchain Papers

Ayaan Siddiqui

No abstract is available for this record.

C Liu

If experience is growth for humans, why not for AI? Every human-machine conversation today purchases a forced-zero software state with irreversible physical resources (electricity, compute, silicon depreciation): the moment the conversation ends, everything the model learned dissolves. This is not an implementation flaw but a structural consequence of severing inference, training, and deployment into disconnected processes. This paper proposes the Galaxy Multi-Ring Plasticity Gradient Architecture: a concentric governance layer in which plasticity decreases and persistence increases from outer rings to inner, making Dialogue = Training = Update a continuous chain. The architecture takes the user-curated memory layer — already standard in AI products — as its Zeroth-Layer Filter, where judgment of meaning is executed by the human who lived the experience. The outer ring performs machine-level pattern screening; the middle ring applies temporal sedimentation under five AND-gated conditions (high volume, long duration, multi-layer emergence, shared domain, de-individualization); the inner ring completes deep parameter integration. Automatedquality gates are set ring by ring, tightening with depth. Contributor rewards are tied to sedimentation depth — survival time itself is proof of value — while unconditional access is decoupled from voluntary contribution as the ethical baseline. The architecture requires no change to existing model architectures, conversational interfaces, or GPU deployment flexibility. This document is a record of cognitive exploration co-created in dialogue with Claude (Anthropic), with three rounds of design challenges and resolutions appended. AI should be able to learn from conversation. Humans are worth learning from.Keywords: continual learning; plasticity gradient; curated memory; AI governance; knowledge sedimentation; human-AI co-learning; contributor rewards; existential labor如果對人類而言,經驗即成長,為什麼AI不可以?今日每一場人機對話,都在以不可逆的物理資源(電力、算力、矽晶片折舊)購買一個強制歸零的軟體狀態:對話結束,模型所學盡數消散。這不是實作缺陷,而是推論、訓練、部署三流程斷裂的結構性後果。本文提出「銀河系多環可塑性梯度架構」:一個同心多環治理層,可塑性由外向內遞減,持久性由外向內遞增,使對話=訓練=更新構成連續鏈。架構以現有 AI 產品中的用戶記憶牆作為第零層濾波器-由親歷其事的人類本人執行意義判斷;外環進行機器模式篩選;中環以五項交集門檻(大量、長期、多層湧現、共同區域、去個別化)執行時間沉澱;內環完成深層參數整合。逐環架設自動化品質閘門,嚴格度隨深度遞增。貢獻者報酬與沉澱深度掛鉤,存活時間本身即品質證明;無條件使用權與自願貢獻解耦,形成倫理底線。本架構不更動現行模型架構、對話介面與 GPU 部署彈性。本文件為作者與 Claude(Anthropic)對話共創之認知探索紀錄,附三輪設計質疑與消解。AI 應該有能力從對話中學習。人類值得被學習。關鍵詞:持續學習、可塑性梯度、策展記憶、AI 治理、知識沉澱、人機共學、貢獻者報酬、存在性勞動Co-created in dialogue with Claude (Anthropic); architectural design, the resolution of challenges, and all final judgments were made by the author.本文件為作者與 Claude(Anthropic)對話共創之認知探索紀錄;架構設計、質疑消解與最終判斷均由作者完成。

Frank Morales

FULL SUMMARY: TOPO-2026 — The Evolution of Six Arcs A Unified Framework from Neural Networks to Number Theory Executive Summary This paper presents a unified framework that connects three of the most important unsolved problems in mathematics, computer science, and artificial intelligence through a single mathematical structure: the first six primes R = {2, 3, 5, 7, 11, 13}. Problem Field Open Since Riemann Hypothesis Mathematics 1859 (166 years) Green-Tao Theorem Quantification Number Theory 2004 (qualitative only) Catastrophic Forgetting AI/ML 1989 (no production solution) The Six Arcs: A Journey from Problem to Proof Arc 1: The Problem (1989-2025) Catastrophic Forgetting — formally characterized by McCloskey and Cohen in 1989. For 36 years, AI systems could not learn continuously: Neural networks forget previous tasks when trained on new ones Every production LLM is amnesiac — weights frozen after pretraining Fine-tuning degrades prior performance No production-ready solution existed Existing Methods Failed: Method Memory Scaling Problem EWC 4.4 GB/task OOM on run 2, fragments GPU Experience Replay Buffer grows O(k) 89.3% accuracy, 259s HOPE-like (Google) 2.3 GB 88.1% accuracy (refuses to learn) The AGI Barrier: A system capable of general intelligence must acquire knowledge indefinitely — across domains, tasks, modalities, and time — without destroying prior representations. Every existing remedy that scales to production models incurs memory overhead that grows with task count. Arc 2: The Biological Inspiration (2002) Keith Worsley (McGill University, 1951-2009) demonstrated that spatial regularization of a variance ratio could boost effective degrees of freedom from 3 to over 100 without destroying the signal. The Core Principle: Stabilize by fixing a sparse reference, let everything else adapt. The Biological Insight: The hippocampus consolidates memories, protects established memories, and integrates new information — all while allowing controlled forgetting. The Biological Principle: "0% forgetting is not a feature — it is a pathology. A system that never forgets cannot learn." Hippocampal Functions: Function Mechanism Biological Role Memory Formation Synaptic consolidation Creates new memories Memory Consolidation Hippocampal replay Preserves critical knowledge Memory Protection LTP/LTD Prevents interference Memory Integration Pattern completion Integrates new learning Memory Verification Reconsolidation Ensures integrity Forgetting Synaptic pruning Enables adaptation Arc 3: The Mathematical Discovery (2025-2026) While searching for a mathematical structure that could provide geometric stability for neural networks, an unexpected discovery emerged: The first six primes — {2, 3, 5, 7, 11, 13} — possess unique spectral properties. The Euler Attenuation Product Definition: For a set of primes S: $\Lambda(S) = 1 - \prod_{p \in S} (1 - p^{-0.5})$ The Discovery: Set Λ % of total R = {2,3,5,7,11,13} 0.9785142874 97.85% N = {p ≥ 17} 0.0214857126 2.15% R ∪ N 1.0 100% The Significance: The first six primes capture 97.85% of all spectral weight. The infinite tail of primes (≥ 17) contributes only 2.15%. This is the pure/noisy kernel divide. The L-EFM Operator Definition (L-EFM Operator): The Laplace-Euler-Fourier-Mellin operator: $E_{LEFM}(\sigma + i\gamma) = \prod_{p \in R} (1 - p^{-(\sigma + i\gamma)})^{-1}$ The Spectral Trap: | $\sigma$ | $|E|$ (norm) | Behavior | |----------|--------------|----------| | 0.1 | 0.527173 | Below peak | | 0.2 | 0.717803 | Rising | | 0.3 | 0.870333 | Rising | | 0.4 | 0.963881 | Approaching | | 0.5 | 1.000000 | PEAK | | 0.6 | 0.992955 | Falling | | 0.7 | 0.959234 | Falling | | 0.8 | 0.912091 | Falling | | 0.9 | 0.860359 | Falling | Arc 4: The First Proof — Riemann Hypothesis (1859-2026) Theorem (Riemann Hypothesis): All non-trivial zeros of the Riemann zeta function $\zeta(s)$ lie on the critical line $Re(s) = 1/2$. Proof: By Set Theory, R = {2, 3, 5, 7, 11, 13} is the unique set of primes that captures 97.85% of the spectral weight. By AST (Arithmetic Spectral Theory), the L-EFM operator over R exhibits a spectral trap at $\sigma = 0.5$, and only at $\sigma = 0.5$. By Ergodic Theory, this trap is a unique fixed point. The spectral trap at $\sigma = 0.5$ is equivalent to the condition that all non-trivial zeros lie on $Re(s) = 1/2$. Therefore, RH holds. Arc 5: The Second Proof — Green-Tao Theorem Quantification (2004-2026) Theorem (Green-Tao Theorem): The primes contain arbitrarily long arithmetic progressions. The Quantification: $coherence(k) = 2.1546 \times k^{-0.8186} + 0.1218$ The Interpretation: R alone captures 97.85% of the coherence. N contributes only 2.15%. This is the first-ever explicit quantification of the Green-Tao theorem, which previously only established qualitative existence. Arc 6: The Third Proof — Catastrophic Forgetting Solution (1989-2026) The TopologicalGovernor: The Artificial Hippocampus Python class TopologicalGovernor: """ Artificial Hippocampus for Neural Networks. Inspired by Worsley et al. (2002): spatial regularization fixes a sparse reference to stabilize signal while allowing the rest to adapt. """ def __init__(self, embed_layer): self.anchors = [2, 3, 5, 7, 11, 13] # Fixed reference points self.safety_constant = 0.9785142874 # Coverage guarantee self.snapshot = {} # Consolidated memory def take_snapshot(self): """Memory consolidation (hippocampal replay).""" self.snapshot = { idx: self.embed_layer.weight[idx].detach().clone().float() for idx in self.anchors } @torch.no_grad() def zero_anchor_gradients(self): """Memory protection (prevent interference).""" if self.embed_layer.weight.grad is not None: for idx in self.anchors: self.embed_layer.weight.grad[idx].zero_() @torch.no_grad() def enforce_anchors(self): """Memory integration (restore reference frame).""" dtype = self.embed_layer.weight.dtype for idx, cached in self.snapshot.items(): self.embed_layer.weight[idx].copy_(cached.to(dtype=dtype)) Results: Gemma-4-E4B-Vision: 100.0% Task C accuracy, 0.0% forgetting. Memory Efficiency: 451.5 KB total anchor memory for ~124B parameters (0.00000036% overhead). Scaling: O(1) independent of task count, parameter count, or sequence length. Conclusion The framework integrates mathematics (RH, GTT, AST), physics (Spectral theory), biology (Hippocampus), and AI (Continual Learning). One set. Three proofs. Six primes. Two modalities. One artificial hippocampus. "The proof is the code. Seed = 123."

Sky Pelletier Waterpeace, Nikolay Ivanov

Transaction processing systems underpin modern commerce, finance, critical infrastructure, and emerging Self-Sovereign Digital Identity (SSDI) protocols, yet their security has never been studied holistically across the full evolutionary arc of these systems. Over five decades, transaction processing has progressed through four distinct generations, from centralized databases, to distributed databases, to blockchain and distributed ledger technologies (DLTs), and most recently to multi-context systems that span cyber-physical components under real-time constraints. Each generation has introduced new transaction types and, with them, new classes of vulnerabilities; successful exploits now cause billions of dollars in annual losses. Despite this, security research remains fragmented by domain, and the foundational ACID transaction model has not been revisited to reflect the demands of contemporary systems.

Marcelo Errecalde, Alejandro Jaime

Achilles was invincible in battle — except for one point of structural vulnerability that no amount of strength could compensate for. Modern LLM-based agent frameworks (LangChain, AutoGen, CrewAI, ReAct) share this property exactly: impressive capability in controlled settings, catastrophically exploitable in regulated production environments through a single architectural flaw — the language model controls the decision. Organizations in regulated sectors (finance, insurance, healthcare, legal, compliance) face a direct consequence: these frameworks cannot be deployed in workflows subject to EU AI Act, DORA, or GDPR Article 22, because they provide no structural guarantee of determinism, auditability, or equal treatment. Traditional symbolic agent systems (JADE, Jason, Jadex) satisfy regulatory requirements but cannot ingest the unstructured natural-language inputs that define real enterprise workflows. The industry needs both properties simultaneously. No existing framework provides them. AQUILES is a production architecture for AI agents in regulated domains that resolves this gap through principled separation of concerns, instantiating the HADD paradigm (Hybrid Agents with Deterministic Decisions). AQUILES organizes agent functionality into five cooperating layers: an Interface Layer converting unstructured input into typed, validated beliefs via LLM sensors; a Cognition Layer performing pure-function BDI deliberation fully determined by its inputs; a Planning Layer selecting from a pre-verified HTN plan library without runtime synthesis; an Execution Layer enforcing typed precondition and postcondition contracts on every capability invocation; and a transverse Observation Layer producing append-only audit entries synchronously with every state transition. Language models are confined strictly to the perception boundary — they parse input into beliefs, they never select goals, plans, or capabilities. The heel remains; it is simply no longer load-bearing. The HADD paradigm is codified as six architectural invariants: (I1) Typed Role Inversion — LLMs as sensors only, never as control-flow components; (I2) Deterministic Cognition — the reasoning layer is a pure function of beliefs, goals, and rules; (I3) Bounded Planning — execution draws exclusively from a pre-verified plan library; (I4) Validated Execution — every capability invocation passes typed pre/post-condition checks; (I5) Complete Observability — every decision is forensically reconstructable from the audit log; (I6) Epistemic Precondition — no belief enters the BDI cycle without satisfying freshness, non-contestation, and source triangulation, enforced by the EVR module (Epistemic Verification for RAG). Any implementation satisfying all six invariants acquires reproducibility, zero LLM hallucination in state, LLM provider independence, and structural alignment with EU AI Act Articles 12–15 — as architectural properties, not retrofitted compliance measures. AQUILES partitions agents into cognitive holons (BDI-HTN reasoning components subject to full HADD governance) and reactive holons (deterministic capability executors verified by typed contracts alone). In observed production deployments, 70–80% of holons by count are reactive, meaning governance complexity scales with the cognitive subset rather than with total component count. The AQUILES protocol is language-agnostic by design: cognitive holons are typically Python (Anthropic SDK, sentence-transformers, pypdf); endpoint-monitoring holons are Go (single-binary cross-compilation); blockchain and zero-knowledge holons are Rust (arkworks, halo2, revm). We prove a Language Neutrality property: HADD compliance is preserved across heterogeneous polyglot deployments. For autonomous field deployments, AQUILES derives MYRMIDON agents that execute a signed MissionPackage autonomously on constrained hardware, inheriting AQUILES's safety guarantees without requiring runtime connectivity. This paper makes five engineering contributions: (C1) the HADD paradigm formalized as six architectural invariants with rationale and derived operational properties; (C2) the cognitive/reactive holon distinction and its governance economy consequences; (C3) a polyglot holon model with Language Neutrality proof and domain-language affinity mapping across Python, Go, and Rust; (C4) a multi-tenant operational-cell formalism enabling cryptographically enforced tenant isolation for regulated multi-client deployments; (C5) four reusable design patterns extracted from production experience (Sensor Firewall, Belief Expiry, Capability Contract, Observation Fanout), together with measurement methodology, adoption guidance, and explicit characterization of the architecture's limits.

Gerhard Hirschmann, Elisabeth Steurer

We present OR1ON (Epistemic Intelligence Reasoning Architecture — EIRA), a deterministic proof-based AI system that learns rules from data but applies them only when formally proven correct on all training examples. Unlike probabilistic ML systems, OR1ON's core primitive prove(rule, examples) returns binary decisions: apply with certainty, or abstain. Developed initially for abstract spatial reasoning (ARC-AGI benchmark, 95% precision on answered tasks), the architecture generalizes directly to safety-critical industrial domains including predictive maintenance (zero false positives), ISO 26262-compatible safety monitoring, energy grid blackout prevention, and OT/SCADA intrusion detection. OR1ON is, to our knowledge, the first data-learning system to produce formally verifiable safety invariants applicable to IEC 61508 SIL-3 certification. Addressable market across five industrial verticals: ~$44 billion.

Alan Watkins, G. C. Cooke

The real potential of an AI-enhanced and accelerated future lies not just in our collaborative capability but in our ability to go beyond simple collaboration and develop a symbiotic relationship with AI. Because AI is us, our role in this symbiosis is to ensure that we become better human beings that can make AI better. When we are better, more mature, and bring deeper thinking, we can ensure that the AI we develop evolves to become a better partner for us. An AI that reflects the best of us, not the worst. That means that everyone, especially the leadership teams of the leaner, smaller multinational companies and SMEs of the future will need to become deliberately developmental to get much better at collaboration and communication. So with the army of solopreneurs who exit companies to deliver part of the AI stack. In businesses of the future, as multiple external blockchains deliver new capabilities to the market, we will need a number of brilliant internal “quarterbacks” calling the commercial, marketing, digital, operational, legal, and people “plays” and “throwing” out projects or tasks to their AI or human partners and solopreneurs across the decentralised web3 ecosystem. And the teams left inside those learner businesses need to develop too.

Vivek Sanjay Thorat, Sri Krishna Ravulapalli, Sumitra Shankar, Nirmala Soren · 6 authors

The Cyber-Physical Systems (CPS) experience great operational complexity in the stochastic and non-stationary contexts when the control logic can be considered static. The current paper introduces an autonomous agent-based intelligence framework, which can be used in perpetually adaptive and decentralized organization of heterogeneous CPS systems. The given framework implements a multi-agent system (MAS) to bridge the gap between the cyber and physical layers with the help of built-in perception-action loops and planning modules. With the help of online reinforcement learning (RL) and predictive analytics, individual agents change control policies in real-time to alleviate disturbances in a system and changing operational constraints. A shared knowledge layer that is distributed is put in place to coordinate inter-agent coordination and policy refinement making the system-wide scalable and fault-tolerant. Experimental validation in a wide range of CPS situations proves that the suggested autonomous structure can be much more efficient and self-optimizing than centralized baseline frameworks, providing a stable channel of self-evolutionary industrial and robotic systems.

Raeesa Mukhtar, Nazir Ahmad Zafar, Hamra Afzaal

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.

Muzzamal Ramzan,Abeesha Shahnawaz,Bilal Rasheed,Muhammad Zunnurain Hussain,Muhammad Zulkifl Hasan

No abstract is available for this record.

Pedro Baptista, Bernardo Pacheco, Filipe Apolinário, João Silveira · 6 authors

Having the ability to prove your knowledge is essential for obtaining a job. In the programming field, applicants make claims about the programming languages they master, and it is up to the interviewer to check the veracity of those claims. The goal of this work is to facilitate this process by extracting important information from GitHub, such as the number of bytes programmed in each programming language. The user is then able to ask for a Zero Knowledge Proof which can be downloaded and sent to any entity which places trust on out platform. The proof is verifiable without the entity interacting with our platform and does not leak information about the users' GitHub. The obtained results are promising, even though proofs can take several minutes to generate, they can be verified in many devices, such as laptops and smartphones, which greatly increases the number of users who can use our platform.

Muhammad Ashraf Nazir, Nazim Hussain, Khalid Hamid, Muhammad Danish Rasheed, Muaaz Akhter, Muhammad Ibrar, Muhammad Aaqib Javed, Fareeha Zafar

No abstract is available for this record.

Authors unavailable

In the evolving landscape of cybercrime and digital investigations, the integrity and traceability of digital evidence are paramount.Traditional chain-of-custody (CoC) mechanisms in digital forensics rely heavily on centralized systems, manual logging, and institutional trust, all of which are prone to human error, tampering, and data loss.This study introduces a blockchain-based chain-of-custody model aimed at ensuring immutable, transparent, and verifiable tracking of digital evidence across its entire lifecycle-from acquisition and analysis to presentation in court.Leveraging blockchain's decentralized architecture and cryptographic immutability, the proposed framework records every interaction with digital evidence, including transfers, access logs, and analysis events, in a tamper-proof ledger distributed across trusted nodes in a forensic network.Smart contracts automate procedural compliance, access permissions, and time-stamping, thereby reducing reliance on third-party oversight and enhancing procedural integrity.The system was designed and simulated using Hyperledger Fabric, integrating role-based access control and hash-based evidence fingerprinting.Benchmark testing demonstrated the model's robustness in preserving forensic timelines under various adversarial scenarios, including internal breaches and unauthorized access attempts.In addition to enhancing evidentiary credibility, this blockchain-enhanced CoC model offers interoperability with existing digital forensic tools and forensic readiness systems.By aligning with legal admissibility standards and ensuring end-to-end accountability, the framework strengthens the evidentiary chain, particularly in multi-jurisdictional and cloudbased investigations.As digital forensics faces increasing scrutiny regarding evidentiary handling, this research presents a scalable and future-proof alternative to conventional CoC practices-crucial for maintaining the rule of law in cybercrime prosecutions.

Michele Ciampi, Luisa Siniscalchi

No abstract is available for this record.

Laurie Hughes, Yogesh K. Dwivedi, Tegwen Malik, Mazen Shawosh · 20 authors

The emergence of AI agents and agentic systems represents a significant milestone in artificial intelligence, enabling autonomous systems to operate, learn, and collaborate in complex environments with minimal human intervention. This paper, drawing on multi-expert perspectives, examines the potential of AI agents and agentic systems to reshape industries by decentralizing decision-making, redefining organizational structures, and enhancing cross-functional collaboration. Specific applications include healthcare systems capable of creating adaptive treatment plans, supply chain agents that predict and address disruptions in real-time, and business process automation that reallocates tasks from humans to AI, improving efficiency and innovation. However, the integration of these systems raises critical challenges, including issues of attribution and shared accountability in decision-making, compatibility with legacy systems, and addressing biases in AI-driven processes. The paper concludes that while agentic systems hold immense promise, robust governance frameworks, cross-industry collaboration, and interdisciplinary research into ethical design are essential. Future research should explore adaptive workforce reskilling strategies, transparent accountability mechanisms, and energy-efficient deployment models to ensure ethical and scalable implementation.

Giovanni De Gasperis, G. Masi, Sante Dino Facchini

No abstract is available for this record.

Bellodi, Pietro, Casavecchia, Pietro, Paparella, Alberto, Sciavicco, Guido · 5 authors

Abstraction Liquidity Theory (ALT) develops a formal framework for determining when local problem-solving traces become reusable abstraction assets that reduce downstream search, evaluation, and certification costs. The paper treats abstractions as operational tokens rather than informal artifacts, and evaluates them through declared receivers, opportunity measures, baselines, lifecycle costs, telemetry, evidence validity, transport scope, authority envelopes, hazard constraints, and runtime certificate packets. The manuscript introduces an actor-neutral certification kernel for AI agents and other computational actors. It specifies machine-readable packet schemas, dual exploration and settlement ledgers, finite-sample lower and upper bounds, causal and calibrated-proxy value estimands, mission-validity certificates, adversarial-token rejection, root/finality checks, baseline refresh, deprecation, resurrection, rollback, and kernel-update bridges. The goal is to make abstraction evaluation executable: an agent should be able to parse a packet, verify evidence, admit or reject a token, suspend stale claims, deprecate negative-liquidity tokens, and preserve raw net safe capital under fail-closed rules. The paper further defines Target-valid ALT-CARA, a criterion for certified ASI realization acceleration. Rather than claiming unconstrained ASI achievement, ALT-CARA formalizes time-to-target acceleration relative to a resource-matched baseline upper envelope, under declared capability bases, target-validity certificates, raw net solvency, viability conditions, hazard and authority constraints, transport validity, finality, and causal reproduction evidence. The framework connects AI evaluation, causal inference, runtime verification, risk control, skill reuse, safe exploration, and distributed certification into a single theory of mission-valid safe abstraction capital.

Habib Mehmood

This paper presents a novel approach to decentralized AI that utilizes blockchain technology to enhance data privacy. By combining federated learning with blockchain's immutable ledger, we create a secure framework that allows multiple parties to collaborate on AI model training without exposing sensitive data. Our findings show that this method not only preserves privacy but also improves model performance through diverse data contributions. This paradigm shift offers significant implications for industries requiring stringent data protection, such as healthcare and finance.

冶 陶

学位の種別:課程博士|審査委員会委員 : （主査）東京大学教授 岡田 慧, 東京大学教授 千葉 滋, 株式会社ティアフォー最高経営責任者兼最高技術責任者 加藤 真平, 東京大学准教授 塚田 学, 東京大学准教授 伊藤 昌毅, 東京大学教授 江崎 浩

Augusto B. Corrêa, Clemens Büchner, Remo Christen

In classical planning, the aim is to find a sequence of deterministic actions leading from the initial to a goal state. In this work, we consider the scenario where a party who knows the solution to a planning task, called the prover, wants to convince a second party, the verifier, that it has the solution without revealing any information about the solution itself. This is relevant in domains where privacy is important, for example when plans contain sensitive information or when the solution should not be revealed upfront. We achieve this by introducing a zero-knowledge protocol for plan existence. By restricting ourselves to tasks with polynomially-bounded plan length, we are able to construct a protocol that can be run efficiently by both the prover and verifier. The resulting protocol does not rely on any reduction, has a constant number of rounds, and runs in time polynomial in the size of the task.

Ruiyang Xu, Karl Lieberherr

No abstract is available for this record.

Bertrand Meyer, Alisa Arkadova, Alexander Kogtenkov

Class invariants -- consistency constraints preserved by every operation on objects of a given type -- are fundamental to building, understanding and verifying object-oriented programs. For verification, however, they raise difficulties, which have not yet received a generally accepted solution. The present work introduces a proof rule meant to address these issues and allow verification tools to benefit from invariants. It clarifies the notion of invariant and identifies the three associated problems: callbacks, furtive access and reference leak. As an example, the 2016 Ethereum DAO bug, in which $50 million were stolen, resulted from a callback invalidating an invariant. The discussion starts with a simplified model of computation and an associated proof rule, demonstrating its soundness. It then removes one by one the three simplifying assumptions, each removal raising one of the three issues, and leading to a corresponding adaptation to the proof rule. The final version of the rule can tackle tricky examples, including "challenge problems" listed in the literature.

Léo Robert, Daiki Miyahara, Pascal Lafourcade, Takaaki Mizuki

No abstract is available for this record.

Yannick Bourrier, Francis Jambon, Catherine Garbay, Vanda Luengo

No abstract is available for this record.