model-checking

6 posts

model-checkingautoverusrustverification

AutoVerus verwandelt 40 Stunden Proof-Writing in 3 LLM-Calls. Der Trick ist, zu wissen, wann man aufgibt.

AutoVerus nutzt ein Netzwerk von LLM-Agents, um Verus-Correctness-Proofs für Rust-Code zu generieren und über 90% der Proof-Obligations durch eine Generate-Repair-Discharge-Schleife zu automatisieren, die vom Feedback des SMT-Solvers getrieben wird.

Der schwierigste Teil der formalen Verifikation war nie der Verifier. Es ist das Schreiben des Proofs. Gib einem erfahrenen Rust-Engineer Verus, den…
model-checkingllmrustformal-proofs

LLMs können Rust-Code generieren. Formale Beweise sind ein ganz anderes Problem.

Große Sprachmodelle schreiben erstaunlich guten Rust-Code, aber wenn man sie um einen formalen Beweis bittet, halluzinieren sie Invarianten und erfinden Syntax, die kein Verifizierer akzeptiert. Hier ist, was sie tatsächlich richtig machen, wo sie scheitern und wie man sie dennoch nutzen kann.

LLMs können Rust schreiben, das kompiliert und sogar besteht. Was sie nicht zuverlässig können, ist einen formalen Beweis dafür zu führen, dass der Code für…
model-checkingtemporal-logicformal-methodsverification

Sie können Code mit einem Model Checker verifizieren, ohne Temporal Logic zu lernen

Bounded Model Checker wie Kani und relationale Model Finder wie Alloy ermöglichen die Verifikation von Eigenschaften mit gewöhnlichen Assertions und Constraints. Sie geben Liveness-Beweise auf, dafür ist die Lernkurve auf Stunden statt Wochen gemessen.

Sie müssen keine lineare temporale Logik lernen, um einen Model Checker zu verwenden. Tools wie Kani, CBMC und Alloy ermöglichen die Verifikation von…
model-checkingrustverificationformal-methods

Man kann Rust-Code korrekt beweisen, ohne einen einzigen Beweis zu schreiben – aber der Zustandsraum ist die Rechnung

Model-Checking-Tools wie Kani erlauben es, Rust-Eigenschaften mit Assertions statt formaler Beweise zu verifizieren. Das Problem ist, was passiert, wenn deine Schleifen keine kleinen Grenzen haben.

Man kann Rust-Code korrekt beweisen, ohne einen einzigen Beweis zu schreiben. Das Tool, das das macht, heißt Model Checker, und für Rust ist der praktischste…