Dafny is a programming language that allows users to check the correctness of their code. This requires a formal specification of what a program is expected to do, and a mechanism to prove that the actual behavior of the program satisfies the specification. Dafny follows an auto-active verification approach and uses the SMT solver Z3 to discharge the resulting proof obligations. In addition to program verification, Dafny can be used to prove mathematical properties expressed through predicates and lemmas.Our intention is to explore how effectively Dafny can prove the correctness of reductions between decision problems. A reduction transforms instances of one problem into instances of another so that an algorithm solving the second problem can be used to solve the original one. By formalizing several classical reductions, we evaluate Dafny as an environment for this type of proof and identify a reusable verification pattern based on a reduction function and forward and backward correctness lemmas. The verification of the time complexity of these reductions is outside the scope of this work and is left for future research.
We lay out a new choreographic model that, departing from point-to-point interactions, aims to harness local-first coordination of distributed applications. We dub our model friend-to-friend choreographies since its main application domain are decentralised applications that guarantee confidentiality in a fully decentralisedsetting. A key principle of local-first coordination is indeed that the control on computational resources is not given to third-parties. This yields a notion of projection different than those usually found in the literature since our projection operation aims to identify minimal sets of agents that should be aware of an interaction and so compute the cryptographic keys necessary to ensure confidentiality.Friend-to-friend choreographies have a straightforward implementation in Nearbytes, a platform which provides a communication infrastructure and friend-to-friend decentralised storage.
AI agents are transforming software development from a human-led activity into a collaborative process involving autonomous planners, coders, testers, and reviewers. This shift raises a deceptively simple question with deep engineering and social consequences: when software work is shared between humans and autonomous agents, who is really in charge? This paper argues that the central challenge is coordination: deciding who does what, when, and under whose authority. Natural-language conversation is now the primary medium through which humans and agents interact, assign tasks, and negotiate outcomes; however, conversation is not a substitute for explicit coordination structure. We trace the evolution from Agent-Oriented Software Engineering (AOSE) to contemporary Agentic Software Engineering (ASE), and use a multi-agent code-review scenario to distinguish conversational interaction from governed coordination. The paper argues that autonomy increases the need for coordination; it does not reduce it. Making agentic systems governable therefore requires explicit mechanisms for assigning responsibility, validating outputs, escalating uncertainty, and preserving accountability. We introduce the notion of a runtime coordination contract, a lightweight governance abstraction that specifies roles, task scopes, input/output schemas, escalation conditions, and audit obligations. The paper positions coordination contracts as a runtime analogue of classical coordination and behavioral-contract mechanisms: more flexible than fully pre-designed protocols, but sufficiently explicit to support monitoring and auditability. We discuss some implications for software engineering practice. We conclude proposing an open research agenda concerning contract languages, runtime conformance monitoring, multi-agent benchmarks, and human-agent teaming.
