Skip to content

Draft: formal audit article#33

Draft
fricoben wants to merge 1 commit intomainfrom
fricoben/explain-verity-lean
Draft

Draft: formal audit article#33
fricoben wants to merge 1 commit intomainfrom
fricoben/explain-verity-lean

Conversation

@fricoben
Copy link
Copy Markdown
Contributor

Summary

  • add a draft research article: How a Formal Audit Works in Detail
  • add the article to the research index

Status

This PR is intentionally a draft and should not be merged as-is.

The article needs a complete refactor.

Rewrite Brief

The rewrite should:

  • be based on the current /research/what-is-a-formal-proof style, pacing, and level of explanation
  • reuse the same clean article language and visual approach: simple sections, normal prose, and snippet-style blocks only when there is real code or Lean to show
  • take structural inspiration from our current Unlink Notion / proposal pages for how the audit process is explained
  • stay generic to how a formal audit works in detail
  • avoid protocol-specific examples and assumptions from the proposal, especially concrete Unlink details such as circuits

Direction For The Next Pass

The next version should focus on the actual technical workflow of a formal audit:

  • specification and scoping
  • threat model and attack-surface mapping
  • modeling the relevant contract logic in Verity
  • proving agreed invariants in Lean
  • iterative bug-finding / fix / re-proof loop
  • deliverables and maintenance semantics

Note

The benchmark repos and our existing research pages are useful source material, but the article still needs to be rewritten into the house style before it is publishable.

@vercel
Copy link
Copy Markdown

vercel Bot commented Apr 23, 2026

The latest updates on your projects. Learn more about Vercel for GitHub.

Project Deployment Actions Updated (UTC)
lfglabs-dev Ready Ready Preview, Comment Apr 23, 2026 3:11pm

Request Review

@fricoben
Copy link
Copy Markdown
Contributor Author

This draft should be treated as a placeholder only. The article needs a complete refactor so it matches the style and explanation quality of , and it should take structural inspiration from our current Unlink Notion/proposal pages without carrying over protocol-specific cases such as circuits.

@fricoben
Copy link
Copy Markdown
Contributor Author

This draft should be treated as a placeholder only. The article needs a complete refactor so it matches the style and explanation quality of /research/what-is-a-formal-proof, and it should take structural inspiration from our current Unlink Notion/proposal pages without carrying over protocol-specific cases such as circuits.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant