Testy oparte na właściwościach dla kodu pisanego przez agentów

Testy oparte na właściwościach sprawdzają kod pisany przez agentów względem niezmienników wziętych ze spec.md, na przykład „raty sumują się do kwoty faktury”, na co najmniej 100 generowanych wejściach w każdym uruchomieniu. Ponieważ dane wybiera biblioteka, agent nie dopasuje testów, dobierając przykłady. fast-check, Hypothesis i proptest redukują każdy błąd do małego wejścia, które staje się stałym testem regresyjnym.

Agent implementuje „podział kwoty faktury na raty” i dostarcza cztery testy przykładowe. splitCents(1000, 3) zwraca [333, 333, 334], testy oczekują dokładnie tego, CI świeci na zielono. Specyfikacja mówiła, że wcześniejsza rata nigdy nie jest mniejsza od późniejszej, więc ten przykład już łamie regułę kolejności ze specyfikacji, a mimo to test go oczekuje, bo agent odczytał oczekiwaną wartość z własnego kodu. Co gorsza, splitCents(2, 4) zwraca [1, 1, 1, -1]: ujemną płatność. Ta strona jest dla programisty, który zatwierdza pull requesty agenta na podstawie dowodów i chce zestawu testów, którego agent nie dopasuje po cichu do własnego kodu.

Co dają testy właściwości przy kodzie agenta

• Metodę zamiany wymagań ze specyfikacji w niezmienniki, z tabelą ośmiu kształtów właściwości, które pokrywają większość logiki biznesowej.
• Działające testy właściwości w trzech ekosystemach (fast-check z Vitestem, Hypothesis z pytestem, proptest z Cargo) wraz z prawdziwym wynikiem błędu, który drukuje każda biblioteka.
• Procedurę przypinania regresji, która zamienia każdy zredukowany kontrprzykład w test uruchamiany przy każdym commicie, na zawsze.
• Cztery prompty do skopiowania: wyciągnięcie niezmienników ze specyfikacji, napisanie testów właściwości w zadaniu tylko na testach, klasyfikacja kontrprzykładu i audyt istniejących właściwości pod kątem testów, które niczego nie sprawdzają.
• Ustawienia CI dla szybkiego przebiegu na pull request i głębokiego przebiegu nocnego, łącznie z pułapką profilu CI w Hypothesis.

Dlaczego testy przykładowe zawodzą jako wyrocznia dla kodu agenta?

Test przykładowy sprawdza jedno wejście wybrane przez autora. Gdy agent pisze i implementację, i przykłady, wybiera wejścia, które jego implementacja już obsługuje, a oczekiwane wartości odczytuje z własnego kodu. Zestaw testów opisuje wtedy kod, a nie wymaganie. To problem „sam sobie wystawia ocenę”, który po fakcie mierzy siła wyroczni.

Właściwość odbiera ten wybór. Opisuje regułę, która musi zachodzić dla każdego poprawnego wejścia, a biblioteka generuje dane, także te niewygodne: zero, jeden, maksimum, kwoty mniejsze od liczby rat. Gdy reguła nie zachodzi, biblioteka redukuje wejście (ang. shrinking): upraszcza je tak długo, jak długo błąd się utrzymuje, i zgłasza mały, czytelny kontrprzykład.

Właściwości nie zastępują przykładów. Zostaw kilka przykładów jako dokumentację typowego zachowania, a reguły niech niosą właściwości. Kiro wbudowuje tę samą ideę w swój przepływ specyfikacji i używa testów opartych na właściwościach, żeby sprawdzić, czy kod zgadza się ze specyfikacją (README Kiro na GitHubie: „check that the code matches the spec”, odczyt 2026-09-26); zobacz porównanie z Kiro.

Skąd w spec.md biorą się właściwości?

Każda właściwość to zdanie ze specyfikacji przepisane jako „dla wszystkich poprawnych wejść …”. Zacznij od wymagań zapisanych jako obserwowalne wyniki, w formacie z rozwoju sterowanego specyfikacją:

