Skip to content

1.9.0

Choose a tag to compare

@leoveanv leoveanv released this 06 Mar 22:27
· 1528 commits to main since this release

2026-03-07

BREAKING CHANGES

  • core.expression() renamed to core.symbolic(); no backward-compatibility alias

Added

  • Axiom formal verification engine via cloud Axle SDK (pip install symbolicai[lean])
  • core.formal() decorator routing to the new formal engine
  • Interface('axiom') with 14 Lean4 tools (check, verify_proof, disprove, etc.)
  • @contract post-conditions can delegate LLM outputs to Lean4 for proof verification
  • GPT-5.4 and GPT-5.4 Pro model support with resilient client config
  • Claude Sonnet 4.6 support with 1-hour prompt caching enabled by default
  • FORMAL_ENGINE_API_KEY / FORMAL_ENGINE config pair for formal verification
  • Local Lean4 engine (FORMAL_ENGINE=local) via Docker, moved to formal package

Changed

  • OpenAI Responses client uses 600s timeout and 3 retries for long-running models

Fixed

  • Bump lxml-html-clean from 0.4.3 to 0.4.4

Maintenance

  • Refactor Parallel search engine: use SDK Pydantic types, pre-compile regex, use tldextract
  • Simplify neuro-symbolic engine tests

Full Changelog: 1.8.3...1.9.0