diff --git a/.clang-format b/.clang-format
new file mode 100644
index 000000000..0a879bb95
--- /dev/null
+++ b/.clang-format
@@ -0,0 +1,75 @@
+# Z3 Theorem Prover clang-format configuration
+# Based on analysis of existing codebase style patterns
+
+BasedOnStyle: LLVM
+
+# Indentation
+IndentWidth: 4
+TabWidth: 4
+UseTab: Never
+
+# Column width
+ColumnLimit: 120
+
+# Braces
+BreakBeforeBraces: Linux
+Cpp11BracedListStyle: true
+
+# Classes and structs
+BreakConstructorInitializers: BeforeColon
+ConstructorInitializerIndentWidth: 4
+AccessModifierOffset: -4
+
+# Function definitions
+AlwaysBreakAfterReturnType: None
+AllowShortFunctionsOnASingleLine: Empty
+AllowShortIfStatementsOnASingleLine: false
+AllowShortLoopsOnASingleLine: false
+
+# Spacing
+SpaceAfterCStyleCast: false
+SpaceAfterLogicalNot: false
+SpaceBeforeParens: ControlStatements
+SpaceInEmptyParentheses: false
+SpacesInCStyleCastParentheses: false
+SpacesInParentheses: false
+SpacesInSquareBrackets: false
+
+# Alignment
+AlignConsecutiveAssignments: false
+AlignConsecutiveDeclarations: false
+AlignOperands: true
+AlignTrailingComments: true
+
+# Line breaks
+AllowAllParametersOfDeclarationOnNextLine: true
+BinPackArguments: true
+BinPackParameters: true
+BreakBeforeBinaryOperators: None
+BreakBeforeTernaryOperators: true
+
+# Includes
+SortIncludes: false  # Z3 has specific include ordering conventions
+
+# Namespaces
+NamespaceIndentation: None
+
+# Comments and documentation
+ReflowComments: true
+SpacesBeforeTrailingComments: 2
+
+# Language standards
+Standard: c++20
+
+# Penalties (for line breaking decisions)
+PenaltyBreakAssignment: 2
+PenaltyBreakBeforeFirstCallParameter: 19
+PenaltyBreakComment: 300
+PenaltyBreakFirstLessLess: 120
+PenaltyBreakString: 1000
+PenaltyExcessCharacter: 1000000
+PenaltyReturnTypeOnItsOwnLine: 60
+
+# Misc
+KeepEmptyLinesAtTheStartOfBlocks: false
+MaxEmptyLinesToKeep: 1
\ No newline at end of file