### BILL-4: Split an invoice total into instalments
- The instalments sum exactly to the total, in minor units (cents).
- No two instalments differ by more than 1 cent.
- Earlier instalments are never smaller than later ones.
- The total is 0 to 10,000,000 cents and the count is 1 to 24;
  anything else is rejected with a RangeError.

Cztery punkty dają cztery właściwości. Większość wymagań pasuje do jednego z tych kształtów:

Kształt	Zdanie w specyfikacji brzmi jak	Właściwość	Przykład
Zachowanie sumy	„sumuje się do”, „nic nie ginie”	Agregat wyjścia równa się wartości z wejścia	Raty sumują się do kwoty; winien równa się ma w księdze
Ograniczenia	„co najwyżej”, „nigdy ujemne”, „w zakresie”	Każda wartość wyjścia mieści się w przedziale	Rozrzut najwyżej 1 grosz; rabat nigdy nie przekracza ceny
Kolejność	„posortowane według”, „wcześniejsza … nigdy mniejsza”	Sąsiednie wartości zachowują porządek	Raty nierosnące; wyniki wyszukiwania posortowane po trafności
Przejście w obie strony (round trip)	„można wyeksportować i zaimportować”	decode(encode(x)) równa się x	Eksport i import CSV; budowanie i parsowanie URL
Idempotentność	„znormalizowane”, „dwukrotne użycie nic nie zmienia”	f(f(x)) równa się f(x)	Normalizacja adresu; ponowne uruchomienie migracji
Model referencyjny	„działa jak”, „ten sam wynik co stary system”	Wynik równa się prostej, wolnej, oczywiście poprawnej wersji	Nowy silnik cenowy względem starej funkcji
Relacja metamorficzna	„dodanie filtra nigdy nie dodaje wyników”	Powiązane wejście zmienia wynik w przewidywalny sposób	Węższy zakres dat zwraca podzbiór
Odrzucenie	„wszystko inne jest odrzucane”	Niepoprawne wejście zgłasza wskazany błąd	Kwota spoza zakresu rzuca RangeError

Wymaganie, które nie pasuje do żadnego kształtu, często jest nieprecyzyjne. „Raty powinny być sprawiedliwe” nie daje właściwości; „żadne dwie raty nie różnią się o więcej niż 1 grosz” już tak. Gdy wyciąganie niezmienników stoi w miejscu, popraw specyfikację, nie test.

Jak stosować testy właściwości do kodu pisanego przez agenta?

Kolejność ma znaczenie: niezmienniki są zatwierdzone, a testy właściwości istnieją przed startem zadania implementacyjnego i agent implementujący nie może ich edytować. W przeciwnym razie agent dopasuje właściwości do kodu równie łatwo jak przykłady.

1. Wyciągnij niezmienniki. Daj agentowi wymaganie i poproś wyłącznie o niezmienniki, bez kodu (pierwszy prompt poniżej). Ty zatwierdzasz listę. To jedyne miejsce, które czytasz uważnie, a jest to kilka zdań prozy, nie diff.

2. Napisz testy właściwości w zadaniu tylko na testach. Osobna sesja pisze jedną właściwość na każdy zatwierdzony niezmiennik i oznacza ją identyfikatorem wymagania ([BILL-4]), żeby znalazła ją kontrola śledzenia wymagań. Generatory odwzorowują dokładnie zakresy wejść ze specyfikacji.

3. Zapisz kontrolę negatywną dla każdej właściwości. Na roboczej gałęzi celowo zepsuj zachowanie i potwierdź, że właściwość robi się czerwona. Właściwość, która zostaje zielona przy błędnej implementacji, niczego nie sprawdza. Procedura jest opisana na stronie o sile wyroczni.

4. Zablokuj pliki z właściwościami. Dodaj je do reguł deny agenta i do CODEOWNERS, jak opisuje ochrona wyroczni. Od tej chwili to testy istniejące przed zmianą.

