Back

VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

Chuyue SunYican SunEthan ZhangDaneshvar AmrollahiShuvendu LahiriShan LuDavid DillClark Barrett

article2026International Conference on Tools and Algorithms for Construction and Analysis of Systems8 citations

Presents VeriStruct, an automated framework that scales AI-assisted formal verification to complex Rust data-structure modules in Verus by combining structured proof planning with syntax-guided error repair to achieve a 99.2% verification success rate.

Listen

As software development increasingly relies on artificial intelligence, systems face growing risks of critical correctness bugs and security vulnerabilities. Formal program verification can mathematically prove that software is free of such defects, but its real-world adoption has been severely limited by the high human expertise and effort required to write complex mathematical annotations. While recent artificial intelligence approaches have automated simple, single-function verification, they struggle with data-structure modules, which are foundational components across software systems that require coordinated reasoning across multiple methods.

The article introduces and evaluates VeriStruct, an artificial intelligence–assisted framework designed to automate the formal verification of multi-method Rust data-structure modules within the Verus verification ecosystem.

VeriStruct uses a structured, two-stage approach that takes standard Rust code and a unit test suite as inputs. First, an automated planning module determines the necessary verification artifacts—such as mathematical representations (views), shared structural invariants, method contracts, and proof hints—and generates an initial draft using targeted language model prompts enriched with formal syntax rules. Second, when the Verus verifier detects failures, VeriStruct executes an automated repair loop that uses pattern matching on error messages to apply specialized fixes, including correcting state mutability, adjusting contract strengths, and resolving syntax mismatches.

Across an evaluation of 11 diverse Rust data-structure benchmarks encompassing 129 functions, VeriStruct fully verified 10 out of 11 modules and 128 out of 129 total functions (a 99.2% success rate). In contrast, a single-prompt baseline solved only 4 modules (52 functions), and an advanced tool-using coding agent solved 8 modules (102 functions). VeriStruct achieved these superior results while consuming slightly fewer computational tokens than the autonomous coding agent. Additionally, an in-depth case study showed that the framework discovered simpler, more concise mathematical representations than those originally written by human experts.

These findings demonstrate that structured, multi-stage artificial intelligence pipelines can overcome the reasoning limitations of language models in complex software verification tasks. Automating this process dramatically reduces manual engineering overhead, lowers development costs, and shortens verification timelines. Most importantly, it creates a practical pathway for establishing mathematically verified, high-assurance software libraries, mitigating the systemic security and reliability risks introduced by unverified code.

Based on these results, software engineering teams should adopt structured planning-and-repair frameworks to verify reusable foundational data structures. To further scale the approach, future development should incorporate automated test generation to eliminate the manual burden of writing unit tests, integrate retrieval-augmented generation to leverage existing mathematical proof libraries, and explore reinforcement learning to improve contract synthesis.

The current evaluation is limited to a benchmark suite of 11 Rust data-structure modules and relies on user-provided unit test suites to establish intended behavior. While confidence in the evaluated domain is high, broader deployment on more complex, large-scale concurrent systems will require additional validation and expanded verification capabilities.

MicrosoftPeking UniversityStanford Universitylarge language modelsverification methodautomatic verificationVeriStructdata-structure modulesVerus
arXiv: 2510.25015ChuyueSun/VeriStruct
  • Paper: VeruSAGE: A Study of Agent-Based Verification for Rust Systems, Chenyuan Yang et al. (2025). Its study of agent frameworks automating Verus proofs in real Rust systems establishes the immediate research context that VeriStruct advances from functions to data-structure modules.
  • Paper: seL4: formal verification of an OS kernel, Gerwin Klein et al. (2009). Its end-to-end machine-checked verification of a production Rust kernel grounds VeriStruct’s goal of making formal guarantees practical for systems software.
Cover for VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus

Abstract

