v1.16.0 — engineer 0.32.0

engineer 0.32.0: formal verification with TLA+ and Lean

Now you can:

• Model-check your code with TLA+. /engineer.tlaplus models retries, locks, async flows and state machines as written, and TLC checks every interleaving, not just the ones your tests happen to hit.
• Prove all-inputs invariants with Lean. /engineer.lean proves that a property holds for every input: a masker never leaks a password, a rounding rule never loses a cent.

How it keeps paying off in your project:

• Counterexamples become failing tests in your suite. Any violation is reproduced against your real code and pinned with a test that fails before the fix and passes after. The model is scaffolding; the test stays.
• It only runs where your code warrants it. /engineer.refinement-advisor reads each diff and recommends TLA+, Lean, mutation testing, an introversion scan, or nothing, each with a reason. For formal checks it drafts the invariant. You pick with one click.
• It's part of the pipeline, not a side quest. /engineer.harden gives CP8 a skill of its own for features and fixes alike. It runs the selected checks and records a reason for anything skipped.