CoChat
Sign Up
Cited by 3Software Testing and Debugging TechniquesLogic, programming, and type systemsFormal Methods in Verification

How We Built Cedar: A Verification-Guided Approach

Open access
Disselkoen, Craig, Eline, Aaron, He, Shaobo, Headley, Kyle, Hicks, Michael, Hietala, Kesha, Kastner, John, Mamat, Anwar +5 more·2024·Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering
DOI 10.1145/3663529.3663854
Open this paper in CoChat — free account

Abstract

This paper presents verification-guided development (VGD), a software engineering process we used to build Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves writing an executable model of the system and mechanically proving properties about the model; writing production code for the system and using differential random testing (DRT) to check that the production code matches the model; and using property-based testing (PBT) to check properties of unmodeled parts of the production code. Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing. While carrying out proofs, we found and fixed 4 bugs in Cedar’s policy validator, and DRT and PBT helped us find and fix 21 additional bugs in various parts of Cedar.

Verified 2026-10-24 · 2 references not checked yet

AI snapshot

Written from the paper’s full text.

TL;DR

The paper presents verification-guided development (VGD), the process used to build Cedar, an open-source authorization policy language. VGD combines Lean executable models and mechanized proofs with differential random testing (DRT) and property-based testing (PBT) of the Rust production code.

Key findings

  • While implementing the Lean model and proving soundness of Cedar’s policy validator, the team found and fixed 4 bugs; DRT and PBT found and fixed 21 additional bugs across Cedar components.
  • The Lean models total 1,673 LOC and Lean proofs 5,714 LOC, compared with 15,693 LOC of Rust production code and 20,458 LOC of Rust tests; the proof-to-model ratio is roughly 3.4:1.
  • DRT/PBT uncovered bugs including 6 parser-roundtrip bugs, 4 validator-parity bugs, 3 validation-soundness bugs, and 2 formatter-roundtrip bugs; RBAC authorizer parity and parser safety found 0.
  • Input generation mattered: for a typical DRT run, 35.5% of `when` condition-expressions from the type-directed ABAC generator were boolean literals, versus 9.7% for the added expression generator.

Methods

  • VGD has two parts: write readable executable Lean models of Cedar’s evaluator, authorizer, and validator, and prove properties such as forbid trumps permit, default deny, explicit allow, order independence, sound slicing, validation soundness, and termination.
  • DRT uses `cargo-fuzz` to generate millions of inputs—access requests, entities, and policies—and checks that the Rust production implementation agrees with the Lean model; PBT checks properties of production components with no Lean model or no proof yet.
  • Testing runs daily on Amazon ECS with 4096 CPU units (4 vCPUs) and 8GB memory, fuzzing each target for 6 hours; minimized corpus tests are saved for continuous integration.

Limitations

  • Stated in the paper: the testing framework missed a non-termination bug because the triggering input probability is extremely low, and it cannot find bugs outside the scope of its generators—for example, parser bugs from malformed policies because generators produce only syntactically correct policies.
  • Stated in the paper: the 6-hour fuzzing duration has no particular justification, though it ensures block coverage saturates or grows slowly near the end of a daily run; the authors plan to investigate optimal fuzzing duration.
  • Evident from the text: the Lean models are not fully feature complete—the parser is not modeled, unit tests were not ported to Lean, and the symbolic compiler model was still in progress—so proofs and DRT do not cover all Cedar components.

Model-written summary. Check it against the paper before relying on it.

Integrity signals

Registry

Crossref · 10.1145/3663529.3663854

Cites

34 of 37 references verified1 citation errors · 0 not checkable

Statistics

Nothing to recompute.

Claims the paper makes