We introduce VeriStruct, a novel framework that extends AI-assisted automated verification from single functions to more complex data structure modules in Verus. VeriStruct employs a planner module to orchestrate the systematic generation of abstractions, type invariants, specifications, and proof code. To address the challenge that LLMs often misunderstand Verus' annotation syntax and verification-specific semantics, VeriStruct embeds syntax guidance within prompts and includes a repair stage to automatically correct annotation errors. In an evaluation on eleven Rust data structure modules, VeriStruct succeeds on ten of the eleven, successfully verifying 128 out of 129 functions (99.2%) in total. These results represent an important step toward the goal of automatic AI-assisted formal verification.

Topics

large language modelsverification methodautomatic verificationverification techniquessyntacticsverification process

Keywords

VeriStructdata-structure modulesVerusspecification generationproof generationverification annotationsLLM-based unit test generation

Table of Contents

  • 1 Introduction
  • 2 Preliminaries: Verifying a Data-Structure in Verus
  • 3 The VeriStruct Workflow
  • 4 Stage 1: Generating the Annotations
  • 5 Stage 2: Repairing the Annotations
  • 6 Evaluation
  • 7 Related Work
  • 8 Conclusion and Future Work
  • References
  • 0.A Supplementary Material

Knowls

  1. Knowl 1 — VeriStruct verifies data-structure modules through generation and repair

    model/method

    VeriStruct takes an unannotated Rust data-structure implementation and a unit-test suite describing expected usage and behavior. It first generates verification annotations, then repeatedly invokes the Verus verifier and repairs annotations in response to verifier errors. The implementation and tests remain unchanged during this workflow. If verification succeeds, VeriStruct returns the annotated code; the tests help align specifications with intended behavior and guard against trivial or vacuous specifications.

  2. Knowl 2 — A planner schedules specialized annotation-generation modules

    model/method

    VeriStruct uses four specialized generation modules: a View module for mathematical abstractions, a type-invariant module, a specification module for specification functions and preconditions and postconditions, and a proof-block module for proof code and loop invariants. The usual dependency order is View, type invariant, specifications, then proof blocks. Before generation, a planner selects which modules are needed: it is guided to request a View when the structure can be represented as a sequence, set, or map; a type invariant when fields have nontrivial relationships; and proof blocks whenever a type invariant is requested. Each selected module is run sequentially. For robustness, each invocation generates multiple candidates, and VeriStruct keeps the candidate that verifies the greatest number of functions.

  3. Knowl 3 — View refinement seeks an abstract, compact logical representation

    model/method

    VeriStruct generates a Verus View implementation to map concrete data-structure state to a logical representation, then can prompt the language model to refine that representation toward fewer, more abstract components. For a ring buffer, the refined view represents the stored elements in logical order as a sequence and includes the capacity, while hiding the concrete head and tail indices. The sequence is formed from one contiguous slice when the tail follows the head, or from the concatenation of the end and beginning slices when the buffer wraps around. This avoids exposing circular-index arithmetic in later specifications. The paper also reports a Bitmap case in which the generated view differs from the human-written one: the generated solution models the bitmap as a single sequence and uses Verus sequence APIs, rather than modeling each 64-bit block as a 64-bit bit sequence in a two-dimensional representation with auxiliary functions.

  4. Knowl 4 — Module-specific prompts provide Verus syntax and semantic guidance

    model/method

    Each VeriStruct generation prompt combines a task objective, module-specific Verus guidance, step-by-step instructions, examples, and the target code and tests. The guidance is drawn from the Verus tutorial and standard-library documentation and is tailored to the annotation being generated. For example, View prompts explain relevant logical types and syntax; specification prompts address Rust mutability and the use of old-state values in preconditions; and proof prompts direct the model to bring type invariants into proof contexts and use relevant lemmas. The prompts are designed to mitigate errors caused by the model confusing Verus specification functions with executable functions or misunderstanding other verification-specific syntax and semantics.

  5. Knowl 5 — Verifier-directed repair iteratively routes errors to specialized modules

    algorithm

    The repair procedure receives annotated code and tests, a maximum of mm repair rounds, and nn samples per repair-module invocation. In each round, it runs Verus and obtains the highest-priority error. If there is no error, it returns success and the code. Otherwise, it matches the error against predefined patterns and invokes the corresponding repair module; if no pattern matches, it invokes a fallback module prompted with the verifier error. It generates nn candidate repairs and retains the candidate verifying the most functions. After mm unsuccessful rounds, it returns failure and the final code. The implemented repair categories cover syntax, type mismatches, arithmetic overflow or underflow, precondition and postcondition failures, loop-invariant failures, missing imports or trait elements, mode and visibility errors, missing old-state references, failed assertions, decreases obligations, and redundant invariant invocations.

  6. Knowl 6 — Failed test assertions can trigger interprocedural contract strengthening

    model/method

    For a verifier error caused by a failed test assertion, VeriStruct's repair module examines the failing assertion, identifies the method called immediately before it, and asks the language model to strengthen that method's postcondition so the assertion follows from the contract. This repair requires reasoning across the method and its caller's test, rather than repairing only a local proof block. The test suite therefore contributes both examples of intended behavior and feedback for refining specifications across method boundaries.

  7. Knowl 7 — Evaluation covers eleven diverse Rust data-structure modules

    experimental setup

    The evaluation uses eleven Rust modules sourced from the Verus repository and other open-source repositories: Atomics (an atomic counter), Bitmap (a bitmap over 64-bit words), Treemap (an ordered binary-search-tree map), Invariants (reusable invariants for concurrent routines), Node (a binary-search-tree node), Option (a polymorphic option wrapper), RingBuffer, RwLockVstd (a read/write lock), SetFromVec (a set abstraction backed by vectors), Transfer (balanced account transfers), and Vectors (a vector implementation with basic algorithms). The benchmark versions were modified to include more complete specifications, additional methods, and unit tests; the authors report that these versions do not occur verbatim in the o1-2024-12-17 training snapshot. The experiments used OpenAI o1 for VeriStruct and the baseline, with three samples per module invocation and at most five repair rounds. They ran on Ubuntu 22.04.5 with a 24-core Intel Core i9-12900K and 64 GB RAM.

  8. Knowl 8 — VeriStruct verifies more benchmarks and functions than the comparison systems

    empirical result

    Across the eleven benchmarks, VeriStruct solves 10 benchmarks and verifies 128 of 129 functions (99.2%); on the only unsolved benchmark, Node, it verifies 11 of 12 functions. A baseline that iteratively prompts the LLM to generate annotations, without VeriStruct's structured generation-and-repair workflow, solves 4 benchmarks and verifies 52 functions. Claude Code configured with Claude Sonnet 4.5 and access to the Verus verifier solves 8 benchmarks and verifies 102 functions. VeriStruct's 10 solved benchmarks and 128 verified functions correspond to reported gains of 150.0% and 146.2%, respectively, over the baseline. Average token use was approximately 22k per benchmark for VeriStruct and 24k for Claude Code.

  9. Knowl 9 — Per-benchmark time and invocation counts show varied verification costs

    data/table

    The following are VeriStruct's reported evaluation statistics; time is in minutes, and calls are LLM invocations. Each entry gives benchmark, functions to verify, time, calls, and outcome: Atomics, 11, 2.1, 8, solved; Bitmap, 14, 12.2, 13, solved; Treemap, 21, 0.3, 6, solved; Invariants, 7, 1.5, 4, solved; Node, 12, 10.4, 12, not fully solved (11/12 verified); Option, 15, 2.6, 3, solved; RingBuffer, 13, 4.2, 12, solved; RwLockVstd, 5, 6.4, 3, solved; SetFromVec, 10, 9.1, 13, solved; Transfer, 5, 1.2, 4, solved; Vectors, 16, 3.1, 6, solved. Treemap required the least reported time (0.3 minutes), while Bitmap required the most (12.2 minutes); Bitmap and SetFromVec used the maximum reported number of calls, 13.

  10. Knowl 10 — The workflow currently depends on a comprehensive user-provided test suite

    limitation

    VeriStruct requires a unit-test suite as input. The authors identify creating tests with high coverage, including corner cases, as time-consuming and error-prone; incomplete tests can also limit the behavioral guidance available for specification generation and repair. Although LLM-assisted techniques were used to generate test cases during the work, integrating automatic unit-test generation into VeriStruct itself is presented as future work.

