- 01You say what must holdPoint Aristotle at your code. No spec needed: describe what should always be true in plain English, or let it propose the properties that matter most.
- 02Aristotle works out the proofIt reads your code and works through the proof one step at a time. If it refutes a property, it tells you why.
- 03You get a verdict, not a guessEach property comes back proved, refuted, or left open if Aristotle couldn’t settle it, with the assumptions behind every proof. Run it on every commit.
Agent
Prove that the code executes without undefined behavior for every record satisfying the caller obligations, and that the response is no longer than the record that requested it.
Proves the upstream fixThe two length checks from OpenSSL 1.0.1g make both claims true.
Refutes both claimsA three-byte request makes the code overread 65,535 bytes and send 65,554.
Models the C code in LeanRecords, reads and the length handed to the network, written down exactly.
Aristotle worked for 8m 31s · 39 steps
Output summary
Checking your code
- ORIGINAL_
MEMORY_ NegatedSAFE - ORIGINAL_
RESPONSE_ NegatedLE_ REQUEST - FIXED_
MEMORY_ ProvedSAFE - FIXED_
RESPONSE_ ProvedLE_ REQUEST
Both claims fail on the original code, and both hold once the two length checks are in.
