{"id":"a593bfb5-a390-4678-9330-92721b0bdb3f","arxiv_id":"2502.00138","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"partial","parameter_count":1,"one_line_summary":"JustAct is a formally specified framework that guarantees policy decisions about agent actions stay valid as agents add new policies or update their agreements, with a Rust implementation demonstrated on medical workflow scenarios.","lead":"This paper defines a formal framework, called JustAct, for building multi-agent systems where every action must be backed by enough policy information to prove it is allowed. The authors implement the framework with a new policy language and a Rust runtime, and test it by recreating the medical data processing workflow of an existing system called Brane.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Abstract's stability claim overstates Theorem 3.7: agreements can be removed by growing updates, so permission is not preserved 'regardless of updated agreements'.","rationale":"The reader correctly notes that the abstract is stronger than Theorem 3.7, but their selected weakest assumption is the unformalized `eval` parameter. I see the stability overclaim as more directly load-bearing, because it concerns the paper's headline auditability guarantee rather than the implementation gap. The `eval` issue is real but secondary: all framework theorems are explicitly parametric in `eval`, so the machine-checked stability properties hold for any choice of `eval`; what is unverified is whether the Rust interpreter realizes the intended well-founded semantics, which affects whether the implemented permission decisions match the normative meaning of Slick policies, not whether the formal framework's definitions are internally consistent. In contrast, the abstract's unconditional phrasing is inconsistent with the framework's own Definition 3.2 and Theorem 3.6, and this inconsistency touches the central claim that auditors can rely on past permission decisions. The verdict remains CONDITIONAL: the framework and Theorem 3.7 can be kept, provided the abstract and discussion are amended to state the exact condition under which permission persists, and the wording is aligned with the formal definitions.","tokens_in":45527,"tokens_out":8343,"duration_ms":98621,"concrete_test":"Formalize in Rocq the exact claim made in the abstract: `forall c c' a, growing(c,c') -> permitted(c,a) -> permitted(c',a)`. Attempt to prove it from Definitions 3.2, 3.5, and 3.10. Then construct a concrete instantiation of the framework parameters with two configurations: `c` has `agreed(c, basis(a))` and `c'` has agreements replaced by `[]`, while `stated` and `enacted` grow as required. Show `growing(c,c')`, `permitted(c,a)`, and `not permitted(c',a)`. If this counterexample typechecks, the abstract must be weakened to the conditional form of Theorem 3.7 or explicitly restricted to a fixed historical configuration.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central advertised property is that a permission decision 'cannot be refuted later, regardless of any added statements or updated agreements'. The formal framework does not support this as stated. Definition 3.5 makes permission depend on `based(c,a)`, which requires `basis(a)` to be an agreement in configuration `c`. Definition 3.2 lets `growing(c,c')` hold while agreements are replaced, and Definition 5.8's `Agree(A')` update replaces the agreement list without preserving the old list. Theorem 3.6 explicitly states that `based` is not preserved under growing, and Theorem 3.7 requires `based(c',a)` as an extra premise. Thus, after an agreement update that removes `basis(a)`, an action that was `permitted(c,a)` is not `permitted(c',a)`. This is not a hypothetical corner case: Section 6.3.5 uses exactly this mechanism, updating agreements to `[]` to make all new actions prohibited. If the abstract means that the historical proposition `permitted(c,a)` remains true, that is trivially true because `c` is fixed, and it requires auditors to retain the old agreement list; the formal `config` type in Definition 5.6 records only the current agreement list and the update relation discards the old one. Either way, the paper's headline guarantee needs a precise qualification: permission is stable only while the original basis remains an agreement, or stability must be stated with respect to a fixed historical configuration.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces JustAct, a parametric framework for open multi-agent systems in which an action is permitted exactly when it is valid, sourced, and based on an agreed message, and in which actors justify their actions by collecting policy-carrying messages. The authors formalize the framework in Rocq, instantiate it with the Slick policy language and a Rust data-exchange runtime, and evaluate the instantiation by reproducing and extending usage scenarios of the Brane medical workflow system. The headline claimed property is that a permission decision made now cannot be refuted later regardless of added statements or updated agreements.","tokens_in":45854,"tokens_out":4445,"duration_ms":47112,"significance":"If the framework's guarantees were established for the actual implementation, this would be a valuable contribution linking policy specification, distributed systems, and auditable medical data exchange. The paper has real strengths: a substantial Rocq formalisation with machine-checked theorems, a concrete Rust implementation, and a reproducible case study that demonstrates the framework on realistic Brane scenarios. However, the advertised stability property is stronger than what the formal results support, and the core policy semantics is left as an unformalized parameter, so the central auditability claim is currently not established for the implemented system.","major_comments":[{"comment":"The abstract claims that a permission decision \"cannot be refuted later, regardless of any added statements or updated agreements.\" This is not supported by Theorem 3.7. Definition 3.5 makes permission depend on based(c,a), and Definition 3.10 requires basis(a) to be agreed in the current configuration c. Definition 3.2 only preserves stated messages and enacted actions under growing, not agreements, and Definition 5.8 replaces the agreement list on an Agree update without retaining the old list. Theorem 3.6 explicitly states that based is not preserved under growing, and Section 6.3.5 uses exactly this mechanism, updating agreements to [] to prohibit all new actions. Therefore an action that is permitted(c,a) may become prohibited(c',a) after an agree-update. The paper must qualify the stability claim: permission is stable only while the original basis remains an agreement, or stability must be stated with respect to a fixed historical configuration. The abstract and Section 3.6 should be revised to match the precise statement of Theorem 3.7.","section":"Abstract and §3.6 (Definitions 3.5, 3.10; Theorems 3.6, 3.7)"},{"comment":"The truth semantics of Slick, eval, is left as an unformalized parameter in the Rocq formalisation, while the Rust implementation uses the alternating fixpoint algorithm with a hard-coded 30,000-step bound and maps overflow to [error]. Since truth feeds into effect-of (Definition 3.3), validity (Definition 4.7), and therefore permission (Definition 3.5), all the machine-checked theorems are parametric over an arbitrary eval and do not cover the semantics actually implemented. The paper also does not prove that the bounded Rust evaluation agrees with the well-founded semantics on the policies appearing in the case study. This is a load-bearing gap for the advertised auditability guarantee: an auditor using the implemented system relies on a semantics that is not covered by the theorems. Please either formalize eval (including termination and the step-bound behaviour) in Rocq, or explicitly present all results as conditional on eval satisfying suitable properties and provide a separate correctness argument or at least a precise bounded-equivalence statement for the Rust implementation.","section":"§4.4 (Parameter 4.1) and §4.5"},{"comment":"As printed, reconfigure has two clauses for Agree and no clause for Enact: the second line reads reconfigure((E,X,A), Agree(a)) := (E[a↦⊤],X,A), which appears intended to be Enact(a), and the third line reads reconfigure((E,X,A), Agree(A')) := (E,X,A'). This makes the function ill-defined and prevents the transition system from modelling enactment. Since Lemma 5.5 and the (enact) rule in Definition 5.11 depend on reconfigure(·,Enact(a)), this must be corrected. If this is a typographical error in the displayed formula rather than in the formalisation, please fix the presentation so the paper matches the Rocq code.","section":"Definition 5.8"}],"minor_comments":[{"comment":"The phrase \"multi-agent agent systems\" in the first sentence is a typo; it should be \"multi-agent systems\".","section":"Abstract"},{"comment":"Related to the second major comment, the occurrence \"Agree(a)\" in the second reconfigure clause is presumably a typo for \"Enact(a)\"; please ensure all occurrences are consistent after correction.","section":"§5.5, Definition 5.8"},{"comment":"The phrase \"e.g., via the x GPS\" appears to contain a typo; it should probably read \"e.g., via GPS\" or \"e.g., via the GPS\".","section":"Footnote 4"},{"comment":"The sentence \"The Curie policy and runtime system not not capture the kinds of user-configurable multi-agent dependencies\" contains a duplicated negation, which should be corrected.","section":"§8.2"}],"recommendation":"major_revision","confidential_remarks":"The paper fits well in formal methods / distributed systems venues and contains substantial reproducible work. My main concern is the mismatch between the abstract's broad stability claim and the formal theorem, together with the unformalized eval parameter; both are addressable by careful rewriting and by making the delimitation of the formal guarantees explicit. I do not see a need to reject, but the advertised properties must be corrected before the paper can be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The JustAct paper is worth reading if you work on policy-regulated multi-agent systems. The main positive: it gives a clean parametrized ontology—agreements, statements, actions, effects, permission—and proves genuine monotonicity results. The Rocq formalization is real: Theorem 3.3 (effects persist under growth) and Theorem 3.4 (sourced actions stay sourced) are simple but useful, and the framework's separation of static policy semantics from dynamic configuration is the right call. The reflective extraction of authorship into policies is a clever mechanism for meta-policy control; I haven't seen that exact trick before.\n\nThe soft spots are real but not fatal. The abstract says a permission decision \"cannot be refuted later, regardless of any added statements or updated agreements.\" That is false as stated. Theorem 3.7 requires based(c', a)—the basis must still be an agreement in the later configuration—and Theorem 3.6 explicitly grants that based can be lost when agreements are replaced. The paper's own case study uses agreement replacement to prohibit actions. The fix is straightforward: state stability with respect to a fixed historical configuration, or require the basis to persist. This is an overstatement in the abstract and surrounding prose, not a flaw in the formal results, which are honest about the premise.\n\nThe second soft spot is the eval parameter. The entire Slick semantics is unformalized; the Rocq theorems are parametric over eval. The Rust implementation uses an alternating fixpoint with a hard 30,000-step bound that returns [error] when exceeded. That means the machine-checked guarantees don't cover the implemented semantics. The authors flag this in Section 4.4, but it matters: the auditability story for the actual system depends on eval being correct, and there is no formal connection. I'd want at least a precise specification of eval, if not a Rocq definition.\n\nMinor: the case study is qualitative and the \"acceptable runtime performance\" claim is unsupported by measurements. The distribution of agents is faked (aliased views), so the distributed claims are architectural, not empirical.\n\nWho is this for? People building verified policy engines or studying Datalog-based normative systems. It deserves a serious referee—the framework is coherent, the formal backbone is mostly machine-checked, and the limitations are honestly discussed. I'd ask for revision, not desk rejection.\n\nRecommendation: send to peer review; the authors need to fix the abstract and either formalize eval or soften the implementability claims.","headline":"A well-structured framework with genuine formal content, but the headline auditability guarantee is weaker than advertised and the implemented semantics is not the formalized one.","tokens_in":46375,"tokens_out":1986,"would_cite":true,"duration_ms":20555,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"JustAct lets actors attach policy statements and a basis agreement to each action, and proves that an enacted action's permission is a stable, objective property no later observer can refute.","keywords":["multi-agent systems","auditable permission","policy languages","Slick","well-founded semantics","Rocq formalisation","inter-organisational policies","medical data sharing"],"falsifier":"Run a Slick policy whose well-founded model needs more than the 30,000-step bound to reveal a true fact (for example, a chain of rules of sufficient length) through the Rust interpreter: if the fact is missing or the policy is declared invalid because eval returns [error], the implemented semantics diverges from the assumed one. Separately, enact an action permitted under one agreement set, replace the agreements so the action's basis is no longer agreed (as the case study does when it sets agreements to the empty list), and re-run the permission decision on the enacted action: the outcome pins down whether the stability claim is unconditional or strictly conditional on the basis remaining agreed.","tokens_in":45319,"feed_emoji":"⚖️","tokens_out":13168,"duration_ms":112977,"temperature":0.7,"pith_summary":"The paper tries to establish that open multi-agent systems regulated by inter-organisational policies can still have objective and stable permission decisions, even though no single agent has complete knowledge of all policies. JustAct defines a class of systems in which actors justify their actions by attaching the relevant policy statements and a basis agreement to the action itself, so any observer can verify permission from the action's payload alone. The central result, Theorem 3.7, proves that a permitted action remains permitted as the configuration grows, as long as its basis message stays agreed; since statements and enacted actions only accumulate, the decision an actor relied on can be reproduced by any future auditor. This matters for settings such as distributed medical data processing, where policies are sensitive, change frequently, and cannot be synchronised in full. The paper instantiates the framework with the Slick policy language, formalises it in the Rocq prover, implements it in Rust, and demonstrates it by reproducing the usage scenarios of the Brane medical workflow system.","feed_headline":"'Permitted' verdicts hold up as policies change","feed_subtitle":"JustAct makes action permission an objective, stable property auditors can verify without full policy knowledge.","key_machinery":"The load-bearing mechanism is the three-criterion permission predicate together with the monotonicity of growing configurations ($\\operatorname{growing}(c,c')$ preserves all stated messages and enacted actions, while leaving agreements free to change). An action carries its own justification in its payload: messages authored by various agents, the distinguished basis message that must be an agreement, and a self-identification of the actor, injected via the $\\operatorname{reflect\\text{-}author}$ and $\\operatorname{reflect\\text{-}actor}$ transformations so that extracted policies express who contributed what. Permission is then decidable locally from the action's payload plus the current agreements, independent of which agent performs the check. Supporting machinery is the Slick policy language, a Datalog-style rule language whose validity is defined as not entailing the error fact and whose semantics is the well-founded semantics, a three-valued logic computed by the alternating fixpoint algorithm that the paper leaves as an unformalised parameter.","core_discovery":"The paper's central claim is that permission in a JustAct system is a stable and objective property of enacted actions: any decision that an action is permitted now cannot be refuted later, regardless of added statements or updated agreements. Formally, permission is a three-part conjunction, $\\operatorname{permitted}(c,a) := \\operatorname{valid\\text{-}act}(a) \\land \\operatorname{sourced}(c,a) \\land \\operatorname{based}(c,a)$: the policy extracted from the action's payload must be valid (must not entail the error fact), every message in the payload must have been stated, and the action's distinguished basis message must be an agreement. Statements and enacted actions are historical facts that only grow, and validity is static, so the only fragile ingredient is the agreement; Theorem 3.7 shows that a permitted action stays permitted under any growing configuration provided its basis remains agreed. Because the justification travels inside the action, the decision is decidable and identical for every observer, which the paper treats as the foundation for auditing, for keeping sensitive policies private, and for letting actors predict how future auditors will judge their past behaviour.","pith_inferences":["The abstract's unconditional phrasing of the stability claim is slightly stronger than Theorem 3.7, which requires the action's basis message to remain agreed ($\\operatorname{based}(c',a)$); the case study's emergency update of the agreements to the empty list shows agreements do change, so the defensible reading is that the past decision is stable, not that a re-check under a new agreement cannot","Because $\\operatorname{eval}$ is an unformalised parameter implemented by an alternating fixpoint algorithm with a hard-coded 30,000-step bound, the machine-checked theorems are parametric over the very semantics that decides validity and therefore permission; a formalisation of the well-founded semantics itself would close the gap between the proofs and the executable system.","The practical bottleneck the paper identifies is justification search: an actor must discover which combination of statements and agreements makes a desired action permitted, which is a combinatorial search; solver-assisted or heuristic justification search would be a natural, testable extension.","The framework's recognised gap that policies cannot regulate communication (an agent who receives a sensitive statement may forward it without becoming ill-behaved) points toward a natural extension in which gossip itself is treated as an action subject to permission, a direction the paper leaves open."],"forward_implications":["Auditors can verify whether an enacted action was permitted using only the action's payload and the agreements, without needing complete knowledge of all statements ever made.","Sensitive policy information can be disclosed on a need-to-know basis while preserving objective accountability, because the justification an actor used travels with the action.","Statements can be gossiped asynchronously and even forgotten by agents, since stated messages and enacted actions only accumulate; only agreements need to be synchronised.","Agreements act as the system's control knob: replacing them restricts which future actions are permitted, while leaving the well-behavedness of past actors intact.","The framework's guarantees are generic over the policy language, so any language with decidable truth and validity that meets the framework's requirements can be plugged in and inherit the stability theorems."],"supporting_citations":[{"why":"Supplies the alternating fixpoint algorithm that implements eval, the unformalised semantic parameter on which all validity and permission guarantees rest.","marker":"[VG89]"},{"why":"Defines the well-founded semantics that Slick policies are intended to have, the reference semantics for the implementation.","marker":"[VGRS91]"},{"why":"Defines the stable model semantics that the well-founded semantics approximates, motivating why Slick uses a three-valued semantics.","marker":"[GL88]"},{"why":"Introduces the Slick policy language, including its syntax, safety, and validity, which this paper adopts.","marker":"[Est25]"},{"why":"Provides the composition-control mechanism for cooperative policy specification that underlies Slick validity and meta-policies.","marker":"[EvB24]"},{"why":"The earlier version of the JustAct framework that this article extends with a new implementation, formalisation, and case study.","marker":"[EMvB24]"},{"why":"Describes the Brane system whose usage scenarios the case study reproduces.","marker":"[VCB21]"},{"why":"Defines the EPI framework's roles and the involves/authorise relations that the initial agreement encodes in Slick rules.","marker":"[KME+24]"}],"fun_headline_variants":["JustAct: permissions stay final as policies evolve","Once permitted, always: JustAct's stability proof","Auditable multi-agent actions with JustAct's stable permissions","JustAct guarantees permission decisions are durable","Stable permission judgments for open multi-agent systems"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The strongest guarantee in the paper rests on eval, the function that computes which facts a policy makes true: it is never formally defined, only implemented in Rust as an alternating fixpoint algorithm with a hard-coded 30,000-step bound, so the machine-checked proofs cover any eval rather than the one that actually runs.","fun_headline_variants_meta":{"raw":{"variants":["JustAct: permissions stay final as policies evolve","Once permitted, always: JustAct's stability proof","Auditable multi-agent actions with JustAct's stable permissions","JustAct guarantees permission decisions are durable","Stable permission judgments for open multi-agent systems"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000246,"raw_usage":{"total_tokens":1574,"prompt_tokens":1014,"completion_tokens":560,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":630,"completion_tokens_details":{"reasoning_tokens":488}},"tokens_in":630,"tokens_out":560,"duration_ms":5844,"temperature":1.0,"reasoning_tokens":488,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-09T20:02:19.207179+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run a Slick policy whose well-founded model needs more than the 30,000-step bound to reveal a true fact (for example, a chain of rules of sufficient length) through the Rust interpreter: if the fact is missing or the policy is declared invalid because eval returns [error], the implemented semantics diverges from the assumed one. Separately, enact an action permitted under one agreement set, replace the agreements so the action's basis is no longer agreed (as the case study does when it sets agreements to the empty list), and re-run the permission decision on the enacted action: the outcome pins down whether the stability claim is unconditional or strictly conditional on the basis remaining agreed.","supporting_citations":[],"review_version":1}