Creusot 0.9.0: Launching the Creusot Devlog
Summary
Creusot 0.9.0 announces the Devlog launch and highlights key features: automatic insertion of type invariants into loop invariants, a renamed creusot_std library with no_std compatibility, and initial concurrency support via AtomicI32 and AtomicInvariant. The post also covers Creusot’s POPL 2026 presence, a new tutorial, and ongoing work on supporting concurrent verification and embedded contexts.