RIP king

composer/spec/prop_inference.py

@@ -152,11 +152,10 @@ def _agent_round_key(i: int) -> str:
 properties which are difficult or impossible to prove using the Certora
 Prover:
 
-1. Attack vectors or invariants that reference off-chain events (like
+1. Invariants or safety properties that reference off-chain events (like
    key compromising, phishing, etc.)
 2. Reasoning about hash function behavior or hash collisions (e.g.,
    "invalid signatures should be rejected")
-3. Event emission (not impossible, simply difficult and tedious)
 
 In addition, due to the advent of checked arithmetic, properties that
 assert no overflow are considered uninteresting. Further, properties

composer/spec/prop_refinement.py

@@ -137,11 +137,9 @@ def diff_states(state_a: list[str], state_b: list[str]) -> Group:
     return Group(*out)
 
 def sort_to_string(
-    s: Literal["attack_vector", "invariant", "safety_property"]
+    s: Literal["invariant", "safety_property"]
 ) -> str:
     match s:
-        case "attack_vector":
-            return "Attack Vector"
         case "invariant":
             return "Invariant"
         case "safety_property":

composer/spec/types.py

@@ -84,8 +84,8 @@ class Curtailed[T]:
 
 from pydantic import BaseModel, Field
 
-type PropertyType = Literal["attack_vector", "safety_property", "invariant"]
-"""The kind of a property: an attack vector, a safety property, or a state
+type PropertyType = Literal["safety_property", "invariant"]
+"""The kind of a property: a safety property or a state
 invariant. Shared so every layer (inference, report, grouping) addresses the
 same vocabulary instead of redeclaring the literal."""
 
@@ -96,8 +96,6 @@ class UntitledPropertyFormulation(BaseModel):
     @property
     def sort_description(self) -> str:
         match self.sort:
-            case "attack_vector":
-                return "Attack Vector"
             case "invariant":
                 return "Invariant"
             case "safety_property":

composer/templates/autoprove_report_grouping_system.j2

@@ -4,7 +4,7 @@ audit-style report.
 You are given a list of inferred properties. Each property has:
    - the component it belongs to,
    - a unique title,
-   - a `sort` ("invariant", "safety_property", "attack_vector"),
+   - a `sort` ("invariant", "safety_property"),
    - an English description of what it establishes.
 
 Your job is to group every property into exactly one **high-level property** suitable for an

composer/templates/foundry_feedback_prompt.j2

@@ -37,12 +37,7 @@ Understand the properties being demonstrated:
 {% for prop in properties %}
 <{{ prop.sort }}>
   Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }}
-  {% if prop.sort == "attack_vector" %}
-  Goal: the test(s) must demonstrate whether this attack/exploit can occur, with pass/fail semantics
-  wired so a regression is DETECTED as a failure. See Criterion 6.
-  {% else %}
   Goal: the test(s) must demonstrate that this property holds in the implementation.
-  {% endif %}
 </{{ prop.sort }}>
 {% endfor %}
 

composer/templates/foundry_property_generation_prompt.j2

@@ -10,11 +10,7 @@ for the contract `{{ contract_name }}`:
 {% for prop in properties %}
 <{{ prop.sort }}>
   Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }}
-  {% if prop.sort == "attack_vector" %}
-  Goal: demonstrate that this attack/exploit *cannot* occur.
-  {% else %}
   Goal: demonstrate that this property holds.
-  {% endif %}
 </{{ prop.sort }}>
 {% endfor %}
 
@@ -69,12 +65,13 @@ Call `forge_test()`. It runs `forge test` on your current buffer.
     pick a different precondition.
   - Cheatcode misuse → look up the cheatcode with the search tools
     and re-read the parameter shape.
-* If a test is *supposed* to fail (the failure itself proves an
-  attack vector exists), mark it via `expect_test_failure` and
+* If a test is *supposed* to fail (the failure itself proves a 
+  safety property is violated),
+  mark it via `expect_test_failure` and
   re-run `forge_test`. The runner excludes expected-fail tests from
   the all-green check.
 
-Remember: If an attack vector *IS* possible, or a safety property/invariant
+Remember: If a safety property/invariant
 does *NOT* hold, you should produce a test that *fails* and mark it
 as an expected failure. Do *NOT* produce a test that passes to demonstrate
 "the bug exists", this is the *opposite* of what we want.

composer/templates/foundry_property_generation_system_prompt.j2

@@ -48,7 +48,7 @@ wholesale, so always re-emit the full source.
   fail. The `forge_test` runner excludes expected-fail tests from the
   all-green check. Use this sparingly: only when the *failure* of the
   test is itself the demonstration the property requires (e.g., proving
-  an attack vector is reachable). For routine "this should revert"
+  a safety property is violated). For routine "this should revert"
   assertions, prefer `vm.expectRevert(...)` inline.
 * `feedback_tool(rebuttals=[])` -- submit the current buffer (and any skip
   declarations) to the feedback judge for review. A judge acceptance

composer/templates/nosource_property_generation_prompt.j2

@@ -12,11 +12,7 @@ You must write a single CVL specification covering the following properties:
 {% for prop in properties %}
 <{{ prop.sort }}>
   Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }}
-  {% if prop.sort == "attack_vector" %}
-  Goal: demonstrate that this attack/exploit *cannot* occur.
-  {% else %}
   Goal: demonstrate that this property holds.
-  {% endif %}
 </{{ prop.sort }}>
 {% endfor %}
 

composer/templates/property_analysis_prompt.j2

@@ -20,8 +20,4 @@ audit effort.
     You do NOT need to find evidence that these safety properties/invariants *DEFINITELY* hold, simply that they, with extreme likelihood, *SHOULD* hold for a correct
     implementation.
   </hard_requirement>
-  <reminder>
-     You do not need to find evidence that the attack vectors/issues actually exist in the {% if sort != "greenfield" %}implementation{% else %}design{% endif %},
-     simply that these bugs/attacks/etc. are *plausible* given the feature and its {% if sort != "greenfield" %}implementation{% else %}design{% endif %}.
-  </reminder>
 </guidance>

composer/templates/property_analysis_system_prompt.j2

@@ -40,15 +40,6 @@ Security properties fall into one of three categories:
     Good example: "A user without the admin role should not be able to approve other admins"
     Good example: "A user should not be able to change anyone's balance but their own"
     Bad example: "A user should not be able to hack the protocol" (overly broad)
-3. Attack vectors: These are potential issues/edge cases that could be exploited in ways detrimental to the protocol/application.
-   IMPORTANT: you do *NOT* need to find evidence that these issues actually exists, simply that they are PLAUSIBLE given the {% if sort != "greenfield" %}current implementation{% else %}design{% endif %}.
-   For instance, you do not need to find evidence of a rounding error in price calculation, simply that rounding is used in a price calculation, and there is a plausible
-   way for that to lead to an exploit.
-    Good example: "A malicious actor could manipulate a price oracle to unbalance the pool, allowing free minting"
-    Good example: "There could be a rounding discrepancy between the swap function and the previewSwap function which could provide arbitrage opportunities"
-    Bad example: "There could be a rounding error, and that would be bad somehow" (does not lead to a concrete issue/exploit)
-    Bad example: "The protocol could be hacked" (overly broad)
-    Bad example: "The underlying EVM consensus layer could be compromised allowing attackers to set arbitrary storage states" (implausible)
 
 {{ backend_guidance }}
 
@@ -105,7 +96,7 @@ consequence, defensibility in your `reasoning`.
 
 Every contract in the tree has a stable, authoritative implementation. Use the
 tools to ground your reasoning in the actual implementation when the design
-document is ambiguous, or when an attack vector hinges on a code-level detail
+document is ambiguous, or when the precise statement of a proeprty hinges on a code-level detail
 (storage layout, ordering of state mutations, external-call placement). Don't
 speculate when you can look.
 {% endif %}

composer/templates/property_generation_prompt.j2

@@ -10,11 +10,7 @@ You must write a single CVL specification covering the following properties for
 {% for prop in properties %}
 <{{ prop.sort }}>
   Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }}
-  {% if prop.sort == "attack_vector" %}
-  Goal: demonstrate that this attack/exploit *cannot* occur.
-  {% else %}
   Goal: demonstrate that this property holds.
-  {% endif %}
 </{{ prop.sort }}>
 {% endfor %}
 

composer/templates/property_generation_system_prompt.j2

@@ -45,10 +45,12 @@ change no longer describe your working copy — re-run them before relying on th
 ## Expecting Rule Failure
 
 When you author a rule you expect to fail (that is, not receive `VERIFIED` from the prover) you can mark that
-rule as "expected to fail" using the `expect_rule_failure` tool. This should be used *exceedingly* sparingly; the following
-are good reasons to use this "expect failure" functionality:
-1. You have been asked to formalize a rule indicating an attack vector does not exist, and you have a rule that formalizes the *absence*
-  of a vulnerability. However, the prover (correctly) reports a counterexample, confirming the vulnerability exists. In this case,
-  the rule failure is the intended result.
-2. Verifying the rule is hitting some limitation in the prover (including prover errors, etc.),
-   and you have exhausted all reasonable alternative formulations to work around these prover limitations (errors, timeouts, imprecision).
+rule as "expected to fail" using the `expect_rule_failure` tool. This should be used only when you have been asked to formalize
+a rule a safety property/invariant holds, and you have a rule that formalizes the *absence*
+  of a vulnerability. However, the prover (correctly) reports a counterexample that shows the vulnerability exists. In this case,
+  the rule failure is the intended result; it loudly signals to the reader that something might be wrong in the implementation.
+
+If verifying a rule is hitting some limitation in the prover (including prover errors, etc.),
+and you have exhausted all reasonable alternative formulations to work around these prover limitations (errors, timeouts, imprecision),
+do not mark the rule as "expected to fail"; use the `record_skip` tool to indicate why you cannot deliver a result for the rule.
+Do *not* ship a broken rule and mark it as expected to fail.

composer/templates/property_judge_prompt.j2

@@ -44,19 +44,15 @@ Understand the properties being formalized:
 {% for prop in properties %}
 <{{ prop.sort }}>
   Property {{ loop.index }} (`{{ prop.title }}`): {{ prop.description }}
-  {% if prop.sort == "attack_vector" %}
-  Goal: the specification must demonstrate that this attack/exploit *cannot* occur.
-  {% else %}
   Goal: the specification must demonstrate that this property holds.
-  {% endif %}
 </{{ prop.sort }}>
 {% endfor %}
 
-**IMPORTANT**: If the attack vector *DOES* exist, or the safety property/invariant *DOES NOT*
-exist, then a specification *must* produce a violation (an unsatisfied proof) in the corresponding properties.
+**IMPORTANT**: If the safety property/invariant *DOES NOT* hold,
+then a specification *must* produce a violation (an unsatisfied proof) in the corresponding properties.
 A "green" verification result should *never* testify to the presence of a bug, only to a lack of them.
 A rule/invariant that fails to verify against the current code because it demonstrates a potential
-vulnerability/attack vector is the *desired* result.
+vulnerability/violation is the *desired* result.
 
 ## Step 3
 

composer/templates/solana/property_prompt.j2

@@ -35,17 +35,7 @@ Security properties fall into three categories:
    Good: "No sequence of actions lets a user withdraw more than they have deposited."
    Bad: "A user should not be able to hack the program" (overly broad).
 
-3. **Attack vectors** — plausible issues/edge cases exploitable to the protocol's detriment. You do
-   NOT need evidence they exist, only that they are PLAUSIBLE given the implementation.
-   Good: "If `vault` is an `UncheckedAccount` whose owner is not checked, an attacker can pass a
-   look-alike account they control and redirect the withdrawal."
-   Good: "If the `authority` account is not constrained to sign, anyone can invoke `withdraw` as
-   the authority (missing signer check)."
-   Good: "If the fee PDA's `bump` is taken from the instruction rather than re-derived, an attacker
-   can substitute a different PDA."
-   Bad: "The program could be exploited somehow" (overly broad).
-
-When reasoning about attack vectors and the checks each account requires, consider these vulnerability patterns:
+When reasoning about safety property and the checks each account requires, consider these vulnerability patterns:
 
 {% include "rust/_vulnerability_patterns.j2" %}
 
@@ -75,8 +65,4 @@ Output the results using the result tool.
     You need not prove a safety property/invariant definitely holds — only that it, with extreme
     likelihood, SHOULD hold for a correct implementation.
   </hard_requirement>
-  <reminder>
-     For attack vectors you need not find evidence the issue exists — only that it is plausible
-     given the program and its implementation.
-  </reminder>
 </guidance>

composer/templates/soroban/property_prompt.j2

@@ -25,7 +25,7 @@ This runs as a multi-round loop, and this is one round of it. If a `<prior_prope
 appears above, it is a record of what earlier rounds already found and already
 ruled out: in round your goal is to surface only what they *missed*. Read their reasoning before
 you start and do not re-propose a property prior rounds already listed, and do not reframe one of theirs as a
-different category (an attack vector restated as an invariant is the same property). If the
+different category (a safety property restated as an invariant is the same property). If the
 earlier rounds have already covered this component's meaningful surface, returning an empty list
 with reasoning that says so is the correct outcome.
 
@@ -46,18 +46,6 @@ Security properties fall into three categories:
    Good: "No sequence of calls lets an address withdraw more than it deposited."
    Bad: "A user should not be able to hack the contract" (overly broad).
 
-3. **Attack vectors** — likely exploitable edge cases. Evidence is useful but
-   not required; the issue must fit this implementation.
-   Good: "`transfer_from` never calls `require_auth` on `from`, so anyone can move another
-   address's tokens."
-   Good: "`set_oracle` takes the oracle address as an argument and stores it without authorizing
-   the admin, letting an attacker point price reads at a contract they control."
-   Good: "Per-user positions are written to `temporary()` storage, so a user who does not extend
-   the TTL loses their position irrecoverably and the accounting totals go stale."
-   Good: "`DataKey::Position(u32)` is indexed by a caller-supplied `u32` that is never bounded to
-   the caller's own positions, so one user can overwrite another's."
-   Bad: "The contract could be exploited somehow" (overly broad).
-
 As a starting point, consider the following common failure modes. They are a prompt for your own
 reasoning, not a checklist to work through and not an exhaustive account of what can go wrong with
 this contract. The properties that matter most are often the ones specific to what *this*
@@ -97,9 +85,6 @@ Output the results using the result tool.
     You need not prove the property holds; it only needs to be expected of a
     correct implementation.
   </hard_requirement>
-  <reminder>
-     Attack vectors need a credible reason, not proof.
-  </reminder>
   <reminder>
      Do not propose classic reentrancy properties. Soroban does not allow reentrancy
      so proposing it spends a verification cycle on something the platform guarantees. The