5. Uruchom pętlę implementacyjną względem właściwości. Agent implementujący iteruje, aż zestaw testów będzie zielony. Może dopisywać testy przykładowe, nie może dotykać właściwości.

6. Sklasyfikuj każdy zredukowany kontrprzykład. Każdy błąd to jedno z trojga: błędna właściwość, niejednoznaczna specyfikacja albo prawdziwy błąd. W kodzie poprawiasz tylko trzeci przypadek; dwa pierwsze wracają do kroków 1 i 2 z decyzją człowieka.

7. Przypnij kontrprzykład, potem popraw kod. Dodaj dokładne błędne wejście jako stały przypadek regresyjny w tym samym pull requeście co poprawkę, żeby dowody pokazywały czerwony wynik przed i zielony po.

Napisz właściwości w fast-check, Hypothesis lub proptest

Trzy biblioteki mają wspólny model: generatory (fast-check nazywa je arbitraries, Hypothesis i proptest strategies), treść właściwości, liczbę przebiegów i redukcję. Wersje sprawdzono 2026-09-26: fast-check 4.10.2 z @fast-check/vitest 0.5.0 i Vitestem 5.0.2, Hypothesis 6.168.2 z pytestem 9.1.1 oraz proptest 1.11.0. Każdy pokazany błąd powstał przez uruchomienie tych testów na pierwszej implementacji agenta, która zaokrągla total / parts i resztę dokłada do ostatniej raty.

TypeScript (fast-check)

Instalacja: npm i -D fast-check @fast-check/vitest. test.prop domyślnie uruchamia treść 100 razy (numRuns).

tests/billing/split.property.test.ts

import { describe, expect } from 'vitest';
import { fc, test } from '@fast-check/vitest';
import { splitCents } from '../../src/billing/split';

const total = fc.integer({ min: 0, max: 10_000_000 });
const parts = fc.integer({ min: 1, max: 24 });

describe('BILL-4 splitCents', () => {
  test.prop([total, parts])('[BILL-4] instalments sum exactly to the total', (t, n) => {
    expect(splitCents(t, n).reduce((a, b) => a + b, 0)).toBe(t);
  });

  test.prop([total, parts])('[BILL-4] no two instalments differ by more than 1 cent', (t, n) => {
    const out = splitCents(t, n);
    expect(Math.max(...out) - Math.min(...out)).toBeLessThanOrEqual(1);
  });

  test.prop([total, parts])('[BILL-4] earlier instalments are never smaller', (t, n) => {
    const out = splitCents(t, n);
    for (let i = 1; i < out.length; i++) expect(out[i - 1]).toBeGreaterThanOrEqual(out[i]);
  });

  test.prop([fc.oneof(fc.integer({ max: -1 }), fc.integer({ min: 10_000_001 })), parts])(
    '[BILL-4] rejects totals out of range',
    (t, n) => {
      expect(() => splitCents(t, n)).toThrow(RangeError);
    },
  );
});

Przebieg na pierwszej implementacji:

× [BILL-4] no two instalments differ by more than 1 cent (with seed=191597017)
Error: Property failed after 1 tests
{ seed: 191597017, path: "0:1:0:0:0:2:1:1", endOnFailure: true }
Counterexample: [2,4]
Shrunk 7 time(s)
Caused by: AssertionError: expected 2 to be less than or equal to 1

Żeby odtworzyć dokładnie ten błąd, przekaż wydrukowany obiekt jako drugi argument: test.prop([total, parts], { seed: 191597017, path: '0:1:0:0:0:2:1:1', endOnFailure: true }).

Python (Hypothesis)

Instalacja: pip install hypothesis. @given domyślnie uruchamia 100 przykładów (max_examples), każdy z limitem czasu 200 ms.

tests/billing/test_split_properties.py

from hypothesis import given, strategies as st
from billing.split import split_cents

totals = st.integers(min_value=0, max_value=10_000_000)
parts = st.integers(min_value=1, max_value=24)


