rust

9 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-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…
capability-based-securityrustcap-stdsandboxing

Deine Dependencies können jede Datei auf dem Datenträger lesen. cap-std zwingt sie, um Erlaubnis zu fragen.

Die Standardbibliothek von Rust gewährt jeder Dependency umgebungsbasierte Dateisystemberechtigungen. cap-std ersetzt sie durch Capability-basierte APIs, die Code zwingen, nachzuweisen, dass er das Recht hat, auf einen Pfad zuzugreifen, bevor er ihn öffnet.

Jede Crate in deinem Dependency-Tree kann öffnen, in dein -Verzeichnis schreiben oder jede Datei in deinem Projekt auflisten. Die Standardbibliothek von Rust…
deep-divesmutation-testingrustcargo-mutantstest-quality

Mutation Testing in Rust funktioniert, aber deine Compile-Zeiten werden es hassen

cargo-mutants findet die Tests, die nur so tun, als würden sie deinen Code prüfen. Hier erfährst du, wie Mutation Testing in Rust funktioniert, was es findet und ob sich der Compile-Time-Aufwand lohnt.

Du hast 100% Line Coverage. Jeder Branch wird getroffen. Jede Funktion wird aufgerufen. Dann ändert jemand ein in ein in deiner Pricing-Logik, führt die Tests…
deep-divesrustproperty-based-testingquickcheckproptest

Property-Based Tests in Rust finden die Bugs, die deine Unit Tests übersehen

Beispielbasiertes Testing deckt nur die Inputs ab, an die du gedacht hast. Property-Based Testing generiert zufällige Daten, prüft Invarianten und reduziert Fehler auf minimale Gegenbeispiele.

Du hast eine -Funktion geschrieben. Du hast sie mit und getestet. Sie besteht. Du veröffentlichst sie. Ein Nutzer übergibt einen Slice mit einem einzigen…
deep-divesrustruntime-contractsperformance

Rust-Runtime-Contracts können in Release-Builds kostenlos sein, aber der Compiler macht das nicht für dich

Rust entfernt Debug-Assertions automatisch, aber echtes Design-by-Contract braucht mehr als debug_assert!. So baust du zero-cost runtime contracts, die aus deinem Release-Binary verschwinden.

Rust kann runtime contracts in der Entwicklung erzwingen und sie komplett aus Release-Builds entfernen. Die Einschränkung ist, dass die Sprache contracts nicht…