4 of 11 cited sources checked · 4 supported · 0 flagged

  • Premisecitation
    § 1 INTRODUCTION · p. 1

    Cedar is a new, open-source authorization policy language.

    “Cedar [7, 11] is a new, open-source authorization policy language.”
    Quote in the paperSubstantial claim1 of 2 sources checked
    • cites [7] [7] cedar 2024. Cedar Language. https://www.cedarpolicy.com/en. -

      Not checked in the free run.

    • cites [11] [11] Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, and Andrew M. Wells. 2024. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. Proc. ACM Program. Lang. 8, OOPSLA1 (2024). - source
  • Premisecitation
    § 4.3 Experience · p. 5

    Complete line coverage alone does not guarantee effective testing.

    “Complete line coverage alone does not guarantee effective testing [4].”
    Quote in the paperSubstantial claim1 of 1 sources checked
    • cites [4] [4] Marcel Böhme, László Szekeres, and Jonathan Metzman. 2022. On the reliability of coverage-based fuzzer benchmarking. In Proceedings of the 44th International Conference on Software Engineering . 1621-1633. - source
  • Findingnone given
    § 3.2 Proofs of properties · p. 4

    Sound slicing: The policy slicing algorithm selects a slice (i.e., subset) of policies that produces the same authorization decision as the full policy set for a given request and entities.

    “Sound slicing : The policy slicing algorithm selects a slice (i.e., subset) of policies that produces the same authorization decision as the full policy set for a given request and entities.”
    Quote in the paperSubstantial claim
  • Findingreasoning
    § 2 THE CEDAR POLICY LANGUAGE · p. 3

    If the Cedar validator accepts a policy against a schema, then when requests conform to the schema, the policy's evaluation will never result in run-time type errors.

    “If the validator is satisfied, users can be sure that when requests conform to the schema, their policies' evaluation will never result in run-time type errors.”
    • Also stated in: § 3.2 Proofs of properties · p. 4 · plain
      “Validation soundness : If the validator accepts a policy, its evaluation will never result in a type error.”
    Quote in the paperSubstantial claim
  • Findingown data
    § 3.2 Proofs of properties · p. 4

    Order independence: The authorizer outputs the same decision regardless of policy evaluation order or duplicates.

    “Order independence : The authorizer outputs the same decision regardless of policy evaluation order or duplicates.”
    Quote in the paperSubstantial claim
  • May combine two claims. 22
  • Classified as probably not a substantial claim. 43

  • May combine two claims.

    Study design and conductcitation
    § 3 LEAN MODELS AND PROOFS · p. 3

    We wrote models of the Cedar evaluator, authorizer, and validator in Lean, and are in the process of writing one for the symbolic compiler.

    “We wrote models of the Cedar evaluator, authorizer, and validator in Lean [31], and are in the process of writing one for the symbolic compiler.”
    Quote in the paperSubstantial claim1 of 1 sources checked
    • cites [31] [31] Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In Automated Deduction-CADE 28: 28th International 29. Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28 . Springer, 625-635. - source

  • May combine two claims.

    Study design and conductcitation
    § 1 INTRODUCTION · p. 1

    The first part of VGD is constructing simple and readable formal models of Cedar's components in Lean and carrying out mechanized proofs to show they satisfy important correctness properties.

    “First, we construct simple and readable formal models of Cedar's components. We write these models in the Lean programming language [31], and carry out mechanized proofs to show that they satisfy important correctness properties.”
    Quote in the paperSubstantial claim1 of 1 sources checked
    • cites [31] [31] Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 theorem prover and programming language. In Automated Deduction-CADE 28: 28th International 29. Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings 28 . Springer, 625-635. - source

  • May combine two claims.

    Findingown data
    § 4.1 Input generation · p. 4

    The type-directed generator produces more complicated inputs, like set operations, than the non type-directed version, leading to deeper coverage of core logic and faster bug discovery.

    “The type-directed generator produces more complicated inputs, like set operations, than the non type-directed version, leading to deeper coverage of core logic and faster bug discovery.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingreasoning
    § 4.1 Input generation · p. 4

    Naïve input generation is insufficient: if policies, entity stores, and requests are generated independently, policies are likely to be ill-typed and to reference non-existent entities or attributes, over-exercising error-handling code and failing to cover much of a component's core logic.

    “Naïve input generation is insufficient: If we randomly generate a policy, entity store, and request independently , policies are likely to be ill-typed and to reference non-existent entities or attributes. This would over-exercise errorhandling code and fail to cover much of a component's core logic.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Findingown data
    § 4.3 Experience · p. 5

    Differential testing against the Lean model helped us find a bug in a Rust package we used for parsing IP addresses, which motivated us to write our own IP address parser.

    “As one example, differential testing against the Lean model helped us find a bug in a Rust package we used for parsing IP addresses. This finding eventually motivated us to write our own IP address parser, replacing the buggy external package.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Findingown data
    § 3.2 Proofs of properties · p. 4

    Our Lean proofs are fast to verify, and the models are fast to execute. It takes about 3 minutes to check all proofs and compile models for execution.

    “Our Lean proofs are fast to verify, and the models are fast to execute. It takes about 3 minutes to check all proofs and compile models for execution.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Findingown data
    § 3.2 Proofs of properties · p. 4

    During differential testing, the median execution time for the Lean authorizer is 6 microseconds, compared to 10 microseconds for Rust.

    “During differential testing, the median execution time for the Lean authorizer is 6 microseconds, compared to 10 microseconds for Rust.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § 3.1 A human-readable specification · p. 3

    We found three other bugs while attempting to carry out the validator soundness proof.

    “We also found three other bugs while attempting to carry out the validator soundness proof.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingreasoning
    § 3.1 A human-readable specification · p. 3

    The Lean code for the Cedar authorizer naturally expresses the logic that an authorization decision is allowed as long as some permit policy is satisfied and no forbid policies are.

    “This code naturally expresses the logic that an authorization decision is allowed as long as some permit policy is satisfied and no forbid policies are.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § 4.3 Experience · p. 5

    Property testing helped us uncover subtle bugs in the Cedar policy parser, in how the formatter handles comments, and how namespace prefixes on application data are interpreted.

    “Property testing helped us uncover subtle bugs in the Cedar policy parser, in how the formatter handles comments, and how namespace prefixes on application data (e.g., TinyTodo::List::”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data
    § 3.2 Proofs of properties · p. 4

    Our total proof-to-model ratio is roughly 3.4:1.

    “Our total proof-to-model ratio is roughly 3 . 4 : 1 (see Table 1).”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingown data
    § 4.3 Experience · p. 5

    An unreleased early version of Cedar provided a method to get the size of a string; the model and production code had different implementations (using bytes vs. codepoints vs. graphemes), causing DRT to fail, and we eventually dropped this feature.

    “For example, an unreleased early version of Cedar provided a method to get the size of a string. The model and production code ended up having different implementations (using bytes vs. codepoints vs. graphemes), causing DRT to fail. We eventually dropped this feature after agreeing that it confuses users more than it benefits them.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The parser did not parse namespaced extension function names correctly.

    “The parser did not parse namespaced extension function names correctly”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The Rust implementation incorrectly handled policies containing certain types of records.

    “The Rust implementation incorrectly handled policies containing certain types of records”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    Pretty-printing did not consistently add parentheses to negation operations.

    “Pretty-printing did not consistently add parentheses to negation operations”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingcitation
    § REFERENCES · p. 8

    The Rust implementation and definitional model disagreed on the type of resource in [] when resource has unspecified entity type.

    “The Rust implementation and definitional model disagreed on the type of resource in [] when resource has unspecified entity type”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The validator did not parse extension function call arguments correctly.

    “The validator did not parse extension function call arguments correctly”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The Rust implementation and definitional model computed string sizes differently.

    “The Rust implementation and definitional model computed string sizes differently”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    Pretty-printing certain function call ASTs resulted in a crash.

    “Pretty-printing certain function call ASTs resulted in a crash”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingown data
    § A TROPHY AND ANTI-TROPHY CASES · p. 8

    Some bugs were fixed on earlier versions of Cedar, prior to open-sourcing.

    “Items without links were fixed on earlier versions of Cedar, prior to open-sourcing.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingcitation
    § REFERENCES · p. 8

    Comments could be dropped in an is expression.

    “Comments could be dropped in an is expression”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The parser did not parse the pattern literals of the like operation correctly.

    “The parser did not parse the pattern literals of the like operation correctly”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    Comments on records were dropped by the formatter.

    “Comments on records were dropped by the formatter”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The Rust implementation supported embedding IPv4 addresses in IPv6 addresses while the definitional model did not.

    “The Rust implementation supported embedding IPv4 addresses in IPv6 addresses while the definitional model did not”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § A TROPHY AND ANTI-TROPHY CASES · p. 9

    The validator did not terminate on certain inputs.

    “The validator did not terminate on certain inputs”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § A TROPHY AND ANTI-TROPHY CASES · p. 8

    All bugs listed in the appendix have been promptly fixed by Cedar developers.

    “In this appendix, we list trophy (bugs found) and anti-trophy (bugs missed) cases of DRT and PBT, all of which have been promptly fixed by Cedar developers.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § A TROPHY AND ANTI-TROPHY CASES · p. 9

    The JSON schema parser accepted inputs with unknown attributes.

    “The JSON schema parser accepted inputs with unknown attributes”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    The Rust implementation and definitional model named extension functions differently (e.g., lt vs. lessThan).

    “The Rust implementation and definitional model named extension functions differently (e.g., lt vs. lessThan )”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    The Rust implementation and definitional model named extension functions differently (e.g., ipaddr vs. IPAddr).

    “The Rust implementation and definitional model named extension functions differently (e.g., ipaddr vs. IPAddr )”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    The Rust implementation required the operands of the isInRange extension function to be both IPv4 or IPv6 addresses while the definitional model did not.

    “The Rust implementation required the operands of the isInRange extension function to be both IPv4 or IPv6 addresses while the definitional model did not”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Findingreasoning
    § 4.3 Experience · p. 5

    Integration tests allowed us to fix these bugs before pushing the code, avoiding the delay for the daily DRT run to uncover them.

    “Integration tests allowed us to fix these bugs before pushing the code, avoiding the delay for the daily DRT run to uncover them.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    The parser performed constant folding incorrectly.

    “The parser performed constant folding incorrectly”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Findingnone given
    § REFERENCES · p. 8

    The Rust implementation incorrectly rejected certain policies with schemas containing unspecified entity types.

    “The Rust implementation incorrectly rejected certain policies with schemas containing unspecified entity types”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The validator ignored certain entity type namespaces.

    “The validator ignored certain entity type namespaces”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The parser did not unescape raw strings.

    “The parser did not unescape raw strings”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Findingnone given
    § REFERENCES · p. 8

    The validator did not correctly typecheck certain has expressions.

    “The validator did not correctly typecheck certain has expressions”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Interpretationnone given
    § 1 INTRODUCTION · p. 1

    Cedar policies are separate from application code, so they can be independently authored, updated, analyzed, and audited.

    “Because Cedar policies are separate from application code, they can be independently authored, updated, analyzed, and audited.”
    Quote in the paperNot a substantial claim

  • Classified as probably not a substantial claim.

    Study design and conductcitation
    § 4 DIFFERENTIAL RANDOM TESTING · p. 4

    The second part of VGD is to use differential random testing to increase confidence that the behavior of formal models matches that of production code.

    “The second part of the verification-guided development process is to use differential random testing [29] to increase our confidence that the behavior of our formal models matches that of our production code.”
    Quote in the paperSubstantial claim0 of 1 sources checked
    • cites [29] [29] William M McKeeman. 1998. Differential testing for software. Digital Technical Journal 10, 1 (1998), 100-107. -

  • Probably not a substantial claim: may not pass S3 (load-bearing). May combine two claims.

    Premisenone given
    § 2 THE CEDAR POLICY LANGUAGE · p. 2

    The Cedar authorizer returns Deny if no permit policy is satisfied or if any forbid policy is satisfied; it returns Allow if at least one permit policy is satisfied and no forbid policies are.

    “The authorizer returns decision Deny if no permit policy is satisfied or if any forbid policy is satisfied. It returns Allow if at least one permit policy is satisfied and no forbid policies are.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisenone given
    § 2 THE CEDAR POLICY LANGUAGE · p. 3

    When a policy evaluation results in a dynamic type error, the erroring policy does not factor into the final authorization decision-it is ignored.

    “When this happens, the erroring policy does not factor into the final authorization decision-it is ignored.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationreasoning
    § 4 DIFFERENTIAL RANDOM TESTING · p. 4

    PBT is complementary to DRT because it allows testing properties we have yet to prove in Lean, and those of production components for which no model exists.

    “PBT is complementary to DRT because it allows us to test properties we have yet to prove in Lean, and those of production components (such as the Cedar policy parser) for which no model exists.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisenone given
    § 2 THE CEDAR POLICY LANGUAGE · p. 2

    Cedar supports indexing policies so that they can quickly be sliced to a subset relevant to a particular request.

    “Cedar supports indexing policies so that they be can quickly sliced to a subset relevant to a particular request.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing).

    Premisenone given
    § 3.1 A human-readable specification · p. 3

    Lean allows us to write concise specifications.

    “Lean allows us to write concise specifications.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationreasoning
    § 3.1 A human-readable specification · p. 3

    Lean is a purely functional language with algebraic data types, so it was easy to directly express Cedar's evaluator, validator, and symbolic compiler as recursive functions over abstract syntax trees.

    “Lean is a purely functional language with algebraic data types, so it was easy to directly express Cedar's evaluator, validator, and symbolic compiler as recursive functions over abstract syntax trees.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Premisecitation
    § 2 THE CEDAR POLICY LANGUAGE · p. 3

    The Cedar symbolic compiler translates Cedar policies to SMT-lib, producing an encoding that is sound, complete, and decidable.

    “The Cedar symbolic compiler translates Cedar policies to SMT-lib [2], the language of SMTsolvers, producing an encoding that is sound, complete, and decidable.”
    Quote in the paperSubstantial claim0 of 1 sources checked
    • cites [2] [2] Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2016. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org . -

      Not checked in the free run.

  • Probably not a substantial claim: may not pass S2 (checkable), S4 (based).

    Interpretationreasoning
    § 1 INTRODUCTION · p. 2

    VGD provides a practical balance of competing concerns around high assurance, ease of development, and maintainability.

    “VGD provides a practical balance of competing concerns around high assurance, ease of development, and maintainability.”
    Quote in the paperNot a substantial claim

  • May combine two claims.

    Interpretationown data
    § ABSTRACT · p. 1

    Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing.

    “Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Premisereasoning
    § 3.1 A human-readable specification · p. 3

    Lean requires all recursive definitions to be well-founded, which complicates modeling of complex recursive structures.

    “Lean requires all recursive definitions to be well-founded (so functions always terminate), which complicates modeling of complex recursive structures.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim. May combine two claims.

    Interpretationreasoning
    § 3.2 Proofs of properties · p. 4

    Properties 1-4 capture how authorization decisions are made, and their proofs give a simple, declarative specification of Cedar's authorization behavior, complementing the executable specification provided by the model.

    “Properties 1-4 capture how authorization decisions are made. Their proofs give us a simple, declarative specification of Cedar's authorization behavior, complementing the executable specification provided by the model.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Premisereasoning
    § 3.1 A human-readable specification · p. 3

    While Rust lets us represent Cedar values as a recursive datatype over built-in sets and maps, Lean prohibits doing so for its standard set and map datatypes because their invariants introduce circular reasoning.

    “While Rust lets us represent Cedar values as a recursive datatype over built-in sets and maps, Lean prohibits doing so for its standard set and map datatypes because their invariants introduce circular (not well-founded) reasoning.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Study design and conductnone given
    § 4 DIFFERENTIAL RANDOM TESTING · p. 4

    If the Lean model and Rust production implementation agree on the output for generated inputs, then we obtain evidence that Rust production code is on par with the Lean model; if they disagree, then we have found a bug.

    “If the two versions agree on the output, then we obtain a piece of evidence that Rust production code is on par with the Lean model. If they disagree, then we have found a bug (e.g., production code incorrectly implements the specification).”
    Quote in the paperSubstantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing).

    Premisecitation
    § 2 THE CEDAR POLICY LANGUAGE · p. 2

    Cedar is a language for writing authorization policies, supporting idioms in the style of role-based access control (RBAC) and attribute-based access control (ABAC) and their combination.

    “Cedar is a language for writing authorization policies, supporting idioms in the style of role-based access control (RBAC) [14], attribute-based access control (ABAC) [20], and their combination.”
    Quote in the paperNot a substantial claim0 of 2 sources checked
    • cites [14] [14] David F. Ferraiolo and D. Richard Kuhn. 1992. Role-Based Access Control. In 15th National Computer Security Conference . -

      Not checked in the free run.

    • cites [20] [20] Vincent C. Hu, D. Richard Kuhn, David F. Ferraiolo, and Jeffrey Voas. 2015. Attribute-Based Access Control. Computer 48, 2 (2015), 85-88. https://doi.org/ 10.1109/MC.2015.33 - source

  • Classified as probably not a substantial claim.

    Premisenone given
    § 4.3 Experience · p. 5

    The same lines of code executed with different program state can lead to very different outcomes.

    “The same lines of code executed with different program state can lead to very different outcomes.”
    Quote in the paperSubstantial claim

  • Classified as probably not a substantial claim.

    Interpretationreasoning
    § 5 RELATED WORK · p. 6

    Extracted code from the Lean model would be challenging to maintain and operate, e.g., when debugging broader system failures in deployment, because it is not intended to be readable.

    “such extracted code would be challenging to maintain and operate, e.g., when debugging broader system failures in deployment, because it is not intended to be readable.”
    Quote in the paperSubstantial claim

  • May combine two claims.

    Interpretationreasoning
    § 6 CONCLUSION · p. 6

    VGD is a practical approach for developing high-assurance code: it leverages the benefits of formal methods while producing code that is easy to use, develop, and maintain.

    “Our experience shows that VGD is a practical approach for developing high-assurance code: it leverages the benefits of formal methods while producing code that is easy to use, develop, and maintain.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based). May combine two claims.

    Interpretationnone given
    § 6 CONCLUSION · p. 6

    Our proof effort leverages Lean's extensive theorem libraries, interactive IDE support, and fast verification.

    “Our proof effort leverages Lean's extensive theorem libraries, interactive IDE support, and fast verification.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S2 (checkable), S3 (load-bearing), S4 (based).

    Interpretationnone given
    § 5 RELATED WORK · p. 6

    Developing industrial-strength code in Lean (or any PPL) is challenging because of its limited library support and limited base of developer expertise, compared to a mainstream language.

    “Even with such a compiler, developing industrial-strength code in Lean (or indeed, any PPL) is challenging because of its limited library support and limited base of developer expertise, compared to a mainstream language.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S3 (load-bearing), S4 (based).

    Study design and conductnone given
    § 6 CONCLUSION · p. 6

    Our DRT/PBT input generators are carefully crafted to achieve good code coverage and balanced input distributions.

    “Our DRT/PBT input generators are carefully crafted to achieve good code coverage and balanced input distributions.”
    Quote in the paperNot a substantial claim

  • Probably not a substantial claim: may not pass S4 (based).

    Interpretationnone given
    § 4.3 Experience · p. 5

    The probability of generating inputs triggering the non-termination bug is extremely low.

    “The reason for this is that the probability of generating inputs triggering this bug is extremely low.”
    Quote in the paperNot a substantial claim