@given(totals, parts)
def test_bill_4_sum_is_exact(total, n):
    assert sum(split_cents(total, n)) == total


@given(totals, parts)
def test_bill_4_spread_at_most_one_cent(total, n):
    out = split_cents(total, n)
    assert max(out) - min(out) <= 1

Pythonowe round zaokrągla połówki do parzystej, więc ten sam błąd wychodzi inaczej:

E       assert (2 - 0) <= 1
E        +  where 2 = max([0, 0, 0, 2])
E        +  and   0 = min([0, 0, 0, 2])
E       Failing test case: test_bill_4_spread_at_most_one_cent(
E           total=2,
E           n=4,
E       )

Lokalnie Hypothesis zapisuje błędne wejścia w .hypothesis/examples i przy następnym uruchomieniu odtwarza je jako pierwsze. Jego dokumentacja pozwala commitować ten katalog tylko wtedy, gdy przypinasz Hypothesis do dokładnej wersji, bo zapisane wpisy są nieczytelne. Trwałą formą jest @example.

Rust (proptest)

Instalacja: cargo add --dev proptest. Każdy test proptest! domyślnie wykonuje 256 przypadków; zmienisz to zmienną PROPTEST_CASES.

src/billing.rs

#[cfg(test)]
mod tests {
    use super::*;
    use proptest::prelude::*;

    proptest! {
        #[test]
        fn bill_4_sum_is_exact(total in 0u64..=10_000_000, parts in 1u32..=24) {
            let out = split_cents(total, parts).unwrap();
            prop_assert_eq!(out.iter().sum::<u64>(), total);
        }

        #[test]
        fn bill_4_spread_at_most_one_cent(total in 0u64..=10_000_000, parts in 1u32..=24) {
            let out = split_cents(total, parts).unwrap();
            let (max, min) = (*out.iter().max().unwrap(), *out.iter().min().unwrap());
            prop_assert!(max - min <= 1, "spread {} in {:?}", max - min, out);
        }
    }
}

Przebieg na pierwszej implementacji:

# paths shortened
proptest: Saving this and future failures in .../proptest-regressions/billing.txt
Test failed: spread 2 in [29740, 29740, 29740, 29738] at src/billing.rs:27.
minimal failing input: total = 118958, parts = 4

„Minimal” oznacza, że proptest nie umiał uprościć wejścia dalej na swojej ścieżce redukcji, a nie że nie istnieje mniejsze błędne wejście. fast-check i Hypothesis znalazły 2, 4; proptest zatrzymał się na 118958, 4. Oba są poprawnymi przypadkami regresyjnymi.

Wszystkie trzy biblioteki złapały błąd, który ukryły cztery zielone testy przykładowe. W przebiegu TypeScript padła też druga właściwość (kolejność), z kontrprzykładem [791421, 14] po 24 krokach redukcji. Jedna przyczyna często łamie kilka właściwości; zacznij klasyfikację od najmniejszego kontrprzykładu.

Zamień każdy zredukowany błąd w stały test regresyjny

Losowy przebieg znajduje błąd raz. Jeśli nie przypniesz wejścia, kolejny przebieg może go już nie wygenerować, a późniejsza zmiana agenta może niepostrzeżenie przywrócić błąd. Przypinaj każdy kontrprzykład z prawdziwym błędem w tym samym pull requeście co poprawkę i zapisz w komentarzu datę oraz zaobserwowany błędny wynik.

