“Validating Lemmas with Rustdoc [...]”
summary
Describes a pipeline that uses RustDoc links as the edges of a directed proof graph to validate security and integrity of web and API server code, framing obligations, assumptions and requirements as semiformal proofs. Tooling parses link targets and texts, finds dangling references and mismatched assertions, detects circular logic, catalogs every place a given assumption is used (files contain 1–100 assumptions), and integrates with blame to flag code that changed since last review, giving automated, actionable evidence the approach works.
AI-written summary · about
related talks
35mThe practical implementation of Documentation as Code
24mEscaping the Curse of Outdated Docs
14mExploring possibilities for integrating StrictDoc with ELISA's requirements temp...
32mA Survey of Weak Reasoning Assistants
07mTooling and Sharing Traceability Discussion
31mAutomating Linux Kernel Documentation for Safety-Criti...
23mSecurity Considerations in API Docs
27mProduction Language Specification - Requirements for Multiple Usages