59 of 59

  • The authors state this as an assumption.

    The Lean models serve as Cedar's specification.

    “The models serve as Cedar's specification”

  • The paper relies on this without support.

    String handling logic (e.g., unescaping raw strings) is non-trivial and error-prone.

    “because string handling logic (e.g., unescaping raw strings) is non-trivial and error-prone.”

  • The paper relies on this without support.

    The tools OpenJML, Krakatoa, Aeneas, Kani, Prusti, Creusot, Verus have limitations in scope, scalability, and tooling that prevent their use on an industrial scale.

    “However, these tools have limitations in scope, scalability, and tooling that prevent their use on an industrial scale.”
3 of 3

Cites

Flagged first, then by citations

Research works printed but not linked: 2

  1. David F. Ferraiolo and D. Richard Kuhn. 1992. Role-Based Access Control. In 15th National Computer Security Conference.
  2. Xavier Leroy, Sandrine Blazy, Daniel Kästner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert-a formally verified optimizing compiler. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress.

Cited by

Sorted by citations

Related

Authors
Disselkoen, C., Eline, A., He, S., Headley, K., Hicks, M., Hietala, K., Kastner, J., Mamat, A., McCutchen, M., Rungta, N., Shah, B., Torlak, E., & Wells, A.
Affiliations
  • Amazon (United States) (US)
  • Unaffiliated, Arlington, United States
  • University of Maryland, College Park (US)
  • University of Chicago (US)
ORCID
Venue
Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering
Publisher
ACM
Published
2024-07-10
Pages
351-357
DOI
10.1145/3663529.3663854
OpenAlex
W4400484855
Cited by
3
References
21
Citations by year
2025: 2 · 2024: 1
FWCI
0.83
Type
conference paper
Language
en
Open access
Licence
Locations
  • arXiv (Cornell University) (submittedVersion, cc-by)
  • arXiv (Cornell University) (cc-by)
Topics
  • Physical Sciences › Computer Science › Software › Software Testing and Debugging Techniques
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Computational Theory and Mathematics › Formal Methods in Verification
Keywords
executable models, mechanical proof, property-based testing, policy verification, bug detection, software verification

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Claims read by deepseek-v4.1-flash under definition version 3 (extract-v3) on 2026-10-24.

Classified by jev-1.13-20260917 (gold-guideline-v0.2) on 2026-10-24.

Cited sources are checked by gpt-6-sol.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review