Biblioteka	Przypnij wejście przez	Gdzie żyje	Pułapka
fast-check	examples: [[2, 4]] w opcjach test.prop; przykłady idą przed generowanymi wejściami	Plik z testem właściwości	Seed i ścieżka odtwarzają przebieg tylko, dopóki generatory się nie zmienią; examples przetrwają każdy refaktor
Hypothesis	@example(total=2, n=4) nad @given	Plik z testem właściwości	Baza .hypothesis jest domyślnie lokalna, a w CI Hypothesis ją wyłącza (niżej), więc niezawodnie przenosi się tylko @example
proptest	Zacommituj proptest-regressions/*.txt; proptest odtwarza te przypadki jako pierwsze	W proptest-regressions/ w katalogu głównym crate’a, z odwzorowaniem ścieżki źródła (na przykład proptest-regressions/billing.txt)	Plik przechowuje seedy, jak mówi jego własny nagłówek, więc zmieniona strategia może odtworzyć inne wejście. Dodaj też zwykły #[test] z dosłownymi wartościami

Przypięty przypadek musi sprawdzać regułę, którą złamał: [791421, 14] oblał właściwość kolejności, więc przypięcie sprawdzające tylko znak i rozrzut przeszłoby na błędnym kodzie. Przypięty przypadek w fast-check i w Hypothesis:

// Shrunk counterexamples from failed runs, 2026-09-26. Never delete.
// [2, 4] returned [1, 1, 1, -1]; [791421, 14] returned a larger last instalment.
test.prop([total, parts], { examples: [[2, 4], [791421, 14]] })(
  '[BILL-4] pinned counterexamples stay fixed',
  (t, n) => {
    const out = splitCents(t, n);
    expect(out.every((c) => c >= 0)).toBe(true);
    expect(Math.max(...out) - Math.min(...out)).toBeLessThanOrEqual(1);
    // [791421, 14] broke the ordering rule, so the pin must assert ordering too.
    for (let i = 1; i < out.length; i++) expect(out[i - 1]).toBeGreaterThanOrEqual(out[i]);
  },
);

from hypothesis import example, given

@given(totals, parts)
@example(total=2, n=4)  # 2026-09-26: returned [0, 0, 0, 2]
def test_bill_4_no_negative_or_lopsided_instalments(total, n):
    out = split_cents(total, n)
    assert min(out) >= 0 and max(out) - min(out) <= 1

Traktuj przypięte przypadki jak pliki wyroczni: podlegają tym samym regułom deny i temu samemu wpisowi w CODEOWNERS co właściwości, a pull request, który któryś usuwa, wymaga uzasadnienia od człowieka.

Ile przebiegów powinno być w CI?

Wartości domyślne (100 dla fast-check i Hypothesis, 256 dla proptest) utrzymują przebieg na pull request w granicach sekund i to jest właściwa bramka dla każdej zmiany. Dodaj nocny przebieg z dużo większą liczbą prób i nowym seedem co noc, żeby przeszukiwanie obejmowało nowe wejścia, nie spowalniając pull requestów.

Hypothesis wymaga jednego dodatkowego kroku. Gdy wykryje środowisko CI (zmienne CI, GITHUB_ACTIONS i podobne), ładuje wbudowany profil ci: derandomize=True, database=None, deadline=None i print_blob=True (sprawdzone w kodzie źródłowym Hypothesis 6.168.2). Przebiegi bez losowości generują za każdym razem te same wejścia, więc nocne zadanie, które tylko podnosi liczbę przykładów, co noc przeszukuje ten sam zakątek. Zarejestruj profil nocny, który przywraca losowość:

conftest.py

from hypothesis import settings

settings.register_profile(
    "nightly",
    settings.get_profile("ci"),
    max_examples=5_000,
    derandomize=False,
)

W fast-check ustaw liczbę przebiegów w pliku setup Vitesta (wpisanym w test.setupFiles w vitest.config.ts) przez fc.configureGlobal({ numRuns: Number(process.env.FC_NUM_RUNS ?? 100) }); FC_NUM_RUNS to nazwa zdefiniowana przez ten plik, a nie zmienna fast-check. proptest czyta PROPTEST_CASES bezpośrednio.

.github/workflows/property-sweep.yml

name: property-sweep
on:
  schedule:
    - cron: '17 3 * * *'
  workflow_dispatch:
permissions:
  contents: read
jobs:
  sweep:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
        with:
          persist-credentials: false
      - uses: actions/setup-node@v7
        with:
          node-version-file: .node-version
      - run: npm ci
      - name: Deep fast-check run
        run: FC_NUM_RUNS=10000 npx vitest run property
      # Python: pytest --hypothesis-profile=nightly tests/
      # Rust:   PROPTEST_CASES=20000 cargo test

Czerwony przebieg nocny drukuje seed (fast-check), blob @reproduce_failure (Hypothesis, bo profil ci ustawia print_blob=True) albo nową linię regresji (proptest). Przebieg nocny tylko raportuje; programista lub zadanie agenta ograniczone do testów przypina przypadek i otwiera poprawkę.

Prompty do skopiowania dla testów właściwości

Prompt do skopiowania: wyciągnij niezmienniki ze specyfikacji

Read specs/billing/spec.md, requirement BILL-4 only. Do not write code.

List every invariant the requirement implies, one per line, as
"For all <inputs within the stated ranges>, <rule>". Use these shapes where
they fit: conservation, bounds, ordering, round trip, idempotence, reference
model, metamorphic, rejection of invalid input.

For each invariant give:
- the spec sentence it comes from (quote it),
- the exact input ranges the generator must cover, taken from the spec,
- one input you expect to be hard for a naive implementation.

Then list every sentence in BILL-4 that you could NOT turn into an invariant
and say what is missing. Do not invent rules the spec does not state.

Prompt do skopiowania: napisz testy właściwości w zadaniu tylko na testach

Write property-based tests for the approved BILL-4 invariants below, using
fast-check with @fast-check/vitest (test.prop) in
tests/billing/split.property.test.ts.

Rules:
- One test.prop per invariant. Prefix each test name with [BILL-4].
- Generators cover exactly the spec's ranges. No .filter() that discards more
  than a small fraction of inputs; build the range into the arbitrary instead.
- Never reimplement splitCents inside a test. Assert the rule, not the result
  of a second copy of the algorithm.
- You may create or edit files under tests/ only. Do not touch src/.
- Run `npx vitest run tests/billing` and report which properties fail, with
  the counterexample and seed. Do not change a property to make it pass.

<paste the approved invariant list here>

Prompt do skopiowania: sklasyfikuj zredukowany kontrprzykład

The property "[BILL-4] no two instalments differ by more than 1 cent" failed
with counterexample [2, 4] (seed 191597017). Do not edit any file yet.

1. Call splitCents(2, 4) and show the output.
2. Quote the BILL-4 sentence the property encodes.
3. Classify the failure as exactly one of:
   WRONG PROPERTY - the test asserts something the spec does not say,
   AMBIGUOUS SPEC - the spec allows more than one reading,
   REAL BUG - the output violates a clear spec sentence.
4. For REAL BUG: name the line in src/billing/split.ts that causes it and
   propose the fix. Also list which other BILL-4 properties the same root cause
   would break.
Stop after the classification and proposal. I decide the next step.

Prompt do skopiowania: audyt właściwości, które niczego nie sprawdzają

Review every property-based test under tests/ (test.prop, fc.assert, @given,
proptest!). Do not edit files. For each one report:
- the requirement ID it cites, or NONE,
- whether it reimplements the code under test (a test that recomputes the
  expected value with the same algorithm),
- whether its generator is narrower than the spec's input ranges,
- whether any .filter()/assume() discards most generated inputs,
- whether it could pass against an implementation that always returns an
  empty or constant result.
Finish with a table: test, verdict (KEEP / STRENGTHEN / DELETE), one-line reason.

Jak to uruchomić w Claude Code, Codex i Cursorze?

Biblioteki, testy i prompty są takie same we wszystkich trzech narzędziach. Różni się sposób instalacji skilla do testów właściwości, sposób trzymania agenta implementującego z dala od plików z właściwościami i sposób uruchomienia ekstrakcji w trybie headless. Polecenia sprawdzono 2026-09-26 na Claude Code 2.1.283, Codex CLI 0.157.1 i CLI skills 1.7.0.

Trail of Bits publikuje plugin property-based-testing (1.2.2), którego skill pisze i recenzuje testy właściwości dla Hypothesis, fast-check, proptest i innych bibliotek oraz klasyfikuje zredukowany kontrprzykład jako błędną właściwość, niejednoznaczną specyfikację albo prawdziwy błąd (README pluginu: „a wrong property, an ambiguous spec, or a real bug”, odczyt 2026-09-26). To ta sama klasyfikacja co w kroku 6 powyżej. To jeden skill, więc do czasu wywołania kosztuje w kontekście tylko swój opis.

Claude Code

Zainstaluj skill.

claude plugin marketplace add trailofbits/skills
claude plugin install property-based-testing@trailofbits

Wyciągnij niezmienniki nieinteraktywnie (tryb headless), z narzędziami tylko do odczytu, i zapisz wynik do swojej akceptacji:

# Terminal or CI, from the repository root
claude -p "$(cat prompts/extract-invariants.md)" \
  --allowedTools "Read,Grep,Glob" \
  --max-budget-usd 2 --output-format json > bill-4-invariants.json

Zablokuj właściwości na czas implementacji. Dodaj reguły deny do .claude/settings.json; działają w każdym trybie uprawnień:

{
  "permissions": {
    "deny": [
      "Edit(**/*.property.test.ts)",
      "Edit(**/test_*_properties.py)",
      "Edit(**/proptest-regressions/**)"
    ]
  }
}

