ETNA workload for the Cedar-Lean formalization (cedar-policy/cedar-spec). Each variant reintroduces one historical bug fix by reverse-applying a patch against a fixed base commit and pairs it with a Plausible-driven property and a deterministic witness. Patches are the only durable per-variant artefact; no etna/<variant> git branches are used.
Per-property results
| Property | passed | failed | other | verdict |
|---|---|---|---|---|
DecimalParseNegativeSignPreserved | 6 | 4 | 0 | bug found |
DecimalParseNoUnderscore | 0 | 10 | 0 | bug found |
DefineEntityRejectsNonMember | 0 | 10 | 0 | bug found |
SchemaWellFormedNoSingletonBools | 9 | 1 | 0 | bug found |
SmtEncodeStringBalancedQuotes | 0 | 10 | 0 | bug found |
ValidateActionEntityNoAttrs | 10 | 0 | 0 | — |
ValidateRejectsUndeclaredEntities | 10 | 0 | 0 | — |
ValidateRequestPrincipalExists | 10 | 0 | 0 | — |
ValidateWithLevelAccepts | 2 | 8 | 0 | bug found |