Summary
Create a full worked case study demonstrating a bug that passed all code-level testing but failed in production due to an unstated mathematical assumption — and show how symproof would have caught it.
Motivation
This is a key value-prop demonstration for the "three-legged stool" concept in the README: code correctness alone is not enough. When the underlying algorithm depends on a mathematical property (convexity, invertibility, boundedness, stability margin, etc.) that doesn't hold for a particular input domain, traditional testing won't catch it because the tests verify the code does what it says, not that the mathematical preconditions are satisfied.
What this should include
-
A realistic scenario — pick a domain already covered by the library (control systems, optimization, or DeFi are strong candidates). For example:
- A controller tuned assuming a system matrix is Hurwitz, deployed on a plant where it isn't
- An optimizer assuming convexity on a function that is only convex in a restricted region
- A DeFi protocol assuming a reserve ratio bound that doesn't hold under certain market conditions
-
The "before" picture — show the code passing unit tests, integration tests, and type checks while silently depending on an unstated assumption
-
The failure — demonstrate the production failure that results from the violated assumption
-
The "after" picture — show the same system with symproof axioms making the assumption explicit, and seal() either:
- Refusing to seal because the assumption isn't axiom-backed, or
- Producing a bundle whose advisories surface the assumption for review
-
Narrative — write it up as a readable case study, not just code. Engineers should be able to follow the story and see why mathematical assumptions need to be first-class artifacts alongside code and tests.
Placement
examples/ directory as a runnable script with narrative comments- Optionally also as a section in docs (once the doc site exists, see related issue)
Summary
Create a full worked case study demonstrating a bug that passed all code-level testing but failed in production due to an unstated mathematical assumption — and show how symproof would have caught it.
Motivation
This is a key value-prop demonstration for the "three-legged stool" concept in the README: code correctness alone is not enough. When the underlying algorithm depends on a mathematical property (convexity, invertibility, boundedness, stability margin, etc.) that doesn't hold for a particular input domain, traditional testing won't catch it because the tests verify the code does what it says, not that the mathematical preconditions are satisfied.
What this should include
A realistic scenario — pick a domain already covered by the library (control systems, optimization, or DeFi are strong candidates). For example:
The "before" picture — show the code passing unit tests, integration tests, and type checks while silently depending on an unstated assumption
The failure — demonstrate the production failure that results from the violated assumption
The "after" picture — show the same system with symproof axioms making the assumption explicit, and
seal()either:Narrative — write it up as a readable case study, not just code. Engineers should be able to follow the story and see why mathematical assumptions need to be first-class artifacts alongside code and tests.
Placement
examples/directory as a runnable script with narrative comments