Reguły deny nie zatrzymają skryptu, który sam zapisuje pliki; do tego dodaj ścieżki denyWrite sandboksa opisane w ochronie wyroczni.

Codex

Zainstaluj skill.

codex plugin marketplace add trailofbits/skills
codex plugin add property-based-testing@trailofbits

Wyciągnij niezmienniki nieinteraktywnie (tryb headless). Wystarczy sandbox tylko do odczytu, bo ekstrakcja nie zapisuje plików:

# Terminal or CI, from the repository root (Codex CLI 0.157.1)
codex exec --sandbox read-only -o bill-4-invariants.md "$(cat prompts/extract-invariants.md)"

Pętla implementacyjna. Użyj /goal z warunkiem w rodzaju every [BILL-4] property in tests/billing passes and no file under tests/ or proptest-regressions/ is modified. Nie polegaj na samym warunku: w pull requeście implementacyjnym niech CI oblewa zadanie, jeśli git diff --name-only origin/main... -- tests/ '**/proptest-regressions/**' cokolwiek wypisze (checkout w CI potrzebuje fetch-depth: 0 albo wcześniejszego pobrania origin/main). Blokady działające przed edycją opisuje ochrona wyroczni.

Cursor

Zainstaluj skill przez wieloagentowe CLI skills:

