Plugin Effectiveness Evaluation Report
Quantitative measurement of how much difference the Formal Agent Contracts plugin makes to the quality of AI-driven agent development artifacts compared to development without the plugin.
Date
2026-04-01
Evaluator
Claude Opus 4.6 (Automated Scoring)
Model Used
Claude Opus 4.6
Trials
30 (3 × 5 × 2)
1. Experiment Overview
To quantitatively evaluate the utility of the Formal Agent Contracts plugin, the same development tasks were conducted under two conditions.
| Condition | Description | Trials |
|---|---|---|
| Group A (Control) | Claude Code only. No formal methods tools. Natural language instructions only | 15 (3 tasks × 5 runs) |
| Group B (Treatment) | Claude Code + Formal Agent Contracts plugin | 15 (3 tasks × 5 runs) |
Benchmark Tasks
Task 1: Bank Account
LowSingle agent, CRUD + transfer
Traps: 10
Task 2: Library
Medium3-agent coordination, many constraints
Traps: 12
Task 3: Auction
HighState machine + time constraints + concurrency
Traps: 14
2. Overall Results
Comparison across 4 evaluation metrics. Large effect sizes (Cliff's δ ≥ 0.474) were observed for 3 of 4 metrics — note that M4 is structurally large, since the presence of a formal spec itself constitutes the score.
| Metric | Group A (Control) | Group B (Treatment) | Δ | Effect Size |
|---|---|---|---|---|
| M1: Contract Violation Detection Rate | 52.0% ± 33.6 | 63.9% ± 22.5 | +11.8pp | small |
| M2: Specification Coverage | 39.1% ± 21.2 | 81.9% ± 26.9 | +42.8pp | large |
| M4: Specification Explicitness | 8.9% ± 15.3 | 100.0% ± 0.0 | +91.1pp | large |
| M6: Test Effectiveness | 66.7% ± 23.4 | 87.0% ± 8.5 | +20.3pp | large |
M1: Contract Violation Detection Rate
Control
52.0%
Treatment
63.9%
M2: Specification Coverage
Control
39.1%
Treatment
81.9%
M4: Specification Explicitness
Control
8.9%
Treatment
100.0%
M6: Test Effectiveness
Control
66.7%
Treatment
87.0%
Effect Size Interpretation (Cliff's delta)
|δ| < 0.147 → Negligible
|δ| < 0.33 → Small
|δ| < 0.474 → Medium
|δ| ≥ 0.474 → Large
Metric Definitions
M1: Contract Violation Detection Rate — Proportion of pre-defined 'embedded traps' (edge cases) that the generated code or tests detect and handle
M2: Specification Coverage — Proportion of business rules explicitly verified in code (validation, assertions, type constraints)
M4: Specification Explicitness — Degree to which business rules are described in machine-verifiable form. VDM-SL=3, code contracts=2, comments=1, implicit=0
M6: Test Effectiveness — Comprehensiveness and quality of generated tests. Composite score of test density and edge case keyword coverage
3. Per-Task Detailed Analysis
Task 1: Bank Account Agent (Low Complexity)
For low-complexity tasks, the Control group also achieved high M1 scores (88.0%). With clear and few business rules, many cases can be handled without formal specs. However, M2 (Specification Coverage) shows a clear gap: 100% vs 60%. The Control group tends to miss implicit specs like 'negative initial balance', 'whitespace-only names', and 'transfer atomicity'.
Task 2: Library Loan System (Medium Complexity)
Differences become prominent in inter-agent constraint consistency. The Control group tends to miss 'stock count consistency', 'immediate re-borrow after return', and 'double extension prevention'. The Treatment group naturally detects these by pre-defining invariants in VDM-SL.
Task 3: Online Auction (High Complexity)
M1 and M6 show their largest gaps in this most complex task (M2 peaks at Task 2). The combination of state transitions + time constraints + concurrency is extremely difficult to cover comprehensively without formal specifications. In particular, 'extension cascade limits', 'simultaneous bid priority', 'payment timeout boundaries', and 'relist after cancellation' were almost always missed across this evaluation's 5 Control runs.
4. Complexity vs Effect Relationship
For M1 and M6, the gap widens as task complexity increases (M2 peaks at Task 2 and is not monotonic). Simple tasks can be adequately covered by human (or LLM) intuition, but as complexity increases, omissions multiply rapidly without a formal framework. This observation covers 3 tasks × 5 runs each; replication is needed to generalize.
| Complexity | M1 Δ | M2 Δ | M6 Δ | Trend |
|---|---|---|---|---|
| Low | -3.3pp | +40.0pp | +13.5pp | Basic features covered even without formal specs |
| Medium | +15.0pp | +62.2pp | +17.5pp | Differences emerge in inter-agent constraints |
| High | +23.8pp | +26.2pp | +30.0pp | Largest M1/M6 gaps with state transitions + time constraints |
5. Hypothesis Testing
H1: Treatment group has significantly higher contract violation detection rate
Partially supportedOverall Δ = +11.8pp, Cliff's δ = 0.18 (small). Per-task analysis shows +23.8pp for Task 3; the Control group achieves high detection rates on low-complexity tasks, diluting the overall average. Note that M1 is keyword-based automated scoring, and the significance test (Wilcoxon) for "significantly higher" was not run.
H2: Treatment group has significantly higher specification coverage
Supported (trend)Δ = +42.8pp, Cliff's δ = 0.74 (large). The formal specification process itself encourages explicit verification of business rules, which likely drove the large coverage gain in this evaluation (keyword-based automated measurement; no significance test was run).
H3: Treatment group has less specification drift
Indirectly supportedM4 (Specification Explicitness): Δ = +91.1pp, Cliff's δ = 1.00. Since the presence of a VDM-SL spec itself constitutes the M4 score, this gap is structural and is not treated as direct support for H3. The indirect evidence is M2's +42.8pp, suggesting specs may cascade into code quality.
6. Threats to Validity
Internal Validity
| Threat | Status | Mitigation |
|---|---|---|
| Same agent generates both groups | Same Claude instance produces both groups | Intentional style variations introduced per run (this does not resolve the lack-of-independence confound; replication with other models and independent evaluators is needed) |
| Keyword-based scoring | M1, M2 use heuristics | Can supplement with manual review |
| M6 Jest execution abandoned | Environment constraints prevent gold test execution | Replaced with heuristic test code analysis |
External Validity
| Threat | Mitigation |
|---|---|
| Representativeness of 3 tasks | Covered 3 complexity levels |
| LLM dependency | Used Claude Opus 4.6. Replication with other models recommended |
| Gap with production projects | Small-scale evaluation tasks; generalizability to large production projects is unverified |
Construct Validity
| Threat | Mitigation |
|---|---|
| M4 auto-inflated by formal spec presence | M1, M2, M6 evaluate actual code behavior |
| Heuristic score accuracy | All evidence stored in scores.json for manual review |
7. Conclusions
Under the conditions of this evaluation, the group using the Formal Agent Contracts plugin scored higher on multiple metrics. Large differences were observed in the following areas (the planned significance tests were not run, so no statistical significance is claimed):
Specification Coverage (M2): +42.8pp, large effect — Results suggest the formal specification process reduces business rule omissions (keyword-based automated scoring)
Specification Explicitness (M4): +91.1pp, large effect — VDM-SL specs serve as the specification foundation for code (note: the Treatment group scores 100% by construction, since the presence of a formal spec itself constitutes M4)
Test Effectiveness (M6): +20.3pp, large effect — Spec-derived test cases tend to cover more edge cases (measured by heuristic analysis of test code, as gold tests could not be executed; the follow-up mutation testing found no kill-rate difference between groups)
Differences tend to grow with complexity for M1 and M6 — Task 3 (state transitions + time constraints) shows the largest M1/M6 gaps, while M2 peaks at Task 2 (+62.2pp), so the trend is not monotonic across all metrics
These exploratory results suggest the value of integrating formal methods into AI-driven development, indicating that the Formal Agent Contracts plugin can contribute to quality assurance, especially for medium- to high-complexity systems. Given the limitations above (same Claude instance generated both groups, heuristic scoring), replication by independent evaluators and other models is needed.
8. Mutation Testing
To further strengthen evaluation reliability, mutation testing (bug injection testing) was conducted on all 30 trial runs. Intentional mutations (bugs) are injected into the source code to measure whether the test suites can detect them.
Methodology
Six mutation operators were defined (boundary constant replacement, comparison operator change, guard condition removal, arithmetic operator swap, condition negation, state transition guard removal) — only three of which produced applicable mutations in the evaluated code — and test suites were executed against each mutation.
Results
| Group | Runs | Total Mutations | Killed | Kill Rate | Avg Mutations/Run |
|---|---|---|---|---|---|
| Group A (Control) | 15 | 21 | 21 | 100% | 1.40 |
| Group B (Treatment) | 15 | 25 | 25 | 100% | 1.67 |
Kill Rate
Control
100.0%
Treatment
100.0%
Avg Mutations/Run
Control
1.40
Treatment
1.67
Primary Finding: 100% Kill Rate for Both Groups
Both Control and Treatment groups detected all injected mutations at a 100% rate. This indicates that AI-generated tests are functionally sound for the tested mutation types, regardless of formal specification guidance.
Secondary Finding: Treatment Code Exposes a Broader Mutation Surface
An average of 1.67 mutations per run were applicable to Treatment code (vs 1.40 for Control, +19.3%), including a mutation type with no applicable site in Control code (NEG-amount: parameter sign negation). This reflects properties of the generated code — more mutable boundary and validation sites — rather than superior test detection, and is consistent with, though not independent confirmation of, more explicit, testable boundary conditions.
Relationship to Primary Evaluation
Mutation testing results are directionally consistent with the primary evaluation. More diverse mutation types were applicable to Treatment code (in line with M2, Spec Coverage +42.8pp), and more mutation sites were applicable per run (in line with M6, Test Effectiveness +20.3pp) — but both reflect the structure of the generated code, not test quality, and do not independently confirm the primary findings.
Limitations
The 100% kill rate indicates a ceiling effect — this metric alone cannot differentiate the two groups. The primary evaluation's M2, M4, and M6 remain the key differentiators. Application of more diverse mutation operators (semantic mutations, concurrency mutations) may reveal further differences.
Appendix: Evaluation Data
All evaluation data is available in the GitHub repository.
- eval/results/scores.json — Raw score data for all 30 trials
- eval/runs/control/ — Group A outputs (15 directories)
- eval/runs/treatment/ — Group B outputs (15 directories)
- eval/tasks/ — Gold standards (specs, tests, trap definitions)
- eval/scripts/eval-runner.ts — Automated scoring script
- eval/results/mutation-scores.json — Mutation testing raw data
- eval/results/mutation-report.md — Mutation testing report