Coverage note — Future directions such as retrieval-augmented generation, resource-algebra synthesis, constrained decoding, and reinforcement learning are omitted because the paper proposes them but does not evaluate them as contributions.

References

  1. 1.Artifact of veristruct (2025), https://github.com/ChuyueSun/VeriStruct
  2. 2.Anthropic: Claude code. https://claude.ai/claude-code (2025), accessed: 2025
  3. 3.Barrett, C., Boyd, B., Bursztein, E., Carlini, N., Chen, B., Choi, J., Chowdhury, A.R., Christodorescu, M., Datta, A., Feizi, S., Fisher, K., Hashimoto, T., Hendrycks, D., Jha, S., Kang, D., Kerschbaum, F., Mitchell, E., Mitchell, J., Ramzan, Z., Shams, K., Song, D., Taly, A., Yang, D.: Identifying and mitigating the security risks of generative ai. Foundations and Trends in Privacy and Security 6(1), 1–52 (2023). https://doi.org/10.1561/3300000041, http://dx.doi.org/10.1561/3300000041
  4. 4.Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, chap. 33, pp. 825–885. IOS Press (Feb 2021), http://theory.stanford.edu/~barrett/pubs/BSST21.pdf
  5. 5.Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) Proceedings of the 10th International Conference on Software Engineering and Formal Methods (SEFM 2012). Lecture Notes in Computer Science, vol. 7504, pp. 233–247. Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16
  6. 6.Dong, Q., Li, L., Dai, D., Zheng, C., Ma, J., Li, R., Xia, H., Xu, J., Wu, Z., Liu, T., et al.: A survey on in-context learning. arXiv preprint arXiv:2301.00234 (2022)
  7. 7.Filliâtre, J.C., Paskevich, A.: Why3. https://why3.lri.fr (2024), version 1.6.0
  8. 8.Fu, Y., Baker, E., Ding, Y., Chen, Y.: Constrained decoding for secure code generation. arXiv preprint arXiv:2405.00218 (2024)
  9. 9.Kamath, A., Senthilnathan, A., Chakraborty, S., Deligiannis, P., Lahiri, S.K., Lal, A., Rastogi, A., Roy, S., Sharma, R.: Finding inductive loop invariants using large language models. arXiv preprint arXiv:2311.07948 (2023)
  10. 10.Knuth, D.E.: The Art of Computer Programming, Volume 1: Fundamental Algorithms. Addison-Wesley (1997)
  11. 11.Lahiri, S.K.: Evaluating llm-driven user-intent formalization for verification-aware languages. In: CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN–FMCAD 2024. p. 142 (2024)
  12. 12.Lattuada, A., Hance, T., Bosamiya, J., Brun, M., Cho, C., LeBlanc, H., Srinivasan, P., Achermann, R., Chajed, T., Hawblitzel, C., Howell, J., Lorch, J.R., Padon, O., Parno, B.: Verus: A practical foundation for systems verification. In: Proceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles. p. 438–454. SOSP ’24, Association for Computing Machinery, New York, NY, USA (2024). https://doi.org/10.1145/3694715.3695952, https://doi.org/10.1145/3694715.3695952
  13. 13.Lattuada, A., Hance, T., Cho, C., Brun, M., Subasinghe, I., Zhou, Y., Howell, J., Parno, B., Hawblitzel, C.: Verus: Verifying Rust programs using linear ghost types. Proceedings of the ACM on Programming Languages (2023). https://doi.org/10.1145/3586037
  14. 14.Lattuada, A., Parno, B., Bosamiya, J., Hawblitzel, C., Hance, T., et al.: vstd: Verus standard library. https://github.com/verus-lang/verus/tree/main/vstd (Jun 2024), version 0.0.0, MIT License
  15. 15.Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2010). Lecture Notes in Computer Science, vol. 6355, pp. 348–370. Springer, Berlin, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20
  16. 16.Levy, A., Campbell, B., Ghena, B., Giffin, D.B., Pannuto, P., Dutta, P., Levis, P.: Multiprogramming a 64kb computer safely and efficiently. In: Proceedings of the 26th Symposium on Operating Systems Principles. p. 234–251. SOSP ’17, Association for Computing Machinery, New York, NY, USA (2017). https://doi.org/10.1145/3132747.3132786, https://doi.org/10.1145/3132747.3132786
  17. 17.Lewis, P., Perez, E., Piktus, A., Petroni, F., Karpukhin, V., Goyal, N., Küttler, H., Lewis, M., Yih, W.t., Rocktäschel, T., Riedel, S., Kiela, D.: Retrieval-augmented generation for knowledge-intensive nlp tasks. In: Proceedings of the 34th International Conference on Neural Information Processing Systems. NIPS ’20, Curran Associates Inc., Red Hook, NY, USA (2020)
  18. 18.Liu, K., Chen, Z., Liu, Y., Zhang, J.M., Harman, M., Han, Y., Ma, Y., Dong, Y., Li, G., Huang, G.: Llm-powered test case generation for detecting bugs in plausible programs (2025), https://arxiv.org/abs/2404.10304
  19. 19.Miltner, A., Padhi, S., Millstein, T., Walker, D.: Data-driven inference of representation invariants. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 1–15. PLDI 2020, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3385412.3385967, https://doi.org/10.1145/3385412.3385967
  20. 20.Misu, M.R.H., Lopes, C.V., Ma, I., Noble, J.: Towards ai-assisted synthesis of verified Dafny methods. Proc. ACM Softw. Eng. 1(FSE) (Jul 2024). https://doi.org/10.1145/3643763, https://doi.org/10.1145/3643763
  21. 21.Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle. https://isabelle.in.tum.de (2024), version 2023
  22. 22.O’Hearn, P.W.: Separation logic. Communications of the ACM 62(2), 86–95 (Feb 2019). https://doi.org/10.1145/3211968
  23. 23.OpenAI: Openai o1 system card. Technical report, OpenAI (2024), includes safety evaluations and red teaming results for the o1 and o1-mini models
  24. 24.Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’05). pp. 247–258. Association for Computing Machinery, New York, NY, USA (2005). https://doi.org/10.1145/1040305.1040327
  25. 25.Perry, N., Srivastava, M., Kumar, D., Boneh, D.: Do users write more insecure code with AI assistants? In: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS). pp. 2785–2799. ACM (2023). https://doi.org/10.1145/3576915.3623157
  26. 26.Poesia, G., Loughridge, C., Amin, N.: dafny-annotator: AI-assisted verification of Dafny programs. CoRR abs/2411.15143 (2024), https://arxiv.org/abs/2411.15143, arXiv:2411.15143
  27. 27.Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002). pp. 55–74. IEEE Computer Society, Los Alamitos, CA, USA (2002). https://doi.org/10.1109/LICS.2002.1029817
  28. 28.Sun, C.E., Gao, S., Weng, T.W.: Breaking the barrier: Enhanced utility and robustness in smoothed drl agents. ICML (2024)
  29. 29.Sun, C., Agashe, V., Chakraborty, S., Taneja, J., Barrett, C.W., Dill, D.L., Qiu, X., Lahiri, S.K.: ClassInvGen: Class invariant synthesis using large language models. CoRR abs/2502.18917 (2025), https://arxiv.org/abs/2502.18917
  30. 30.Sun, C., Sheng, Y., Padon, O., Barrett, C.: Clover: Closed-loop verifiable code generation. In: AI Verification (SAIV 2024). Lecture Notes in Computer Science, vol. 14846, pp. 134–155. Springer, Cham (2024). https://doi.org/10.1007/978-3-031-65112-0_7
  31. 31.The Coq Development Team: The Coq proof assistant. https://coq.inria.fr (2024), version 8.19.0
  32. 32.Verus Contributors: Verus tutorial and reference (2025), https://verus-lang.github.io/verus/guide/
  33. 33.Verus Contributors: vstd: Verus standard library api documentation (2025), https://verus-lang.github.io/verus/verusdoc/vstd/
  34. 34.Verus Project: Verilib. https://verilib.org/, accessed: 2025-02-17
  35. 35.Wang, Z., Liu, K., Li, G., Jin, Z.: Hits: High-coverage LLM-based unit test generation via method slicing. In: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering. p. 1258–1268. ASE ’24, Association for Computing Machinery, New York, NY, USA (2024). https://doi.org/10.1145/3691620.3695501, https://doi.org/10.1145/3691620.3695501
  36. 36.Wang, Z., Zhou, Z., Song, D., Huang, Y., Chen, S., Ma, L., Zhang, T.: Towards understanding the characteristics of code generation errors made by large language models. In: Proceedings of the 47th IEEE/ACM International Conference on Software Engineering (ICSE) (2025), to appear
  37. 37.Wen, C., Cao, J., Su, J., Xu, Z., Qin, S., He, M., Li, H., Cheung, S.C., Tian, C.: Enchanting program specification synthesis by large language models using static analysis and program verification. In: Computer Aided Verification (CAV 2024). Lecture Notes in Computer Science, vol. 14682, pp. 302–328. Springer (2024). https://doi.org/10.1007/978-3-031-65630-9_16
  38. 38.Wu, H., Barrett, C., Narodytska, N.: Lemur: Integrating large language models in automated program verification. In: The Twelfth International Conference on Learning Representations
  39. 39.Yang, C., Li, X., Misu, M.R.H., Yao, J., Cui, W., Gong, Y., Hawblitzel, C., Lahiri, S., Lorch, J.R., Lu, S., Yang, F., Zhou, Z., Lu, S.: AutoVerus: Automated proof generation for Rust code. CoRR abs/2409.13082 (2024), https://arxiv.org/abs/2409.13082