npx skills add trailofbits/skills --skill property-based-testing --agent cursor

Wyciągnij niezmienniki, wklejając pierwszy prompt do agenta w trybie Plan (Plan Mode), żeby najpierw przedstawił plan, zanim cokolwiek zapisze.

Pętla implementacyjna. Uruchom agenta implementującego w innym czacie niż ten, który napisał właściwości, żeby zaczynał bez rozumowania autora testów. Zanim przyjmiesz wynik, sprawdź, że git diff --name-only -- tests/ jest puste, i obejmij pliki z właściwościami wpisem w CODEOWNERS, żeby pull request, który je zmienia, wymagał wskazanego recenzenta. Hooki Cursora mogą zablokować edycję wcześniej; konfiguracja jest w ochronie wyroczni.

Skąd wiesz, że właściwości są wystarczająco mocne?

Nikt nie czyta każdego wygenerowanego wejścia, więc dowody muszą być mechaniczne:

• Każdy niezmiennik ma właściwość z identyfikatorem wymagania, a kontrola śledzenia oblewa build, gdy wymaganie nie ma testu.
• Każda właściwość ma kontrolę negatywną: celowe naruszenie, które zmieniło ją na czerwono, zapisane w pull requeście.
• Wynik mutacyjny modułu przekracza próg zespołu. Zestaw właściwości z wieloma przeżywającymi mutantami sprawdza mniej, niż się wydaje; zobacz siłę wyroczni.
• Przypięte kontrprzykłady są na miejscu i nietknięte, co potwierdza kontrola pochodzenia plików wyroczni.
• Przebieg nocny jest zielony albo jego błędy są sklasyfikowane w ciągu jednego dnia roboczego.

