编辑“︁Lean就业方向”︁（章节）

=== 1. 形式化验证工程师 ===
形式化验证是通过数学方法验证软件或硬件系统正确性的技术，Lean因其强大的元编程能力和可扩展性在该领域被广泛应用。

'''典型职责：'''
* 使用Lean编写形式化规范
* 构建数学证明验证系统行为
* 开发领域特定语言(DSL)的验证框架

'''示例场景：'''<br>
验证一个简单的银行转账函数，确保余额不会出现负数：

<syntaxhighlight lang="lean">
-- 定义账户状态结构
structure Account where
  balance : Nat
  deriving Repr

-- 安全转账函数
def safe_transfer (sender : Account) (receiver : Account) (amount : Nat) : Option (Account × Account) :=
  if amount ≤ sender.balance then
    some ({sender with balance := sender.balance - amount}, {receiver with balance := receiver.balance + amount})
  else
    none

-- 验证性质：转账后总余额不变
theorem transfer_preserves_total (s₁ s₂ : Account) (amt : Nat) :
  match safe_transfer s₁ s₂ amt with
  | some (s₁', s₂') => s₁'.balance + s₂'.balance = s₁.balance + s₂.balance
  | none => True :=
by
  simp [safe_transfer]
  split <;> simp [*]
</syntaxhighlight>

'''输出验证：'''
<pre>
Proof succeeded!
</pre>