Citation

MLA
Sun, C., et al. “VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus”. arXiv, 2025, http://arxiv.org/abs/2510.25015v4.
APA
Sun, C., Sun, Y., Amrollahi, D., Zhang, E., Lahiri, S., Lu, S., Dill, D., & Barrett, C. (2025). VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. arXiv. http://arxiv.org/abs/2510.25015v4
Chicago
Sun, C., Y. Sun, D. Amrollahi, et al. 2025. “VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus”. arXiv. http://arxiv.org/abs/2510.25015v4.
Harvard
Sun, C. et al. (2025) “VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus”, arXiv [Preprint]. Available at: http://arxiv.org/abs/2510.25015v4.
Vancouver
1. Sun C, Sun Y, Amrollahi D, Zhang E, Lahiri S, Lu S, Dill D, Barrett C (2025) VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus. arXiv

BibTeX

@article{sun2025veristruct,
  title = {VeriStruct: AI-assisted Automated Verification of Data-Structure Modules in Verus},
  author = {Sun, Chuyue and Sun, Yican and Amrollahi, Daneshvar and Zhang, Ethan and Lahiri, Shuvendu and Lu, Shan and Dill, David and Barrett, Clark},
  year = {2025},
  journal = {arXiv},
  url = {http://arxiv.org/abs/2510.25015v4},
  eprint = {2510.25015}
}
Metadata:arXiv

Source Code

This paper has an official code repository available. Click below to access the source code.

View Repository

Access the Paper

This paper is available from its original source. Click below to access the PDF.

Open PDF
License: https://creativecommons.org/licenses/by/4.0/