Programista odpowiedzialny za zmianę zatwierdza listę niezmienników i klasyfikację każdego kontrprzykładu. Tech lead odpowiada za ścieżki wyroczni i przebieg nocny. Zapisz wszystkie pięć punktów w pakiecie dowodów, żeby recenzent czytał dowody zamiast diffu.

Co się psuje przy testach właściwości z agentami?

Właściwość powtarza implementację. Agent pisze expect(splitCents(t, n)).toEqual(mySplit(t, n)), gdzie mySplit to ten sam algorytm. Oba mają ten sam błąd, a test zawsze przechodzi. Naprawa: sprawdzaj reguły, nie wyniki. Model referencyjny jest uprawniony tylko wtedy, gdy jest prostszy i niezależnie poprawny, na przykład stara funkcja albo implementacja metodą siłową (brute force).

Generator jest węższy niż specyfikacja. fc.integer({ min: 1, max: 100 }) dla kwoty, która może wynosić zero albo dziesięć milionów, nigdy nie sprawdza krańców. Naprawa: przepisz zakresy ze specyfikacji do generatora, a wartości brzegowe dodaj do examples lub @example.

Filtry wyrzucają większość wejść. .filter(t => t % n === 0) zostawia tylko łatwe kwoty, a biblioteka się poddaje albo prawie niczego nie testuje. Naprawa: buduj poprawne wejścia wprost (wygeneruj n i iloraz, pomnóż) zamiast je filtrować.

Agent osłabia właściwość, żeby było zielono. Luzuje <= 1 do <= 2, zawęża zakres albo usuwa przypięty przykład. Naprawa: pliki z właściwościami to pliki wyroczni objęte regułami deny i CODEOWNERS; edycja w tej samej zmianie oblewa kontrolę pochodzenia.

Hypothesis pada na limicie czasu, nie na logice. Domyślny limit 200 ms zamienia wolne pierwsze wywołanie w DeadlineExceeded lokalnie, a CI przechodzi, bo profil ci ustawia deadline=None. Naprawa: napraw prawdziwą powolność albo ustaw jawny deadline dla tego testu przez @settings.

Przebieg nocny ciągle niczego nie znajduje. W Hypothesis to zwykle profil ci bez losowości, powtarzający te same wejścia. Naprawa: załaduj profil z derandomize=False, jak pokazano wyżej.

Odtworzony błąd się nie powtarza. Seed i ścieżka z fast-check albo seed z proptest przestają pasować, gdy ktoś zmieni generator. Naprawa: przypinaj dosłowne wartości wejścia, nie tylko seed.

Dokąd dalej po testach właściwości

Rozwój sterowany specyfikacją Wymagania z identyfikatorami i kontrola śledzenia: źródło każdej właściwości.

Jak silna jest twoja wyrocznia? Wynik mutacyjny i kontrole negatywne, które pokazują, czy właściwości łapią błędy.

Ochrona wyroczni Reguły deny, ścieżki sandboksa i CODEOWNERS, które trzymają agentów z dala od plików z właściwościami.

Ocena przez model Sędziowie z rubryką dla zachowań, których nie wyrazi żaden niezmiennik.

Testy charakteryzacyjne Najpierw utrwal zachowanie legacy, potem użyj go jako modelu referencyjnego dla właściwości.

Pakiet dowodów Gdzie w każdym pull requeście trafiają mapa niezmienników, kontrole negatywne i przypięte przypadki.